nLab
lens (in computer science)

Contents

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

There are, in general, two different approaches to lenses:

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

In this sense, lawless lenses are applications of two mathematical frameworks which are interesting in their own right: fibrations and optics (thus Tambara modules).

Definition

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

Definition

Let S,VS,V be objects of C\mathbf C. A (lawful) lens LL, with source SS and view VV, is a pair of arrows get:SV\mathrm{get} : S \to V and put:V×SS\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: getput=π 0\mathrm{get} \mathrm{put} = \pi_0.
  2. (GetPut) the put for a trivially updated state is trivial: putget,1 S=1 S\mathrm{put} \langle \mathrm{get}, 1_S \rangle = 1_S.
  3. (PutPut) composing puts does not depend on the first view update: put(1 V×put)=putπ 0,2\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 Lens(C)\mathrm{Lens}(\mathbf C) whose objects are the same as C\mathbf C and whose morphisms XYX \to Y are lenses with states XX and views YY. The identity lens is given by (1 X,π 1):XX(1_X, \pi_1) :X \to X. Composition of (get 1,put 1):XY(\mathrm{get}_1, \mathrm{put}_{1}):X \to Y and (get 2,put 2):YZ(\mathrm{get}_2, \mathrm{put}_{2}):Y \to Z is given by:

get 12=get 1get 2 \mathrm{get}_{12} = \mathrm{get}_1 \circ \mathrm{get}_2
put 12=put 1put 21 Z,get 1,1 X1 Z,Δ X \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 put 12\mathrm{put}_{12} morphism is probably easier to describe using generalized elements:

put 12:(z,x)put 1(put 2(z,get 1(x)),x) \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 C\mathbf C endows Lens(C)\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 C=Set\mathbf{C} = Set. Then every lens L=(S,V,get,put)L = (S, V, \mathrm{get}, \mathrm{put}) is equivalent a “constant complement” lens whose Get is a product projection π 1:C×VV\pi_{1} : C \times V \to V and whose Put is the function π 0,2:C×V×VC×V\pi_{0,2} : C \times V \times V \to C \times V for some set CC.

Proposition

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

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

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.

Lenses with laws

References

Journal papers, conference proceedings, and preprints

Blog posts, talk slides, and other material