The Reader and Writer Monads and Comonads

The Reader and Writer monad are well known, but I would like to present their comonadic counterpart.

Monads

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:

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.

Comonads

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