nLab lens (in computer science)

Redirected from "lawful lenses".
Contents

Contents

Idea

In computer science, originally in database theory, a data structure-type now called (lawful) lenses [Bohannon, Pierce & Vaughan (2006, §3), Foster, Greenwald, Moore, Pierce & Schmitt (2007, §3), but considered under different names already by Oles 1982, 1986 and Hofmann & Pierce 1996] is used to encode data(-base) types SS equipped with a read/write functionality (only) for a specified view-type VV.

In particular, “very well-behaved” or “lawful” lenses (see Def. below) – those for which updates of the “view” VV completely overwrite any previous such changes – turn out to equivalently be data base types of product form S=D×VS = D \times V with “view” given by projecting onto the VV-factor. As such, lawful lenses are equivalent to (cf. monads in computer science):

Thus, lawful lenses may be thought of as encoding read/write functionality (only) at a certain address in a data base (compare the RAM-model given by the state monad which encodes read/write of the entire data base type at once).

More generally, there are two different approaches to lenses:

  • Lawful lenses (as above) 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).

Definition

Definition

(lenses)
Given a category (C,1,×)(\mathbf{C}, 1, \times) with finite products, a lens in C\mathbf{C} is:

  1. a pair of objects of C\mathbf{C}

    1. (“source”)

      SCS \,\in\, \mathbf{C}
    2. (“view”)

      VCV \,\in\, \mathbf{C}
  2. a pair of morphisms of the form

    1. (“view”, “read-out”, “forward operation”)

      get:SV \mathrm{get} \;\colon\; S \longrightarrow V
    2. (“update”, “write”, “backward operation”)

      put:V×SS. \mathrm{put} \;\colon\; V \times S \longrightarrow S \,.

The lens is called well-behaved if this data satisfies:

  • (PutGet) “what has just been written is read out as such”:

    v:V,s:Sget(put(v,s))=v, v \colon V ,\, s \colon S \;\;\;\;\;\; \vdash \;\;\;\;\;\; get\big( put (v,\,s) \big) \;=\; v \,,

and

  • (GetPut) “writing what has just been read out means no change”:

    s:Sput(get(s),s)=s s \colon S \;\;\;\;\;\; \vdash \;\;\;\;\;\; put\big( get(s) ,\, s \big) \;=\; s

and it is called very well-behaved or lawful if in addition it satisfies:

  • (PutPut) “writing means to over-write previous edits”:

    v,v:V,s:Sput(v,put(v,s))=put(v,s) v,\,v' \colon V ,\; s \colon S \;\;\;\;\;\; \vdash \;\;\;\;\;\; put\Big( v',\, put\big( v,\, s \big) \Big) \;=\; put(v',\, s)

Definition appears, under no particular name, in Hofmann & Pierce 1996, p. 12, where it is thought of as providing aspects of object-oriented programming: Here one thinks of SS as a “class” which inherits functionality from the class VV. And indeed, for lawful lenses it follows (see below) that SD×VS \simeq D \times V is a “record” which inherits all fields present in VV but may add some more).

The terminology “lens” for Def. is due to Bohannon, Pierce & Vaughan 2006, Def. 3.2.

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 2get 1 \mathrm{get}_{12} = \mathrm{get}_2 \circ \mathrm{get}_1
put 12=put 1((put 2(1 Z×get 1))×1 X)(1 Z×Δ X) \mathrm{put}_{12} = \mathrm{put}_1 \circ ((\mathrm{put}_2 \circ (1_Z \times \mathrm{get}_1)) \times 1_X) \circ (1_Z \times \Delta_X)

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

Monadicity over Possibility monad

Proposition

(lawful lenses are possibility modales)
Lawful lenses in C\mathbf{C} with view VV (Def. ) are equivalently the modules (modales) of the left base change monad on the slice category over VV (the VV-possibility-modality V\lozenge_V):

(1)

where

  1. view:SVview \,\colon\, S \to V is identified with the slicing morphism,

  2. get:V×SSget \,\colon\, V \times S \to S is identified with the module action V(S)S\lozenge_V(S) \to S.

(Johnson, Rosebrugh & Wood 2010, Prop. 9)
Proof

By direct unwinding of the definitions:

Proposition

If the ambient category C\mathbf{C} is a topos (such as Sets) and the view VV is inhabited, then the adjunction (1) is monadic.

For the case C=Sets\mathbf{C} = Sets this is Johnson, Rosebrugh & Wood 2010, Thm. 12, Cor. 13.
Proof

The monadicity theorem (here) readily gives that the above adjunction (1) is monadic functor: (-)×V(\text{-})\times V preserves all colimits (cf. universal colimits) hence in particular the relevant coequalizers, and it is conservative by the assumption that VV is inhabited (this is clear by inspection in Sets – which is what JRW10 observe on their p. 13 – for the general case use Johnstone 2002, vol 1, Lem. 1.3.2).

Remark

(relation to monadic descent)
In (algebraic) geometry, the statement of Prop. is known as monadic descent. In this context one would say that:

and so the monadicity theorem C(C /V) V\mathbf{C} \,\simeq\, \big(\mathbf{C}_{/V}\big)^{\lozenge_V} in Prop. states that objects over VV which are equipped with such descent data are equivalent to objects over *\ast, hence “do descend” along V*V \to \ast.

Remark

(relation to epistemic logic)
Prop. says that the category of V\lozenge_V-modales among objects in C /V\mathbf{C}_{/V} is equivalent to C\mathbf{C}. This makes good sense when viewing V\lozenge_V as the possibility-modality, see the discussion of potentiality there.

Monadicity over the CoState comonad

Alternatively:

Proposition

(lawful lenses are the costate coalgebras)

For C\mathbf{C} a cartesian closed category, the lawful VV-lenses in C\mathbf{C} (Def. ) are equivalently the coalgebras of the VV-CoState comonad, i.e. that induced by the internal hom-adjunction:

This is due to O’Connor (2010), O’Connor (2011), for further discussion see Gibbons & Johnson (2012), Section 3.2.

A proof is spelled out here at store comonad.

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, λ:(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.

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.

  • 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 SS and VV called the source and view, together with a Get functor g:SVg : S \to V and a function φ:S 0× V 0V 1S 1\varphi \colon S_{0} \times_{V_{0}} V_{1} \to S_{1} which takes a pair (sS,u:gsvV)(s \in S, u : g s \to v \in V) to a morphism

    φ(s,u):sp(s,u)\varphi(s, u) : s \to p(s, u) in SS where p(s,u)=cod(φ(a,u))p(s, u) = cod(\varphi(a, u)) is the Put function. The function φ\varphi must also satisfy three lens laws. When SS and VV 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.

References

General

The definition of what are now called (lawful) lenses is already in

but gained wider attention only with:

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

Further discussion:

Relation to the costate comonad

The observation that lenses are equivalently nothing but the coalgebras of the costate comonad (cf. monads in computer science) is due to:

Early review:

Further details:

Further review:

Relation to produoidal categories

  • Craig Pastro?, Ross Street, Doubles for monoidal categories (2007)

Blog posts, talk slides, and other material

Last revised on March 23, 2024 at 10:43:04. See the history of this page for a list of all contributions to it.