Themes on Streams, Part II
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:
\(\forall g :: a \to b, \forall p :: R \to a, \forall q :: R \to b, \\ \quad (g \circ p = q) \implies (g\ (\mathit{extract}\ p) = \mathit{extract}\ q)\)
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:
\(g\ (\mathit{extract}\ id) = \mathit{extract}\ g\)
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:
\(\forall g :: a \to b, \forall p :: R \to a, \forall q :: R \to b, (g \circ p = q) \implies \\ \quad (\forall y,z :: R, g\ (\mathit{duplicate}\ p\ y\ z) = \mathit{duplicate}\ q\ y\ z)\)
Again setting q = g and p = id gives us
\(g\ (\mathit{duplicate}\ \mathit{id}\ y\ z) = \mathit{duplicate}\ g\ y\ z\)
Writing \(\oplus\) for \(\mathit{duplicate}\ \mathit{id}\) gives us
\(\mathit{duplicate}\ g\ y\ z = g\ (y \oplus z)\)
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 \(r :: R\) and some binary function \(\oplus :: R \to R \to R\),
\(\mathit{extract}\ g = g\ r \\ \mathit{duplicate}\ g\ y\ z = g\ (y \oplus z)\)
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 \(r\) and \(\oplus\) (you can probably already guess, and might want to try working out the proof yourself… =)