The object of this post is to provide a simple example of the use of comonads in Haskell. Much of this post is a rehash of this
awesome paper by Richard B. Kieburtz.
It just so happens that the definition of Comonad is available from hackage. Simply do '
cabal install comonad'. I must admit that typing this command feels kind of funny.
Now we can
> import Control.Comonad
Okay, let's define what a stream is:
> data Stream a = forall b. S b (b -> a) (b -> b)
> current (S x f g) = f x
> rest (S x f g) = S (g x) f g
A stream of a's consists of a current position x, a function f to get some value from the current position, and a function g to transition from the current position to the rest of the stream.
Note, to make this definition,
-XExistentialQuantification must be passed to
ghci or
ghc. Why? Because of the forall b part of the definition of Stream. This allows us to use any type b as a "carrier" or "container" for the underlying implementation of a stream.
Here is the stream of integers corresponding to the Fibonacci sequence:
> fibstream = S (1,1) fst (\(j,k) -> (k, j + k))
In this case, our "carrier" is an iterated 2-tuple. But we don't really need to know that. I shall now pause to ask ghci for some Fibonacci numbers:
*Main> current fibstream
1
*Main> current (rest fibstream)
1
*Main> current (rest (rest fibstream))
2
*Main> current (rest (rest (rest fibstream)))
3
*Main> current (rest (rest (rest (rest fibstream))))
5
*Main> current (rest (rest (rest (rest (rest fibstream)))))
8
Hooray!
Of course, the astute category theorist should recognize that Stream is a functor on the category of Haskell types.
> instance Functor Stream where
> fmap f = \s -> S s (f . current) rest
That is, given an
f that goes from a's to b's, we can make
(fmap f) that goes from a Stream of a's to a Stream of b's.
Note that in category theory, if $F$ is a functor from a category $\mathcal{C}$ to another category $\mathcal{D}$, then we use $F$ to refer to both the object and morphism mappings of $F$. For instance, we blithely refer to $F(X)$ and $F(f)$ where $X$ is an object and $f$ is a morphism.
For our Stream functor in Haskell, the type constructor Stream refers to the object component of the functor and fmap refers to the morphism component.
How about an example of this functor in action?
> square x = x * x
> fibsquares = (fmap square) fibstream
fibsquares ought to be a stream consisting of the squares of the Fibonacci numbers. Let's ask
ghci:
*Main> current fibsquares
1
*Main> current (rest fibsquares)
1
*Main> current (rest (rest fibsquares))
4
*Main> current (rest (rest (rest fibsquares)))
9
*Main> current (rest (rest (rest (rest fibsquares))))
25
*Main> current (rest (rest (rest (rest (rest fibsquares)))))
64
We now have a functor called
Stream, a member
fibstream of the type
Stream Integer, and a function
(fmap square) from
Stream Integer to
Stream Integer, which is the image of the function
square from
Integer to
Integer.
What about this comonad business?
Recall that a comonad $G$ on a category $\mathcal{C}$ consists of a functor $G : \mathcal{C} \rightarrow \mathcal{C}$ together with natural transformations $\Delta: G \rightarrow G^2$ and $\epsilon : G \rightarrow 1$ satisying "the appropriate diagrams", namely, that $\Delta$ is coassociative and $\epsilon$ is a counit for $\Delta$.
Well, as you might have predicted, I claim that the functor
Stream, as defined above, is a comonad. The counit is already defined above as current. I'm going to call $\Delta$ something more descriptive:
> dupstream s = S s id rest
(id is the identity function)
This turns
(Stream a) into
(Stream (Stream a)). By construction, this is a natural transformation (always be suspicious when you read something like this). Shall we verify coassociativity?
> f1 = dupstream (dupstream fibstream)
> f2 = (fmap dupstream) (dupstream fibstream)
In f1, we duplicate the duplicated stream. In f2, we duplicate the stream "encapsulated" by the duplicated stream. I hope that makes sense. Both are of type (Stream (Stream (Stream Integer))). If Stream is really a comonad, f1 ought to be equal to f2.
Well, ghci?
*Main> current (current (current f1))
1
*Main> current (current (current f2))
1
That's not a proof, but rather encouraging.
> instance Comonad Stream where
> extract = current
> duplicate = dupstream
In the Comonad specification, the counit is denoted by "extract" and the comultiplication is denoted by "duplicate". These names are more descriptive than $\epsilon$ or $\Delta$.
Now that we have a comonad, the natural question that a mathematician would ask is, "What are the coalgebras over this comonad?". Recall that given a comonad $G$, a coalgebra over $G$ consists of an object $X$ together with a morphism $\psi: X \rightarrow G(X)$ such that $\Delta_{X} \circ \psi = G(\psi) \circ \psi$. That is, an object $X$ equipped with a comultiplication that is compatible with the comultiplication on $G$. A morphism of coalgebras is a map $f: X \rightarrow Y$ in $\mathcal{C}$ such that $G(f) \circ \psi_{X} = \psi_{Y} \circ f$ (here, I use a subscript to denote respective coalgebra structures).
Given a comonad $G$, we get an entire category of coalgrbas for free. This is the Kleisli category $\mathcal{C}^G$, which consists of all cofree coalgebras.
A cofree coalgebra over $G$ is of the form $\Delta_{X} : G(X) \rightarrow G(G(X))$. It follows that a morphism between cofree coalgebras is a map $f: G(X) \rightarrow G(Y)$ compatible with $\Delta$. Recall that there is a counit $\epsilon_{Y} : G(Y) \rightarrow Y$. Hence, given such an $f$, there is $\epsilon_{Y} \circ f : G(X) \rightarrow Y$.
In fact, all maps in to a cofree coalgebra are lifts of maps to the underlying object. Let's illustrate this with an example.
> smudge s = (current s) + (current (rest s)) + (current (rest (rest s)))
smudge takes a Stream s and adds the first three elements. As we've defined it, is a map from
(Stream a) to
a, where a is a type that
+ works on, namely of the type class
Num.
Observe:
*Main> smudge fibstream
4
For the sake of simplicity, let's consider
smudge a morphism from
(Stream Integer) to
Integer. It ought to life to a morphism from
(Stream Integer) to
(Stream Integer) that is compatible with the cofree coalgebra structure on
(Stream Integer), namely,
duplicate.
How do we lift smudge? Applying
fmap to
smudge will produce a morphism from
(Stream (Stream Integer)) to
(Stream Integer). We can then precompose this with duplicate to obtain a map
(Stream Integer) to
(Stream Integer).
> streamsmudge = (fmap smudge) . duplicate
*Main> :type streamsmudge fibstream
streamsmudge fibstream :: Stream Integer
*Main> current (streamsmudge fibstream)
4
*Main> current (rest (streamsmudge fibstream))
6
In fact, the above lift can be done with any morphism like smudge.
Control.Comonad defines
> extend f = (fmap f) . duplicate
and in this context,
streamsmudge is just
(extend smudge).
What we've done is somewhat trivial. Given a way to smudge the first few elements of a stream, we can create a stream of these smudges. That's what cofree-ness means in this context.
I personally think that this is neat, because concepts like coalgebras and cofreeness can be tricky to understand. Algebras and free things usually easier to grasp in mathematics. The co prefix makes the brain twist around.
