Let there be two categories C and D with objects S,A∈C and T,B∈D. A (generalized) (Ⓛ,Ⓡ)-optic from (S,T) to focuses
(A,B) is an element of the following coend:
OpticⓁ,Ⓡ((A,B),(S,T))=∫M∈MC(S,MⓁA)×D(MⓇB,T)
where M is a monoidal category with two (left) actions Ⓛ, Ⓡ acting on C, respectively 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:
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 ⟨l1∣r1⟩,⟨l2∣r2⟩,
l1:S→MⓁA,l2:A→NⓁZ,r1:MⓇB→T,r2:NⓇW→B
compose as follows:
Let there be functors Fcst:C→C′ and Fstr:D→D′
exhibiting tensorial (left-)costrength respectively tensorial (left-)strength over the respective (left-)actions of a
(Ⓛ,Ⓡ)-optic. The pair (Fcst,Fstr) determines a (pseudo)functor mapping
(Ⓛ,Ⓡ)-optics to (Ⓛ',Ⓡ')-optics
enabled by costrength respectively strength by mapping obj:
(Fcst,Fstr):OpticⓁ,Ⓡ→OpticⓁ′,Ⓡ′
Basically, the functor pair applies the following way by pairs of objects (Fcst,Fstr)((A,B))=(FcstA,FstrB) and optics
⟨l∣r⟩,l:S→MⓁA,r:MⓇB→T to (Fcst,Fstr)(⟨l∣r⟩)=⟨cst∘Fcstl∣Fstr∘str⟩:
Proof. For (Fcst,Fstr) 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)=⟨λⓁ−1∣λⓇ⟩.