lens (in computer science)



In computer science, originally in database theory?, lenses are used in 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).


Let CC be a category with finite products. A lens in C denoted L=(S,V,g,p)L =(S,V,g,p) has states SS and view states VV which are objects of CC, and two arrows of C, a Get arrow g:SVg:S \to V and a Put arrow p:V×SSp: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: gp=π 0g p= \pi_0.
  2. (GetPut) the Put for a trivially updated state is trivial: pg,1 S=1 Sp \langle g, 1_S \rangle = 1_S.
  3. (PutPut) composing Puts does not depend on the first view update: p(1 V×p)=pπ 0,2p(1_V \times p) = p \pi_{0,2}.

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

In other words, a (lawful) lens for a fixed VV is an algebra from the monad V *ΣV^{\ast} \cdot \Sigma (the possibility operator):

C/VV *ΣC. C/V \underoverset {\underset{V^{\ast}}{\longleftarrow}} {\overset{\Sigma}{\longrightarrow}} {\bot} C.

They are also coalgebras for the store comonad.


Many kinds of generalization have been proposed - asymmetric lenses, bimorphic lens, etc.

One generalization considers the lenses from the previous section as monomorphic by contrast to polymorphic lens which go between pairs of types, λ:(S,T)(A,B)\lambda: (S, T) \to (A, B), consisting of a view function, v λ:SAv_{\lambda}: S \to A, and an update function u λ:S×BTu_{\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 defines a symmetric monoidal functor from SymmMonCat to itself. Evaluating the result for different symmetric monoidal categories gives these various generalizations such as Prisms which use the disjoint union in Set. (Riley Theorem 2.0.8)


Last revised on January 27, 2021 at 06:28:26. See the history of this page for a list of all contributions to it.