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.