Lenses are the coalgebras for the costate comonad

I took part in the Dagstuhl Seminar on Bidirectional Transformations “BX” earlier this month. It was a meeting of people from four communities—databases, graph transformations, programming languages, and software engineering—discussing their various perspectives—namely the view–update problem in databases, triple graph grammars, lenses, and model synchronization—on the common problem of “BX”.

While there, I reported on a marvellous observation made by Russell O’Connor, that lenses are exactly the coalgebras for the costate comonad. That is, the independently identified notion of a “very well-behaved lens” in the work of Pierce and others coincides exactly with the categorical notion of a “coalgebra” for a particular comonad, the “costate” comonad. I’ll unpack that claim here.

Lenses

Pierce’s lenses are pairs of functions between “source” and “view” datatypes ${S}$ and ${V}$ : a “get” function ${g : S \rightarrow V}$ and a “put” function ${p : S \times V \rightarrow S}$ . The story is that the view is some projection of the data in the source—perhaps a subset of the data, or the data in a simpler format—and so in order to update the source given a modified view, one needs also a copy of the original source from which to reconstruct the missing information.

For these two functions to capture a “well-behaved” lens, they should satisfy the so-called Get–Put and Put–Get laws:

$\displaystyle \begin{array}{lcl} p\,(s,g\,s) &=& s \\ g\,(p\,(s,v)) &=& v \end{array}$

The Get–Put law says that if you “get” a view of the source, and then “put” it straight back without modifying it, the source remains unmodified: a no-op edit on the view translates into a no-op on the source. The Put–Get law says that if you “put” any view into a source and then “get” it back, you end up with the view you first thought of: nothing is lost from the view when it is put back.

Additionally, for these two functions to capture a “very well-behaved” lens, they must satisfy a third law, the Put–Put law:

$\displaystyle \begin{array}{lcl} p\,(p\,(s,v),u) &=& p\,(s,u) \end{array}$

In words, “put”ting back two views ${v}$ then ${u}$ is equivalent to “put”ting back just the second; any changes to the source from putting back ${v}$ are completely overwritten when putting back ${u}$ . (This turns out to be rather a strong condition, requiring that the source basically factors into the view and a completely independent “complement”; few real applications of bidirectional transformation satisfy it. But that’s another story.)

The costate comonad

Intuitively, comonads capture “data in context”. A comonad ${(D,\mathit{extr},\mathit{dupl})}$ consists of a functor ${D}$ together with two natural transformations ${\mathit{extr} : D \rightarrow 1}$ and ${\mathit{dupl} : D \rightarrow DD}$ that extract the data from its context and duplicate the context, satisfying the three axioms:

$\displaystyle \begin{array}{lcl} \mathit{extr} \cdot \mathit{dupl} &=& \mathit{id} \\ \mathit{fmap}\,\mathit{extr} \cdot \mathit{dupl} &=& \mathit{id} \\ \mathit{fmap}\,\mathit{dupl} \cdot \mathit{dupl} &=& \mathit{dupl} \cdot \mathit{dupl} \end{array}$

One example of a comonad is the “costate” construction: for fixed ${V}$ , define functor ${D}$ by

$\displaystyle \begin{array}{lcl} D\,A &=& V \times (V \rightarrow A) \end{array}$

so that the “map” function for ${D}$ satisfies ${\mathit{fmap}\,h\,(v,f) = (v, h \cdot f)}$ . The operations are given by

$\displaystyle \begin{array}{lcl} \mathit{extr}\,(v,f) &=& f\,v \\ \mathit{dupl}\,(v,f) &=& (v, \lambda u \rightarrow (u,f)) \end{array}$

Verifying that these definitions satisfy the comonad axioms is left as an exercise for the interested reader.

(Incidentally, I think it’s called the “costate” comonad more because it is the dual ${(V\times)\cdot(V\rightarrow)}$ of the “state” monad ${(V\rightarrow)\cdot(V\times)}$ , rather than because it has anything to do with stateful computations. However, it does model state in the sense of stored variables; and indeed, Russell O’Connor’s blog posting calls ${D}$ the “store” comonad.)

Coalgebras of a comonad

For a functor ${F}$ , an ${F}$ -coalgebra is a pair ${(A,f)}$ of a type ${A}$ and a function ${f : A \rightarrow F\,A}$ . A “coalgebra for a comonad ${D}$ ” is a ${D}$ -coalgebra that interacts well with the operations ${\mathit{extr}}$ and ${\mathit{dupl}}$ of the comonad; that is, the function ${f}$ should also satisfy the laws:

$\displaystyle \begin{array}{lcl} \mathit{extr} \cdot f &=& \mathit{id} \\ \mathit{dupl} \cdot f &=& \mathit{fmap}\,f \cdot f \end{array}$

(Another incidentally: I don’t have a feeling for what these laws mean, in the way that I do for the laws of an algebra of a monad. At least for the free monads ${T}$ that represent terms with free variables, an algebra is a pair ${(A, f : T\,A \rightarrow A)}$ such that ${f}$ makes sense as an “expression evaluator”—it respects singleton variables and substitution. It’s clear to me that the laws of a coalgebra for a comonad are the obvious duals of those for the algebra of a monad; and that they describe the interesting ways of putting together the coalgebra operation with the comonad operations; but I still don’t have a direct intuition. Any comments gratefully received!)

Lenses are coalgebras of the costate comonad

Now it’s just a matter of putting the pieces together. Curry the “put” function of a lens to obtain ${p : S \rightarrow (V \rightarrow S)}$ , and define a lens to be the fork of the “get” and “put” functions:

$\displaystyle \begin{array}{lcl} \ell\,s &=& (g\,s, p\,s) \end{array}$

Note that now ${\ell : S \rightarrow D\,S}$ where ${D}$ is the costate comonad. The Get–Put law is equivalent to the counit axiom of the coalgebra:

$\displaystyle \begin{array}{ll} & \mathit{extr} \cdot \ell = \mathit{id} \\ \Leftrightarrow & \qquad \{ \mbox{apply to an~} s \} \\ & \mathit{extr}\,(\ell\,s) = s \\ \Leftrightarrow & \qquad \{ \ell \} \\ & \mathit{extr}\,(g\,s, p\,s) = s \\ \Leftrightarrow & \qquad \{ \mathit{extr} \} \\ & p\,s\,(g\,s) = s \end{array}$

And the Put–Get and Put–Put laws together are equivalent to the coassociativity axiom:

$\displaystyle \begin{array}{ll} & \mathit{dupl} \cdot \ell = \mathit{fmap}\,\ell \cdot \ell \\ \Leftrightarrow & \qquad \{ \mbox{apply to an~} s \} \\ & \mathit{dupl}\,(\ell\,s) = \mathit{fmap}\,\ell\,(\ell\,s) \\ \Leftrightarrow & \qquad \{ \ell \} \\ & \mathit{dupl}\,(g\,s, p\,s) = \mathit{fmap}\,\ell\,(g\,s, p\,s) \\ \Leftrightarrow & \qquad \{ \mathit{fmap} \mbox{~for~} D \} \\ & \mathit{dupl}\,(g\,s, p\,s) = (g\,s, \ell \cdot p\,s) \\ \Leftrightarrow & \qquad \{ \mathit{dupl} \} \\ & (g\,s, \lambda v \rightarrow (v, p\,s)) = (g\,s, \ell \cdot p\,s) \\ \Leftrightarrow & \qquad \{ \mbox{first components are clearly equal} \} \\ & \lambda v \rightarrow (v, p\,s) = \ell \cdot p\,s \\ \Leftrightarrow & \qquad \{ \mbox{apply to a~} v \} \\ & (v, p\,s) = \ell\,(p\,s\,v) \\ \Leftrightarrow & \qquad \{ \ell \} \\ & (v, p\,s) = (g\,(p\,s\,v), p\,(p\,s\,v)) \\ \Leftrightarrow & \qquad \{ \mbox{apply second components to a~} u \} \\ & (v, p\,s\,u) = (g\,(p\,s\,v), p\,(p\,s\,v)\,u) \\ \Leftrightarrow & \qquad \{ \mbox{pair equality is pointwise} \} \\ & v = g\,(p\,s\,v) \land p\,s\,u = p\,(p\,s\,v)\,u \end{array}$