The `Reader`

and `Writer`

monad are well known, but I would like to present their comonadic counterpart.

I will use the following definition of a monad:

```
class Monad m where
return :: a -> m a
(=<<) :: (a -> m b) -> m a -> m b
```

There is no way to understand monads besides using them, and in particular the `Maybe`

, `List`

, and `State`

monads.
Nevertheless, the intuition I get about monads is that:

It's easy to get in, hard to get out, and despite this, one can lift a function using `=<<`

.

What I mean is: suppose that it were easy to “get out” of a monad, i.e., suppose there is a function `getout`

of type `m a -> a`

.
Then the bind `(=<<)`

would be trivial: `f =<< x = f (getout x)`

.
So the strength of the bind operation is that it exists *despite* it being difficult to get out of a monad.

Now, the `Reader`

type constructor is defined (informally) as `Reader s = (->) s`

.
The proof that it is a monad is the following:

```
instance Monad ((->) s) where
return = const
f =<< r = \ s -> (f . r) s s
```

The intuition behind the `Reader`

monad, for a mathematician, is perhaps **stochastic variables**.
A stochastic variable is a function from a probability space to some other space.
So we see a stochastic variable as a monadic value.
Getting *in* is easy: from an ordinary value, produce a *deterministic* stochastic variable.
This is exactly what `return`

does.
The bind operation works as it would for stochastic variables as well.

Now to the `Writer`

monad.
First, the `Writer`

type constructor is (informally) defined as `Writer s x = (s,x)`

.
It is well known that *if the state type s is a monoid*, then `Writer`

is a monad:

```
instance (Monoid s) => Monad ((,) s) where
return x = (mempty, x)
f =<< (s,x) = (t <> s, y)
where (t,y) = f x
```

The idea behind the `Writer`

monad is that it is a **value carrying some logging message**, for instance.
The log messages accumulate along with function composition.
You also see that to “get in”, we need a special log message, in that case an “empty” message, thanks to the monoid property of the state type.

Now to the comonads!

The *comonad* class is defined as follows:

```
class CoMonad m where
extract :: m a -> a
(<<=) :: (m a -> b) -> m a -> m b
```

It's a bizarro monad!
Now, it's easy to get *out* of a comonad, but hard to get in.
And similarly, although it's hard to get in, one can still lift function using the `<<=`

operator.

Here is the first surprise: *without any assumption on the state type*, the `Writer`

is a comonad!
Here is the implementation:

```
instance CoMonad ((,) s) where
extract = snd
f <<= w@((s,_)) = (s, f w)
```

The intuition is that it represents a sort of **hidden state**.
The `extract`

function *observes* only a part of the whole state.
Function binding simply passes the hidden state along.

Finally, there is also a * Reader comonad*, but only if the state type is a monoid!
Here is the implementation:

```
instance (Monoid s) => CoMonad ((->) s) where
extract = ($ mempty)
f <<= r = \ t -> (f . shift t) r
where shift t rr = \ s -> rr (s <> t)
```

What is the intuition behind this?
Well, imagine that the monoid is the natural number.
A monadic value is then a *stream*.
The `Reader`

comonad is thus a **generalisation of the stream comonad**.

There must be some reason why there is such a symmetry between the `Reader`

and `Writer`

type constructors.
The reason must be related to the Currying isomorphism $\mathrm{Hom}(X\times S, Y) = \mathrm{Hom}(X,Y^S)$, but I don't currently have all the details.
There are some ideas in this SO answer.

In the future, I would also like to add *proofs*, in Idris, that these implementations actually fulfill the Monad and Comonad laws.
But that's enough for today!

**Edit** I see now that what I called the `Reader`

comonad (or `Stream`

) is called `Traced`

, and that the `Writer`

comonad is called `Env`

.
I was not aware that the monads and comonads described in this blog post were in fact already on p. 6 of those slides by David Overton.