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.
Let $(\mathbf M, I, \otimes)$ be a symmetric monoidal category. Let $\mathbf C$ and $\mathbf D$ be $\mathbf M$-actegories, i.e. there are pseudoactions $\bullet$ and $\ast$ of $\mathbf M$ acts on $\mathbf C$ and $\mathbf D$, respectively.
The category of optics $(\mathbf C, \mathbf D)$-mixed optics $\mathrm{Optic}_{\bullet, \ast}(\mathbf C, \mathbf D)$ has objects given by pairs $(X : \mathbf C,Y : \mathbf D)$ and hom-sets given by
Optics are morphisms in this category. See (Riley) for the composition rule.
Concretely, an optic $(S,T) \to (A,B)$ is specified by a triple of $(l, M, r)$ where $M : \mathbf M$ is called residual, $l : S \to M \bullet A$ is called ‘view’ or ‘get’ or ‘forward part’ or ‘left part’, and $r : M \ast B \to T$ is called ‘update’ or ‘put’ or ‘backward part’ or ‘right part’.
In the non-mixed case $\mathbf M = \mathbf C = \mathbf D$, the category of optics is defined exactly as the ‘double’ of $\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)$ and $(l', M', r')$ (with same boundaries) equal if there exists a morphism $\alpha : M \to M'$ such that $(\alpha' \bullet A) \circ l = l'$ or a morphism $\beta:M' \to M$ such that $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)
(TODO)
A brief account of the purpose of optics is in:
A similar, but more detailed account, is in:
Articles:
Mitchell Riley, Categories of optics, (arXiv:1809.00738)
Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore, Mario Román, Profunctor optics, a categorical update, 2020, (arXiv:2001.07488)
Mario Román, Open Diagrams via Coend Calculus, (arXiv:2004.04526)
Last revised on October 5, 2021 at 07:10:09. See the history of this page for a list of all contributions to it.