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 acts on C\mathbf C and D\mathbf D, respectively.

Definition 1. The category of optics (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) for the composition rule.

Remark 1. 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’.

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)

References

A brief account of the purpose of optics is in:

A similar, but more detailed account, is in:

  • Emily Pillmore, Mario Román, Profunctor Optics: The Categorical View, (blog post)

Articles:

Last revised on September 9, 2021 at 05:50:15. See the history of this page for a list of all contributions to it.