In a previous post I claimed that *comonad structures on R -> a are in one-to-one correspondence with monoid structures on R*. In this post and the next I'll justify that claim.

## Characterizing comonads on `R -> a`

Suppose we have a comonad structure on `R -> a`

. What could it possibly look like? Well, we must have two functions

```
extract :: (R -> a) -> a
duplicate :: (R -> a) -> (R -> (R -> a))
```

(these are the duals of `return`

and `join`

for monads). Furthermore, `extract`

and `duplicate`

must satisfy some laws; we'll get to those in a minute. For now, let's just think a bit about these functions and their implementations. How would you implement them? They seem awfully constrained. For example, look at the type of `extract`

: it takes a function of type `R -> a`

and must somehow return an `a`

. Intuitively, the only way it could do this is by applying the function to some distinguished value of type `R`

. Similarly, `duplicate`

takes a function `R -> a`

as input and must produce a function of type `R -> R -> a`

. How could this output function behave? It takes two `R`

values and then must produce an `a`

. The only place to get an `a`

is from the argument to `duplicate`

, which must be passed an `R`

; the only possibility is to somehow combine its two `R`

values into one.

Hmm... a distinguished value of type `R`

... combining two `R`

values into one... this should sound familiar! But how do we formalize all of this?

Any time we talk about the way a function's *type* constrains its *behavior* we should immediately think of *parametricity* (aka *free theorems*). Using the very nice free theorem generator (using `T0`

in place of `R`

) we can automatically generate some theorems about `extract`

and `duplicate`

based on their types. I've taken the liberty of specializing and alpha-varying them a bit. First, here's the free theorem for `extract`

:

Now watch what happens when we set `q = g`

and `p = id`

(so `a = R`

). The left-hand side of the implication becomes `g . id = g`

which is trivially satisfied. Hence the right-hand side must hold:

What does this give us? Well, flipping it around, it tells us that applying `extract`

to an arbitrary function `g`

is equivalent to applying `g`

to some value of type `R`

(in particular, the value we get when applying `extract`

to the identity function). In other words, up to behavioral equivalence, the only possible implementation of `extract g`

is the one which applies `g`

to some distinguished `R`

value -- which is exactly what our intuition told us before! `extract`

is completely determined by the chosen value of `R`

; let's call it `r`

.

Similarly, here's the free theorem for `duplicate`

:

Again setting `q = g`

and `p = id`

gives us

Writing for gives us

that is, the only possible implementation of `duplicate g y z`

is to pass some combination of `y`

and `z`

as an argument to `g`

.

So now we know that for some value and some binary function ,

But in order to form a valid comonad instance, these functions must satisfy a few laws. In another post, I'll show what these laws tell us about and (you can probably already guess, and might want to try working out the proof yourself... =)

Very sweet!

Your R->a is Cowriter R a, see my post. In short:

0) the functor (,) transports Monoid R to the monad Writer R;

1) the adjunction between the functors (,) R -| (R->) transports Writer R to Cowriter R (see the accepted answer for my post).

This can be concisely proved in category theory. No Haskell. :o)