constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
In computer science, originally in database theory, a data structure called lenses [Bohannon, Pierce & Vaughan (2006, §3), Foster, Greenwald, Moore, Pierce & Schmitt (2007, §3)] is used to formally capture situations where from some data(-base) may be extracted a specific view (say one field in a record structure) in such a way that changes made to the view can be reflected as updates to the original data.
The same construction has been devised on numerous occasions (cf. Hedges (2018)).
In particular, “well-behaved lenses” (BPV06, Def. 3.2those for which updates of the “view” completely overwrite any previous such changes) turn out to equivalently be just the coalgebras of the costate comonad (cf. monads in computer science), an observation due to O’Connor (2010), (2011); see Prop. below.
More generally, there are two different approaches to lenses:
Lawful lenses are an algebraic structure which axiomatize product projections. The laws govern the ways views and updates relate. These are generalized into Delta lenses, which are more flexible lawful lenses.
Lawless lenses, and in particular bi-directional or polymorphic lenses, separate the two directions of view and update so that the laws no longer type-check. These lawless lenses are used to organize bi-directional flow of data, and are generalized into optics in the functional programming literature.
An alternate generalization of lawless lenses is put forward in Spivak 19 as the Grothendieck construction of the fiberwise dual of an indexed category. This notion of lawless lens has been adopted in the context of categorical systems theory because they represent a bidirectional stateful computation which describes the way some systems expose and update their internal state. For instance, see Myers, Spivak & Niu or Hedges (2021).
In this sense, lawless lenses are applications of two mathematical frameworks which are interesting in their own right: fibrations and optics (thus Tambara modules).
Let $(\mathbf{C}, 1, \times)$ be a category with finite products.
Let $S,V$ be objects of $\mathbf C$. A (lawful) lens $L$, with source $S$ and view $V$, is a pair of arrows $\mathrm{get} : S \to V$ and $\mathrm{put} : V \times S \to S$, often taken to satisfy the following equations, or lens laws:
The two morphisms comprising a lens can also be called ‘view’ and ‘update’. More generally, they are referred to as the ‘forward’ and ‘backward’ parts of the lens.
Sometimes a lens satisfying all three laws is said to be lawful. Sometimes it is said that a well-behaved lens satisfies (1) and (2) and a very well-behaved lens satisfies also (3).
Lenses (regardless of their lawfulness) organize in a category $\mathrm{Lens}(\mathbf C)$ whose objects are the same as $\mathbf C$ and whose morphisms $X \to Y$ are lenses with states $X$ and views $Y$. The identity lens is given by $(1_X, \pi_1) :X \to X$. Composition of $(\mathrm{get}_1, \mathrm{put}_{1}):X \to Y$ and $(\mathrm{get}_2, \mathrm{put}_{2}):Y \to Z$ is given by:
The $\mathrm{put}_{12}$ morphism is probably easier to describe using generalized elements:
Crucially, associativity of this composition relies on naturality of the diagonals, which is a given in cartesian categories but not in more general monoidal categories. Optics are a sweeping generalization of lenses which overcomes this obstacle.
Moreover, the cartesian product of $\mathbf C$ endows $\mathrm{Lens}(\mathbf{C})$ of a monoidal product.
See (Johnson-Rosebrugh-Wood 2010, Proposition 9). See also the possibility operator.
Let $\mathbf{C} = Set$. Then every lens $L = (S, V, \mathrm{get}, \mathrm{put})$ is equivalent a “constant complement” lens whose Get is a product projection $\pi_{1} : C \times V \to V$ and whose Put is the function $\pi_{0,2} : C \times V \times V \to C \times V$ for some set $C$.
(well-behaved lenses are the costate coalgebras)
For $\mathbf{C}$ a cartesian closed category, the well-behaved lenses in $\mathbf{C}$ are equivalently the coalgebras of the CoState comonad, i.e. that induced by the internal hom-adjunction:
There are many generalizations of lenses which have been proposed, however they can be broadly classified into those which satisfy analogues of the lens laws, and those without any axioms or laws.
These sorts of lenses are generalized by Spivak 19. For a quick explanation of how these sorts of generalized lenses are of use in systems theory, see Myers20; for a longer explanation, see Chapter 2 of Myers.
Delta lenses are a generalization which does satisfy laws. Here we have categories $S$ and $V$ called the source and view, together with a Get functor $g : S \to V$ and a function $\varphi \colon S_{0} \times_{V_{0}} V_{1} \to S_{1}$ which takes a pair $(s \in S, u : g s \to v \in V)$ to a morphism
$\varphi(s, u) : s \to p(s, u)$ in $S$ where $p(s, u) = cod(\varphi(a, u))$ is the Put function. The function $\varphi$ must also satisfy three lens laws. When $S$ and $V$ are codiscrete categories, delta lenses are equivalent to a lens in Set; see (Johnson-Rosebrugh 2016, Proposition 4).
A morphism between directed containers is another kind of generalised lens satisfying laws called update-update lenses; see (Ahman-Uustalu 2017, Section 5). These are equivalent to cofunctors.
Aaron Bohannon, Benjamin C. Pierce, Jeffrey A. Vaughan, Relational lenses: a language for updatable views, Proceedings of Principles of Database Systems (PODS) (2006) 338-347 [doi:10.1145/1142351.1142399, pdf]
J. N. Foster, M. B. Greenwald, J. T. Moore, Benjamin C. Pierce, A. Schmitt, Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem, ACM Transactions on Programming Languages and Systems 29 3 (2007) 17-es [doi:x10.1145/1232420.1232424]
Michael Johnson, Robert Rosebrugh, Richard Wood, Algebras and Update Strategies, Journal of Universal Computer Science, 16, 2010 (doi:10.3217/jucs-016-05-0729)
Michael Johnson, Robert Rosebrugh, and Richard J. Wood. Lenses, fibrations and universal translations. Math. Structures Comput. Sci., 22(1):25–42, 2012
Michael Johnson, Robert Rosebrugh, Unifying Set-Based, Delta-Based and Edit-Based Lenses, CEUR Workshop Proceedings, 1571, 2016 (pdf)
Danel Ahman, Tarmo Uustalu, Taking updates seriously, CEUR Workshop Proceedings, 1827, 2017 (pdf)
Mitchell Riley, Categories of optics, preprint, 2018 (arXiv:1809.00738)
David Spivak, Generalized Lens Categories via functors $C^{op} \to Cat$ (arXiv:1908.02202)
David Jaz Myers, Double Categories of Dynamical Systems (Extended Abstract) (arXiv:2005.05956)
Michael Johnson, Robert Rosebrugh, The more legs the merrier: A new composition for symmetric (multi-)lenses, EPTCS, 333, 2020 (arXiv:2101.10482)
Bryce Clarke, Internal lenses as functors and cofunctors, EPTCS, 323, 2020 (doi:10.4204/EPTCS.323.13)
Bryce Clarke, A diagrammatic approach to symmetric lenses, EPTCS, 333, 2021 (arXiv:2101.10481)
Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore, Mario Román, Profunctor optics, a categorical update, (arXiv:2001.07488)
The observation that lenses are equivalently nothing but the coalgebras of the costate comonad (cf. monads in computer science) is due to:
Russell O’Connor, Lenses Are Exactly the Coalgebras for the Store Comonad (30th Nov 2010) [r6research:23705]
Russell O'Connor, Functor is to Lens as Applicative is to Biplate: Introducing Multiplate, contribution to ICFP ‘11: ACM SIGPLAN International Conference on Functional Programming (2011) [arXiv:1103.2841]
Early review:
Further details:
Further review:
Jules Hedges, Lenses for philosophers (2018) [blog post]
David Spivak, Lenses: applications and generalizations, talk at ACT 19 (slides, pdf)
David Jaz Myers, Categorical systems theory, [github, pdf]
David Spivak, Nelson Niu, Polynomial Functors: A General Theory of Interaction [webpage, pdf]
Jules Hedges, Lenses as a foundation for cybernetics, CyberCat seminar, youtube
Last revised on January 26, 2023 at 14:47:55. See the history of this page for a list of all contributions to it.