Themes on Streams
> {-# LANGUAGE DeriveFunctor, FlexibleInstances #-}
Recall that a stream is a countably infinite sequence of values:
> data Stream a = a :> Stream a
> deriving (Functor, Show)
>
> sHead (a :> _) = a
> sTail (_ :> s) = s
Streams are lovely things (especially in a lazy language) with many nice properties.
> type Theme = String
> type Consciousness = Stream Theme
The remainder of this blog post (in two parts) will be of type Consciousness
.
Theme 1: Stream
is a monad
The other day I read Jeremy Gibbons’s blog post about the stream monad, proving the monad laws for the version of join
that diagonalizes nested streams:
> instance Monad Stream where
> return a = a :> return a
> s >>= f = sJoin (fmap f s)
>
> sJoin (s :> ss) = sHead s :> sJoin (fmap sTail ss)
sJoin
takes a stream of streams, and outputs a stream with the first element of the first stream, the second element of the second stream, … the nth element of the nth stream.
I recommend reading his post, it’s a very cool example of using universal properties and equational reasoning.
Theme 2: Stream
s are (isomorphic to) functions
In a comment on Jeremy’s post, Patai Gergely noted that insight into this issue can be gained by observing that Stream a
is isomorphic to Nat -> a
: there is one item in a stream at every natural number index.
Of course, (->) Nat
is a monad: in fact, (->) e
is a monad (the "reader monad") for any type e
. And what does join
for the (->) e
monad do? Why, it duplicates an argument:
> rJoin :: (e -> (e -> a)) -> (e -> a)
> rJoin s e = s e e
A little thought shows that this corresponds exactly to the diagonalizing join
on Stream
s: rJoin s e = s e e
can be read as "the e
th element of rJoin s
is the e
th element of the e
th stream in the stream of streams s
." See?
So I told my officemate Daniel about this, and it occurred to us that there’s nothing special here about Nat
at all! rJoin
is polymorphic in e
; R -> a
is a monad for any type R
.
Functors which are isomorphic to (->) R
for some concrete type R
are called representable; so what this means is that all representable functors are monads. (Not that we were the first to think of this.)
Theme 3: Stream
s are comonads
Hmm, but Stream
is a comonad too, right?
> class Comonad w where
> extract :: w a -> a
> duplicate :: w a -> w (w a)
>
> instance Comonad Stream where
> extract = sHead
> duplicate s@(hd :> tl) = s :> duplicate tl
And since Stream
is isomorphic to (->) Nat
, that type must be a comonad too. What is the corresponding comonad instance for (->) Nat
?
> type Nat = Integer -- just pretend, OK?
>
> instance Comonad ((->) Nat) where
Extracting from a stream just returns its head element, that is, the element at index 0. So extracting from a Nat -> a
applies it to 0.
> extract = ($0)
Duplicating a stream gives us a stream of streams, where the nth output stream contains consecutive elements from the original stream beginning with the nth. Put another way, the jth element from the ith stream in the output is the (i+j)th element of the original stream:
> duplicate s i j = s (i + j)
Neat. Unlike the implementation of join
for the monad instance, however, this is definitely making use of the particular structure of Nat
. So this throws some cold water on our hopes of similarly generalizing this to all representable functors.
…or does it?
Theme 4: Comonads for representable functors
In the previous paragraph I said "this is definitely making use of the particular structure of Nat
", but I was being deliberately obtuse. Nat
has lots and lots of structure, surely we weren’t using all of it! In fact, we only mentioned the particular natural number 0
and the addition operation. Hmm… zero and addition… what’s interesting about them? Well, zero is the identity for addition, of course, and addition is associative – that is, the natural numbers form a monoid under addition with zero as the identity. So just as a wild guess, perhaps it’s the monoid structure of Nat
which makes the comonad instance possible?
In fact… yes! It turns out that comonad structures on R -> a
are in one-to-one correspondence with monoid structures on R
. To prove this, we can… oh, darn, looks like we’re out of time! (Read: this blog post is getting too long and if I don’t publish something soon I never will.) I’ll continue in another post, but in the meantime you might fancy trying to prove this yourself.