Categorial Optics

Contribuitor

• Adriana-Ioana Bălan
• Silviu-George Pantelimon

Generalized optics

Let there be two categories $\mathcal{C}$ and $\mathcal{D}$ with objects $S, A \in \mathcal{C}$ and $T, B \in \mathcal{D}$. A (generalized) $(Ⓛ,Ⓡ)$-optic from $(S, T)$ to focuses $(A, B)$ is an element of the following coend:

$$\mathbf{Optic}_{Ⓛ, Ⓡ}((A, B),(S, T)) = \int^{M \in \mathcal{M}} \mathcal{C}(S, M Ⓛ A) \times \mathcal{D}(M Ⓡ B, T)$$

where $\mathcal{M}$ is a monoidal category with two (left) actions $Ⓛ$, $Ⓡ$ acting on $\mathcal{C}$, respectively $\mathcal{D}$.

An optic, conceptually, is a bidirectional data accessor. For a programmer it is easy to imagine that the optic basically decomposes a type or data structure through a monoidal action to view a nested structure. The result of the decomposition is a context or residual that recomposes with other data to get a composite object. A programmer would have trouble taking advantage of an optic in this form, especially because the most widely used programming languages do not support very abstract semantics like Haskell does, for instance.

The coend is a class of equivalence of all the ways the two hom-objects/hom-sets interact through the residual $M$. When the monoidal actions are known and have convenient properties the coend reduces via these properties and Yoneda reductions to a more manageable form. Various specialized optics have already been presented in the literature, but we would like to review some of those and propose ways to make them more accessible to programmers. Furthermore, the literature actively has been growing the past years, and optics have been subjected to analysis from various viewpoints. Many of the results are dependent on the properties of the categories assumed by the authors when working optics. We will be focussing only on some aspects of optics and from here on out we will propose a few tweeks to optics relax some requirements.

First, we should point out that the most important aspect of optics is that they are higher lever abstractions that can be composed easily. The composition is a consequnce of the axioms of the monoidal actions. Any two $(Ⓛ,Ⓡ)$-optics can be composed as follows:

$$\mathbf{Optic}_{(Ⓛ,Ⓡ)}((A, B),(S, T)) \times \mathbf{Optic}_{(Ⓛ,Ⓡ)}((Z, W),(A, B)) =$$ $$\int^{M \in \mathcal{M}} \mathcal{C}(S, M Ⓛ A) \times \mathcal{D}(M Ⓡ B, T) \times \int^{N \in \mathcal{M}} \mathcal{C}(A, N Ⓛ Z) \times \mathcal{D}(N Ⓡ W, B) \rightarrow$$ $$\int^{M,N \in \mathcal{M}} \mathcal{C}(S, M Ⓛ A) \times \mathcal{C}(A, N Ⓛ Z) \times \mathcal{D}(N Ⓡ W, B) \times \mathcal{D}(M Ⓡ B, T) \rightarrow$$ $$\int^{M,N \in \mathcal{M}} \mathcal{C}(S, M Ⓛ N Ⓛ Z) \times \mathcal{D}(M Ⓡ N Ⓡ W, T) \rightarrow$$ $$\int^{M,N \in \mathcal{M}} \mathcal{C}(S, (M \otimes N) Ⓛ Z) \times \mathcal{D}((M \otimes N) Ⓡ W, T) \rightarrow$$ $$\int^{P \in \mathcal{M}} \mathcal{C}(S, P Ⓛ Z) \times \mathcal{D}(P Ⓡ W, T) =$$ $$\mathbf{Optic}_{(Ⓛ,Ⓡ)}((Z, W),(S, T))$$

We can clearly observe from the demonstration that the two monoidal actions are conveniently strong just so we can compose the hom-sets in both directions. However, we can also see that the two monoidal actions work independently from one another; they only interact through the residuals. Element-wise, optics $\braket{l_{1}|r_{1}}, \braket{l_{2}|r_{2}}$, $l_{1}: S \rightarrow M Ⓛ A, l_{2}: A \rightarrow N Ⓛ Z, r_{1}: M Ⓡ B \rightarrow T, r_{2}: N Ⓡ W \rightarrow B$ compose as follows:

$$\braket{l_{2}|r_{2}} \circ \braket{l_{1}|r_{1}} = \braket{\alpha^{-1}_{Ⓛ~M, N, Z} \circ (id_{M} Ⓛ l_{2}) \circ l_{1}|r_{1} \circ (id_{M} Ⓡ r_{2}) \circ \alpha_{Ⓡ~M, N, W}}$$

Theorem - Functorial lifting of functors

Let there be functors $F_{cst} : \mathcal{C} \rightarrow \mathcal{C'}$ and $F_{str} : \mathcal{D} \rightarrow \mathcal{D'}$ exhibiting tensorial (left-)costrength respectively tensorial (left-)strength over the respective (left-)actions of a (Ⓛ,Ⓡ)-optic. The pair $(F_{cst}, F_{str})$ determines a (pseudo)functor mapping (Ⓛ,Ⓡ)-optics to (Ⓛ',Ⓡ')-optics enabled by costrength respectively strength by mapping obj:

$$(F_{cst}, F_{str}) : \mathbf{Optic}_{Ⓛ,Ⓡ} \rightarrow \mathbf{Optic}_{Ⓛ',Ⓡ'}$$

Basically, the functor pair applies the following way by pairs of objects $(F_{cst}, F_{str})((A, B)) = (F_{cst}A, F_{str}B)$ and optics $\braket{l|r},~l : S \rightarrow M Ⓛ A,~r : M Ⓡ B \rightarrow T$ to $(F_{cst}, F_{str})(\braket{l|r}) = \braket{cst \circ F_{cst} l|F_{str} \circ str}$:

$$\mathbf{Optic}_{Ⓛ,Ⓡ}((A, B), (S, T)) \xrightarrow{(F_{cst}, F_{str})}$$ $$\int^{M \in \mathcal{M}}\mathcal{C}(F_{cst}S, F_{cst}(M Ⓛ A)) \times \mathcal{D}(F_{str}(M Ⓡ B), F_{str}T) \xrightarrow{cst_{M,A}, str_{M,B}}$$ $$\int^{M \in \mathcal{M}}\mathcal{C}(F_{cst}S, M Ⓛ' F_{cst}A) \times \mathcal{D}(M Ⓡ' F_{str}B, F_{str}T) =$$ $$\mathbf{Optic}_{Ⓛ',Ⓡ'}((F_{cst}S, F_{str}T), (F_{cst}A, F_{str}B)) =$$ $$(F_{cst}, F_{str})(\mathbf{Optic}_{Ⓛ,Ⓡ}((A, B), (S, T)))$$

Proof. For $(F_{cst}, F_{str})$ to be a functor it must preserve identity and composition. The identity for optics is induced by the unitors, as pointed out by, $id_{(S, T)} = \braket{\lambda^{-1}_{Ⓛ}|\lambda_{Ⓡ}}$.

$$(F_{cst}, F_{str})(id_{(S, T)}) = (F_{cst}, F_{str})(\braket{\lambda^{-1}_{Ⓛ,S}|\lambda_{Ⓡ, T}}) =$$ $$\braket{F_{cst}\lambda^{-1}_{Ⓛ,S}|F_{str}\lambda_{Ⓡ,T}} \xrightarrow{cst_{I_{\mathcal{C}},S}, str_{I_{\mathcal{D}},T}} \braket{\lambda^{-1}_{Ⓛ',F_{cst}S}|\lambda_{Ⓡ',F_{str}T}}$$ $$\mathbf{Optic}_{Ⓛ, Ⓡ}((A, B),(S, T)) \times \mathbf{Optic}_{Ⓛ, Ⓡ}((Z, W),(A, B)) =$$ $$\mathbf{Optic}_{Ⓛ, Ⓡ}((Z, W),(S, T))$$ $$(F_{cst}, F_{str})(\mathbf{Optic}_{Ⓛ, Ⓡ}((A, B),(S, T))) \times (F_{cst}, F_{str})(\mathbf{Optic}_{Ⓛ, Ⓡ}((Z, W),(A, B))) =$$ $$\mathbf{Optic}_{Ⓛ, Ⓡ}((F_{cst}A, F_{str}B),(F_{cst}S, F_{str}T)) \times \mathbf{Optic}_{Ⓛ, Ⓡ}((F_{cst}Z, F_{str}W),(F_{cst}A, F_{str}B)) \rightarrow$$ $$\mathbf{Optic}_{Ⓛ', Ⓡ'}((F_{cst}Z, F_{str}W),(F_{cst}S, F_{str}T)) = (F_{cst}, F_{str})(\mathbf{Optic}_{Ⓛ, Ⓡ}((Z, W),(S, T)))$$

Resources

• Profunctor Optics
• Categories of Optics
• Optics, functorially