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

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

Thus 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

Thus 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

Thus fmap extract . duplicate = id.

duplicate (duplicate (Store p x))
= ... -- Fill in later (AKA, exercise left to reader)
= fmap duplicate (duplicate (Store p x))

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