nLab optic (in computer science)

Contents

Contents

Idea

Optics are constructions used in computer science as bidirectional data accessors. They include lenses and prisms, used to access and modify, respectively, components of product data types and components of coproduct data types.

Unlike lenses, in general optics do not require a cartesian structure to be present. That’s replaced by a bi-actegorical structure and a quotient which ‘ties’ residual and incoming views.

Definition

Let (M,I,)(\mathbf M, I, \otimes) be a symmetric monoidal category. Let C\mathbf C and D\mathbf D be M\mathbf M-actegories, i.e. there are pseudoactions \bullet and *\ast of M\mathbf M acting on C\mathbf C and D\mathbf D, respectively.

Definition

The category of (C,D)(\mathbf C, \mathbf D)-mixed optics Optic ,*(C,D)\mathrm{Optic}_{\bullet, \ast}(\mathbf C, \mathbf D) has objects given by pairs (X:C,Y:D)(X : \mathbf C,Y : \mathbf D) and hom-sets given by

Optic ,*(C,D)((S,T),(A,B))= M:MC(S,MA)×D(M*B,T) \mathrm{Optic}_{\bullet, \ast}(\mathbf C, \mathbf D)((S,T),(A,B)) = \int^{M : \mathbf M} \mathbf C(S, M \bullet A) \times \mathbf D(M \ast B, T)

Optics are morphisms in this category. See Riley 2018 for the composition rule.

Remark

Concretely, an optic (S,T)(A,B)(S,T) \to (A,B) is specified by a triple of (l,M,r)(l, M, r) where M:MM : \mathbf M is called residual, l:SMAl : S \to M \bullet A is called ‘view’ or ‘get’ or ‘forward part’ or ‘left part’, and r:M*BTr : M \ast B \to T is called ‘update’ or ‘put’ or ‘backward part’ or ‘right part’.

Remark

In the non-mixed case M=C=D\mathbf M = \mathbf C = \mathbf D, the category of optics is defined exactly as the ‘double’ of C\mathbf C as introduced by Pastro and Street in PS07. Their theory has been extended to the mixed case in CEGLMPR20. This provides the fundamental link between optics and the theory of Tambara modules, which gives to mixed-optics the alternative name of ‘profunctor optics’. See ‘Profunctor representation’.

The coend in the above definition has the effect of making two optics (l,M,r)(l, M, r) and (l,M,r)(l', M', r') (with same boundaries) equal if there exists a morphism α:MM\alpha : M \to M' such that (αA)l=l(\alpha' \bullet A) \circ l = l' or a morphism β:MM\beta:M' \to M such that r=r(β*B)r = r' \circ (\beta \ast B).

One says optics are defined up to sliding along the residual, a terminology suggested by the graphical representation of optics as open diagrams, see (Román).

Profunctor representation

Let (M,I,)(\mathbf M, I, \otimes) be a monoidal V-category with two monoidal actions ():MCC(\bullet) \colon \mathbf{M} \otimes \mathbf{C} \to \mathbf{C} and (*):MDD(\ast) \colon \mathbf{M} \otimes \mathbf{D} \to \mathbf{D}. A generalized Tambara module is a V-profunctor P:C opDVP \colon \mathbf{C}^{op} \otimes \mathbf{D} \to \mathbf{V} endowed with a family of morphisms

t M,A,B:P(A,B)P(MA,M*B)t_{M,A,B} \colon P(A,B) \to P(M \bullet A, M \ast B)

V-natural in ACA \in \mathbf{C} and BDB \in \mathbf{D} and V-dinatural in MMM \in \mathbf{M}, which additionally satisfies some axioms, see PS07.

Generalized Tambara modules are the copresheaves of the category of optics, see CEGLMPR20.

References

A brief account of the purpose of optics is in:

A similar, but more detailed account, is in:

Articles:

Last revised on March 14, 2024 at 06:55:09. See the history of this page for a list of all contributions to it.