Every now and then you hear that lenses are actually just “costate comonad coalgebras”.
data State s a = State (s -> (a, s))
The State monad we all know and love. Given a state
s, produce a value
a and a new
data Store s a = Store (s -> a) s
The Store type, which is dual to State. It’s sometimes called CoState. The idea of this type is that we take a “piece” out of our
a value of type
s. We also give a way to insert the
s back into
a, making it whole again.
instance Functor (Store s) where fmap f (Store p x) = Store (f . p) x
If we have a way to turn an
a into a
b, then we can essentially consider the
s to be a piece of
b as well.
fmap id (Store p x) = Store (id . p) x = Store p x
fmap id = id, making sure that
Store s is actually a Functor. The second Functor law is redundant, so we don’t have to prove it.
instance Comonad (Store s) where extract (Store p x) = p x duplicate (Store p x) = Store p' x where p' s = Store p s
To extract the whole value of the Store, simply apply the piece to the builder. To duplicate it, we construct a modified Store to return a
Store s a when it becomes whole again. Since
s is arbitrary, our only choice is to just use the one we’ve given. Our building function has to construct a Store, so we just pass it the
s we’re given and use the builder from the original Store.
extract (duplicate (Store p x)) = extract (Store (\s -> Store p s) x) = (\s -> Store p s) x = Store p x
extract . duplicate = id.
fmap extract (duplicate (Store p x)) = fmap extract (Store (\s -> Store p s) x) = Store (\s -> extract (Store p s)) x = Store (\s -> p s) x = Store p x
fmap extract . duplicate = id.
duplicate (duplicate (Store p x)) = ... -- Fill in later (AKA, exercise left to reader) = fmap duplicate (duplicate (Store p x))
duplicate . duplicate = fmap duplicate . duplicate, and we have shown that
Store s satisfies all of the Comonad laws.
type Coalgebra f a = a -> f a
For a given Functor
f and type
a, a map
a -> f a is known as an F-coalgebra. If the Functor is a Comonad and the map preserves the comonadic structure, then this is known as a comonad coalgebra.
type Lens s a = Coalgebra (Store s) a = a -> Store s a = a -> (s -> a, s)
So there you have it: a Lens gives us a way to take a value and form a Store out of it. For a more detailed look, see Relating Algebraic and Coalgebraic Descriptions of Lenses by Jeremy Gibbons and Michael Johnson.