Rambling Thoughts about Comonads

[Slightly revised since first posted.]

This entire post is, or is intended to be, a Literate Haskell file. You can copy-paste the whole thing into an .lhs file and run it with ghc (I vouch for it only in version 6.12.3). Some caveats: I am not a Haskell programmer. At worst you should suspect everything I say of being, well, wrong, and at best I’m comfortably certain the code in here is not as elegant as it ought to be. Apologies for all the references that I neglected to include either out of ignorance or out of laziness. And as will be clear I’ve been awfully sloppy throughout.

A while back I started thinking about comonads. I now have little idea why—“a while” is nearly two years—but I think I must have been troubled by the apparent lack of symmetry between monads and comonads in functional programming. It seemed somehow ufair that monads are so useful and get so much attention, while their poor duals are neglected. Really I just wondered whether some of the standard monad constructions and connections—monad notation, most obviously, and the connection with Applicative Arrows—had any dual consructions, and whether they might be useful. It turns out they there are indeed dual constructions, although I suppose I can’t truly swear to the usefulness part. Herein are most of my collected thoughts on the subject.

BTW, I have little idea how much of what follows is original, but a couple of things way down below the fold might be. You can easily find a fair bit about comonads and examples thereof, but I haven’t seen either real proposals for comonad notation (not that I’m claiming there’s one of those here either) or anything about “Coapplicative Arrows” elsewhere.

First, some preliminaries:

> {-# OPTIONS_GHC -XArrows -XImpredicativeTypes #-}
> import Prelude hiding (id, (.))
> import Control.Category 
> import Control.Arrow
> import Control.Monad


We’ll be using arrows, so we need to turn on arrow notation and import the relevant modules. We’ll also need Impredicative Types later on. GHC 6.12 will warn about impredicative types, but I hope that something very much like this will work in GHC 7 (maybe with more type annotations, probably not a bad thing). Since Control.Category defines . and id, we’ll hide the Prelude versions. The comonad module (here missing its module declaration, for pedagogical purposes) was lifted from here.

Now to work. So what’s a comonad, anyway? As a quondam mathematician, I find it easiest to think of both monads and comonads in terms of categories and arrows. For programming purposes an “arrow” is a generalization of “function”—they are things that can be composed like functions, but which can have all manner of other structure. In Haskell they are encapsulated by the Arrow class. See this for an introduction to Haskell arrows—this post will make little sense if you don’t—and this for a very nice lecture about monads from this perspective.

Now many arrows can be expressed in terms of plain old functions. It may happen that

    a b c


can be expressed as the set of functions from b to some more compicated type based on c:

    a b c = b -> m c ,


And that’s what a monad is! Or rather, the type constructor m is a monad. From the Arrow class’s composition >>> we can construct the usual bind and join operations on the monad, and from the arrow laws we can derive the monad laws.

Some other arrows can be expressed the other way round. That is they’re functions from some complicated thing to a plain old type:

    a b c = w b -> c


In that case w (“w” is a sort of upside-down “m”…) is a comonad.

In category theory comonads are the duals of comonads, pretty much the same things with all the arrows turned around. In functional programming more or less the same is true. Just as you can always “put something into” a monad with return, you can always “get something out of” a comonad. As you can flatten multiple levels of monad constructors with join, you can introduce more levels of comonadic constructors. Bind has an obvious analog in cobind. In detail

> infixl 1 =>>
> infixl 1 .>>
> class Functor w => Comonad w where
>   extract :: w a -> a
>   (=>>) :: w a -> (w a -> b) -> w b
>   duplicate :: w a -> w (w a)
>   (.>>) :: (w a -> b) -> (w b -> c) -> w a -> c
>   duplicate x = x =>> id
>   f .>> g = \x -> g ( x =>> f )


[Credit: as I said, I stole this from here].

The comonad functions should satisfy laws that are the duals of the monad laws, e.g.

    extract ( x =>> f ) = f(x)
    x =>> extract = x


We’ll also have occasion to use comonadic fixpoints:

> class (Comonad w) => ComonadFix w where
>     wfix :: w (w a -> a) -> a


This will make sense with examples. The simplest one is of course the Identity functor, but that is too simple. Slightly more interesting is taking a product with some fixed type:

> instance Comonad ((,) c) where
>   extract   (c,x) = x
>   (c,x) =>> f = (c, (f (c, x)))


This is dual to the Either monad; mathematically we get a monad from a coproduct and a comonad from a product (and vice versa, sort of—see below). It’s also left adjoint to the (->) monad: the same arrow type can be expressed as either a monad or a comonad. That is,

    (c, b) -> d


is the same as

    b -> c -> d .


More interesting still is state. This is one of the principal inspiration for the use of monads, where we have the State monad

    St s a = s -> (s, a)


(well, conceptually that’s what it is). An object of a State monad type is a “state transformer,” a function that takes transforms a state while extracting a value. That makes more sense (to me!) as a model for computation in terms of arrows: the associated Arrow type is

    a b c  =  b -> (s -> (s, c))


which through the Cartesion adjunction is the same thing as

    a b c  =  (s, b) -> (s, c) 


The arrows are plain old functions, but we’ve tacked states on to everything.

We can do the same thing with (->) rather than (,). From the arrow type

    a b c  =  (s -> b) -> (s -> c)


we can use the adjunction the other way and get a COmonad

    a b c  =  (s, s -> b) -> c .


These arrows are functions that map “value extractors” into each other. In gory detail,

> data CoState s a = CoState s (s->a)
> instance Functor (CoState s) where
>     fmap g (CoState s f) = CoState s (g . f)
> instance Comonad (CoState s) where
>     extract (CoState s f) = f s
>     cs@(CoState s f) =>> g = 
>           CoState s (\x -> g (CoState x f))


These can represent a notion of “computation in a context.” And indeed comonads generally can be viewed as a way of adding context to computations.

Another prototypical example is streams, that is, endless lists. We can define them, and their comonad structure (and some generally useful functions) thusly (see this, from which this example and the next were adapted, for more details on streams):

> infixr 1 :< 
> data Stream a = a :< Stream a
> instance Functor Stream where
>     fmap f (v :< s) = (f v) :< fmap f s
> instance Comonad Stream where
>   extract (v :< _)    = v
>   val@(x :< xs) =>> f = f val :< (xs =>> f)
> headS (h :< t) = h
> tailS (a :< t) = t
> takeS :: Int -> Stream a -> [a]
> takeS 0 s = []
> takeS i (v :< s) = v : (takeS (i-1) s)


Cobinding a function to a stream simply applies the function to each successive “tail” in turn:

    (1, 2, 3, 4, ... ) =>> f =
        ((f (1, 2, 3, 4, ... ),
            (f (2, 3, 4, 5, ...),
                (f (3, 4, 5, 6, ...), ...)


Duplicate collects all the tails into a single stream, so

    duplicate (1, 2, 3, 4, ... ) =
        ((1, 2, 3, 4, ...),
            (2, 3, 4, 5, ...),
               (3, 4, 5, 6, ...), ...)


Comonadic stream computations—the associated arrows—map streams to streams in a “historyless” way. The nth value in the resulting stream depends only on the nth and greater values in the origin stream. If we want something more general we can add a list representing “what we’ve seen so far”:

> data LS a = LS [a] (Stream a)
> instance Functor LS where
>     fmap f (LS l s) = LS (fmap f l) (fmap f s)
> instance Comonad LS where
>     extract (LS _ (h :< _)) = h
>     ls@(LS l s) =>> f = LS (bindL l s) (bindS l s)
>         where
>             bindL [] _ = []
>             bindL l@(h:t) s = h2:l2
>                 where
>                     h2 = f(LS t (h :< s)) 
>                     l2 = bindL t (h :< s)
>             bindS l s@(h :< t) = h2 :< s2
>                 where
>                     h2 = f(LS l s)
>                     s2 = bindS (h:l) t
> nextLS (LS l (h:< t)) = LS (h:l) t
> instance ComonadFix LS where
>     wfix fls@(LS fl fs) = v where
>         wff [] (f :< fs) ls@(LS h s) = 
>             let v = f ls
>                 LS _ t = wff [] 
>                   fs (LS (v:h) (tailS s))
>             in LS h (v :< t)
>         wff (fh : ft) fs ls = 
>                   nextLS (wff ft (fh :< fs) ls)
>         LS h t = wff fl fs (LS [] t) 
>         v = extract (LS h t) 
> toStream :: LS a -> Stream a
> toStream (LS [] s) = s
> toStream (LS (h:t) s) = toStream (LS t (h :< s))
> nextLSF (LS _ (_:< h:< _)) = h
> -- go back to the previous place in the "history"
> -- if we're already at the beginning, prepend
> -- the given value
> delayCF :: a -> LS a -> a
> delayCF a (LS [] _) = a
> delayCF a (LS (h:_) _) = h
> delay :: a -> LS a -> LS a
> delay a w = w =>> delayCF a
> takeLS :: Int -> LS a -> [a]
> takeLS n = takeS n . toStream


That’s also equivalent to a “stream with position.”

Simlarly, comonads can be used to represent all sorts of structures with positions therein. Cellular automata on various sorts of regular grids provide another example.

Armed with specific examples—Stream is generally a good one—we can think about some generalities. We’ve seen some of the relationship between arrows and monads and comands, but let’s make it more precise. If we have a monad we can make an arrow type by taking Kleisli arrows. And pretty much the same thing works with comonads (including fixpoints):

> newtype CoKleisli w a b = 
>       CoKleisli { unCoKleisli :: w a -> b }
> instance (Comonad w) => Category (CoKleisli w) 
>       where
>           id = CoKleisli extract
>           (CoKleisli f) . (CoKleisli g) = 
>               CoKleisli (\x -> f (x =>> g))
> instance Functor (CoKleisli w a) where
>   fmap f (CoKleisli g) = CoKleisli (f . g)
> instance (Comonad w) => Arrow (CoKleisli w) where
>   arr f = CoKleisli (f . extract)
>   CoKleisli a &&& CoKleisli b
>         = CoKleisli (a &&& b)
>   CoKleisli a *** CoKleisli b
>         = CoKleisli (a . fmap fst 
>             &&& b . fmap snd)
>   first a  = a *** arr id
>   second a = arr id *** a
> extractA :: (Comonad w) => (CoKleisli w) b b 
> extractA = CoKleisli extract
> instance ComonadFix w => ArrowLoop (CoKleisli w) 
>   where
>     loop (CoKleisli f) =
>         let
>             -- g :: w a -> w (w (a, b) -> (a, b))
>             g wa = wa =>> (\a -> \wab -> 
>                        (extract a, snd (f wab))) 
>             -- k :: w a -> (a, b)
>             k wa = wfix (g wa)
>         in
>             CoKleisli (\wa -> fst (f (wa =>> k )))


Something interesting (by my nerdly definition of “interesting”) here is that, in a sense, comonads make better Arrows than monads do. The product function *** as applied to monads is not really a product in the categorical sense. It’s not necessarily even a functor. We really should have

    (f *** g) >>> (arr fst) = (arr fst) >>> f


but we don’t—try it with lists, for example. But in the comonadic case *** really does act like a proper product.

On the other hand, monads do have nice Choice functions—(+++) is a real coproduct. Comonads do not. We can still define (+++) for CoKleisli arrows, but it is ill-behaved in the same way as products in the monadic case. This we can do by extracting a value from the comonad, constructing a new “constant comonad” from that value, and apply the given function. For left, that looks like

> instance (Comonad w) => ArrowChoice (CoKleisli w) 
>   where
>     left (CoKleisli f) = 
>         let
>             g (Left x) cm = Left $ 
>                   f (cm =>> \y -> x )
>             g (Right x) cm = Right x 
>             h x = g (extract x) x
>         in
>             CoKleisli h


I don’t know if this is practically useful or not.

Mathematically (and here you might want to skip to the next paragraph, even if you’ve somehow managed to make it this far), that’s a deepish result of the nature of monads and comonads. Given a monad M in some category, we have adjoint functors F |- G, where F sends objects to their counterparts in the Kleisli category, while G sends them back to their monadified versions. Since F is a left adjoint, it preserves colimits, including coproducts, so (F (x|y)) is the coproduct F x | F y. There’s no particular reason for the same to hold with products, though. Looking at arrows and translating to Haskell, that leads to the observations above. Since comonads are dual, we can apply the same reasoning switching “left” and “right”, adding “co-” everywhere it isn’t, and removing it everywhere it is. We thus find that the functor to the CoKleisli category is a right adjoint and preserves limits, including products.

Haskell’s monad notation is of course enormously convenient, so it’s natural to ask whether something similar could be done with comonads. There are of course complications. We can’t really identify a (co)do black with a comand, but rather with a comonadic arrow. We’ll use (probably unwisely) “proc” to name the argument, as with arrows. We also can’t really use the nice nested-lambda translation that is one definition of a monadic do-block, or at least it’s awkward to get it to work (try it!). Instead we’ll “push” the do-bound variables through each line, as in arrow notation (more or less) or in actual implementations of monadic do-blocks (I think).

Suppose we want to attach a meaning to

    proc w -> do
        x <- foo
        y <- bar


foo, bar, and baz are expressions of “simple” type in which w, x, and y appear free as variables of comonadic type. We would like that to mean something along the lines of

    (\w -> foo) .>> (\x -> bar) .>> (\y -> baz)


but that won’t work if w appears in bar or baz. We can get around this by defining the do-block to be (here using “fst”, “snd”, and the imaginary “third” very loosely!)

    \m0 ->
    let m1 = m0 =>> (\w -> (extract w, foo))
        m2 = m1 =>> (\m ->  
                let w = fmap fst m
                    x = fmap snd m
                in (extract w, extract x, bar)
        m3 = m2 =>> (\m ->  
                let w = fmap fst m
                    x = fmap snd m
                    y = fmap third m
                in bar
    in extract m3


or something like that. Needs some work.

However it should work, there’s no comonad notation now, but there is arrow notation, and we can use that to assemble comonadic functions. So let’s go back to the relationship between comonads and arrows.

The Kleisli arrows of a monad are instances of ArrowApply, with an arrow

    app :: a (a b c, b) c


This is just an arrowfied version of the usual eval function

    eval :: (b -> c, b) -> c
    eval (f, x) = f x


Conversely, any instance of ArrowApply whose app satisfies a few conditions leads to a monad, where (in psedocode now)

    m b = a () b
    x >>= f = () -> arr ( () -> (f, x) ) >>> app


We’ve “tied up” the first type argument of an arrow type simply by setting it to (), analogously to the fact that

    b <-> () -> b


Then we can “apply” an arrow to a monadic object in the obvious way:

    m b >>= f  <->  a () b >>> f


If we can establish a corresponence between arrows and monadic functions then we’re done: and this is where we use the app arrow:

    f :: a b c  <->  
        \x -> arr (\(y::a () b) -> 
                (y >>> f, ())) >>> app


What about comonads? We already know how to get an arrow from a comonad, but can we go back the other way? It turns out that we can. To do that we need to be able to construct some type w a from an arrow type and establish some correspondence between arrows and ordinary functions w a -> b. To get a comonadic type from an arrow we need to tie up the second type argument. This takes a little more cleverness than the monadic case did. We can do it by taking a sort of double dual:

    w b = forall c . (a b c -> c)


(and here’s where we start seeing impredicative types). We can easily cobind an arrow to such a thing

    x =>> f  =  \y -> x ( f >>> y )


To associate an arrow to a comonadic function we can use a sort of adjoint to app:

    coapp :: a b (forall c . a b c -> c)
    f :: w b -> c  <->  coapp >>> arr (\x -> f x)


This works if coapp satisfies conditions including

    coapp >>> arr (\g -> g id) = id
    f >>> coapp = 
        coapp >>> arr (\g -> (\h -> g (f >>> h)))


To formalize all this we’ll define a type class

> class Arrow a => ArrowCoApply a where
>     coapp :: a b (forall c . a b c -> c)


CoKleisli arrows are coapplicative:

> instance (Comonad w) => ArrowCoApply (CoKleisli w) 
>   where
>     coapp = CoKleisli (\wb -> \(CoKleisli f) -> f wb)


It’s easy to check the coapp conditions. And now to go back from arrows to comonads:

> newtype ArrowCoApply a => ArrowComonad a b = 
>     ArrowComonad (forall c . a b c -> c)
> instance ArrowCoApply a => Functor (ArrowComonad a) 
>   where
>       fmap f (ArrowComonad g) = 
>           ArrowComonad (\h -> g (arr f >>> h))
> instance ArrowCoApply a => Comonad (ArrowComonad a) 
>   where
>     extract (ArrowComonad f) = f (arr id)
>     (ArrowComonad f) =>> g = 
>         let garr = coapp >>> 
>               arr (\x -> g (ArrowComonad x)) in
>         ArrowComonad (\h -> f (garr >>> h))
> -- Translation between arrows and 
> --    comonadic functions
> comonadToArrow :: (ArrowCoApply a) => ((ArrowComonad a b) -> c) -> a b c
> comonadToArrow g = coapp >>> arr (\x -> g (ArrowComonad x))
> arrowToComonad :: (ArrowCoApply a) => a b c -> (ArrowComonad a b) -> c
> arrowToComonad x (ArrowComonad f) = f x


We’ll close by demonstrating that this actually works by using comonads and arrows to compute Fibonacci numbers in a few increasingly abstruse ways. A simple one first, using CoKleisli arrows of streams; we’ll use arrow notation to make comonadic functions:

> -- a utility class for streams and LS's:
> -- a comonadic "next" function
> class Comonad s => HasNext s where
>       next :: s a -> a
> instance HasNext Stream where
>       next (_ :< x :< xs) = x
> instance HasNext LS where
>       next = extract . nextLS
> nextA :: HasNext w => CoKleisli w a a
> nextA = CoKleisli next
> fibhelp :: Stream Integer-> Integer
> fibhelp = 
>     let f = proc x -> do
>         y <- nextA -< x
>         extractA -< x+y
>     in unCoKleisli f
> fibs :: Stream Integer
> fibs = 1 :< 1 :< (fibs =>> fibhelp)


If we use streams-with-history, we can build the recursion into the proc/do block, through ArrowLoop:

> delayA x = CoKleisli (delayCF x)
> fibhelp2 :: LS () -> Integer
> fibhelp2 =
>     let f = proc a -> do 
>                 rec z <- extractA -< x + y
>                     y <- delayA 1 -< z
>                     x <- delayA 1 -< y
>                 extractA -< x
>     in (unCoKleisli f )
> nothingS = () :< nothingS
> fibs2 = (LS [] nothingS) =>> fibhelp2


and for a particularly recondite and impractical last act, we can take one of these comonads, turn it into an arrow, and then back into a comonad:

> -- take a comonad into the "double dual" comonad
> -- via CoKleisli and ArrowComonad
> toCC :: Comonad w => w a -> ArrowComonad (CoKleisli w) a
> toCC x = ArrowComonad $ \(CoKleisli f) -> f x
> fibsCC = toCC fibs 
> fibsLSCC = toCC fibs2
> nextCC :: HasNext w => 
>       ArrowComonad (CoKleisli w) a -> a
> nextCC = arrowToComonad nextA
> takeCC :: HasNext w => 
>       Integer -> 
>           (ArrowComonad (CoKleisli w) a) -> [a] 
> takeCC 0 x = []
> takeCC n x = 
>       (extract x) : takeCC (n-1) (x =>> nextCC)


And we use all this machinery in a main function of startling banality

> main = do
>       putStrLn "Comonad testing"
>       putStrLn "Streams:"
>       putStrLn $ show $ takeS 10 fibs
>       putStrLn "LS:"
>       putStrLn $ show $ takeLS 10 fibs2
>       putStrLn "Streams via arrows and back:"
>       putStrLn $ show $ takeCC 10 fibsCC
>       putStrLn "LS via arrows and back:"
>       putStrLn $ show $ takeCC 10 fibsLSCC



Tags: , , ,

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: