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

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

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

(TODO)

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 October 5, 2021 at 07:10:09. See the history of this page for a list of all contributions to it.