blog

I came across the idea to use \(F\)-(co)algebras to encode general constructors and destructors when reading Martin Erwig's paper on synchromorphisms.

Once I had mocked out code, they looked pretty familiar. Sure enough, the type signature of a lens suspiciously resembles that of an \(F\)-coalgebra. Curiouser still, both indexed data types (a generalization of algebraic data types) and lenses can give indexed access to data structures.

Consider a lens in Haskell.

Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t

This doesn't quite work. \(F\)-coalgebras must be arrows \(A\rightarrow F(A)\). We instead expand the more familiar Lens', viz.

type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s

So we get a mapping of \(F\)-coalgebras for every endofunctor \(F\). This gives a crucial insight - a lens is a collection of mappings between destructors (i.e. field accessors).

But we can go further. We would like a mapping between \(F\)-coalgebras to be homomorphism, and moreover we would like the homomorphism laws for \(F\)-coalgebras to correspond to the already established lens laws, viz.

view l (set l v s)   = v
set l (view l s) s   = s
set l v' (set l v s) = set l v' s

The definition of an \(F\)-coalgebra homomorphism requires all arrows \(f:A\rightarrow B\) satisfy \(F(f)\circ \alpha = \beta \circ f\), where \((A, \alpha)\), \((B, \beta)\) are the \(F\)-coalgebras in question.

Thus, for lens to be a \(F\)-coalgebra homomorphism, we must have the following:

fmap g . coalgebra = (lens coalgebra) . g

We specialize the types of view and set for better focus:

view :: (forall f. Functor f => (a -> f a) -> s -> f s) -> s -> a
set :: (forall f. Functor f => (a -> f a) -> s -> f s) -> a -> s -> s

We can define our own versions of view and set in order to make things clearer.

set :: Lens' s a -> a -> s -> s
set lens x = runIdentity . lens (Identity . const x)
view :: Lens' s a -> s -> a
view lens = (getConst . lens Const)

Here, the \(F\)-coalgebras are Const and Identity. Let's expand the first lens law with the assumption the lens always maps coalgebras via homomorphism. We assume further that the lens points to a value of the same type, so that the function id will always have the appropriate type, and so that (Identity . const v) is a coalgebra when applied to s.

view l (set l v s) = v
view l ((runIdentity . l (Identity . const v)) s) = v
view l ((runIdentity . fmap id . (Identity . const v)) s) = v
(getConst . l Const) ((runIdentity . fmap id . (Identity . const v)) s) = v
(getConst . fmap id . Const) ((runIdentity . fmap id . (Identity . const v)) s) = v
v = v

We can use the same technique to yield a proof of the second lens law as well.

set l (view l s) s = s
set l ((getConst . lens Const) s) s = s
set l ((getConst . fmap id . Const) s) s = s
(runIdentity . l (Identity . const ((getConst . fmap id . Const)  s))) s = s
(runIdentity . fmap id . (Identity . const ((getConst . fmap id . Const) s))) s = s
s = s

This is a weaker result than we would like. For one, it only applies to the more common sorts of lenses; more perniciously, it only works when the lens accesses a value of the same type.

But it can nonetheless be insightful. We have shown that in such cases the lens laws follow from the condition that the lens is a family of homomorphisms.

Moreover, we have given a connection between Erwig's paper (which uses \(F\)-(co)algebras to generalize algebraic data types) and Haskell's polished lens library. This is a convincing argument that lenses are indeed the right choice for record updates, coalgebra homomorphisms being the "natural" way to generalize and manipulate destructors.