nLab
lens (in computer science)

Idea

In computer science, originally in database theory, a concept called lenses is used to formally capture situations where some structure is converted to a different form – a view – in such a way that changes made to the view can be reflected as updates to the original structure. The same construction has been devised on numerous occasions (Hedges).

An insightful explanation and critique of the concept of “lenses” is offered in Spivak 19 (exposition in Spivak ACT19), where it is argued that the notion may and should be regarded as a small fragment (namely that of trivial display maps) of the general notion of (categorical semantics for) dependent types, such as discussed at hyperdoctrine and related entries.

This perspective, however, it’s not the end of the story. Lenses were born as abstract gadgetry to implement bidirectional (i.e. read/write) accessors for data structures, and this idea can be extended in numerous directions. Notably, optics are a better generalisation of lenses for these uses and indeed emerged first in the functional programming literature.

In this sense, lenses are but the elementary manifestation of two more interesting mathematical frameworks: fibrations and optics (thus Tambara modules?).

More recently, lenses and optics (including both the dependent and non-dependent versions) have been adopted in the context of categorical systems theory, since they represent a bidirectional stateful computation remindful of the way some systems expose and update their internal state. For instance, see first chapter of (Myers and Spivak) or (Hedges 21).

Definition

Let $(\mathbf{C}, 1, \times)$ be a category with finite products.

Definition

Let $S,V$ be objects of $\mathbf C$. A 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:

1. (PutGet) the get of a put is the projection: $\mathrm{get} \mathrm{put} = \pi_0$.
2. (GetPut) the put for a trivially updated state is trivial: $\mathrm{put} \langle \mathrm{get}, 1_S \rangle = 1_S$.
3. (PutPut) composing puts does not depend on the first view update: $\mathrm{put}(1_V \times \mathrm{put}) = \mathrm{put} \pi_{0,2}$.

Remark

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.

Remark

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).

The category of lenses

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:

$$\mathrm{get}_{12} = \mathrm{get}_1 \circ \mathrm{get}_2$$

$$\mathrm{put}_{12} = \mathrm{put}_1 \circ \langle \mathrm{put}_2 \circ \langle 1_Z, \mathrm{get}_1\rangle, 1_X \rangle \circ \langle 1_Z, \Delta_X \rangle$$

The $\mathrm{put}_{12}$ morphism is probably easier to describe using generalized elements:

$$\mathrm{put}_{12} : (z,x) \mapsto \mathrm{put}_1(\mathrm{put}_2(z, \mathrm{get}_1(x)), x)$$

Remark

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.

Properties

Proposition

Lenses are algebras for a monad generated by the adjunction:

Proof

See (Johnson-Rosebrugh-Wood 2010, Proposition 9). See also the possibility operator.

Proposition

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$.

Proof

See (Johnson-Rosebrugh-Wood 2010, Corollary 13).

Proposition

Let $\mathbf{C}$ be a cartesian closed category. Lenses in $\mathbf{C}$ are coalgebras for a comonad (the store comonad) the generated by the adjunction:

Proof

See (Gibbons-Johnson 2012, Section 3.2).

Generalizations

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.

Lenses without laws

• One generalization considers the lenses from the previous section as monomorphic by contrast to polymorphic lens which go between pairs of types, $\lambda: (S, T) \to (A, B)$, consisting of a view function, $v_{\lambda}: S \to A$, and an update function $u_{\lambda}: S \times B \to T$. Without further conditions, these are known as bimorphic lenses. To impose conditions comparable to the lens laws above requires that the types be related.

• An optic generalizes the way lenses ‘remember’ state from the forward part to the backward part, avoiding the necessity of a cartesian structure by swapping it with a sufficiently rich actegorical context.

Lenses with laws

• 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 : gs \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.

Related entries

• optic (in computer science)

• polynomial functor

• delta lens

References

Journal papers, conference proceedings, and preprints

• Aaron Bohannon, Benjamin C. Pierce, Jeffrey A. Vaughan, Relational lenses: a language for updatable views, Proceedings of Principles of Database Systems (PODS), 2006 (doi:10.1145/1142351.1142399)

• J. N. Foster, M. B. Greenwald, J. T. Moore, B. 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, 2007 (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)

• Jeremy Gibbons, Michael Johnson, Relating Algebraic and Coalgebraic Descriptions of Lenses, Electronic Communications of the EASST, 49, 2012 (doi:10.14279/tuj.eceasst.49.726)

• Michael Johnson, Robert Rosebrugh, and R. 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)

• 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)

Blog posts, talk slides, and other material

• Jeremy Gibbons, Lenses are the coalgebras for the costate comonad

• Bartosz Milewski, Lenses, Stores, and Yoneda

• Jules Hedges, Lenses for philosophers, blog post

• David Spivak, Lenses: applications and generalizations, talk at ACT 19 (slides, pdf)

• David Myers, David Spivak, Categorical systems theory, github

• Jules Hedges, Lenses as a foundation for cybernetics, CyberCat seminar, youtube