Mon 27 Jun 2011

## Monads from Comonads

Posted by Edward Kmett under Category Theory , Comonads , Haskell , Kan Extensions , Mathematics , Monads[10] Comments

Today I'll show that you can derive a `Monad`

from any old `Comonad`

you have lying around.

But first, we'll need to take a bit of a bit of a detour.

**A Monad Sandwich**

We'll need the definition of an adjunction on the category of Haskell types, which we can strip down and borrow from my adjunctions package.

class (Functor f, Representable u) => Adjunction f u | f -> u, u -> f where leftAdjunct :: (f a -> b) -> a -> u b rightAdjunct :: (a -> u b) -> f a -> b

Here we can define our Adjunction by defining leftAdjunct and rightAdjunct, such that they witness an isomorphism from `(f a -> b)`

to `(a -> u b)`

Every Adjunction `F -| G : C -> D`

, gives rise to a monad GF on D and a Comonad FG on C.

In addition to this, you can sandwich an additional monad M on C in between GF to give a monad GMF on D:

and you can sandwich a comonad W on D in between F and G to yield the comonad FWG on C:

**A Contravariant Comonad Sandwich**

As was first shown to me me by Derek Elkins, this construction works even when you C is not the category of Haskell types!

Consider the Contravariant functor `Op r`

:

newtype Op a b = Op { getOp :: b -> a } instance Contravariant (Op a) where contramap f g = Op (getOp g . f)

We can view `Op r`

as a functor from `Hask^op -> Hask`

or as one from `Hask -> Hask^op`

.

We can define a notion of a contravariant adjunction `F -| G : Hask^op -> Hask`

.

Data.Functor.Contravariant.Adjunction

class (Contravariant f, Corepresentable g) => Adjunction f g | f -> g, g -> f where leftAdjunct :: (b -> f a) -> a -> g b rightAdjunct :: (a -> g b) -> b -> f a

Where, now, `leftAdjunct`

and `rightAdjunct`

witness the isomorphism from `(f a < - b)`

to `(a -> g b)`

, which means once you flip the arrow around both seem to be going the same way. Ultimately any contravariant adjunction on Hask is comprised of two isomorphic functors, each self-adjoint.

This gives rise to one notion of a comonad-to-monad transformer!

Control.Monad.Trans.Contravariant.Adjoint

But we can we do better?

**An End as the Means**

First, some boilerplate.

{-# LANGUAGE Rank2Types, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, UndecidableInstances #-} import Data.Monoid import Control.Comonad import Control.Applicative import Control.Comonad.Store.Class import Control.Comonad.Env.Class as Env import Control.Comonad.Traced.Class as Traced import Control.Monad.Reader.Class import Control.Monad.Writer.Class import Control.Monad.State.Class import Data.Functor.Bind

Our new comonad to monad transformer is given by

newtype Co w a = Co { runCo :: forall r. w (a -> r) -> r }

What we've done is added a quantifier to prevent the use of the type *r*, as we did when describing `Codensity`

and `Ran`

, categorically we've taken some kind of end. This idea came to me after an observation was made by Russell O'Connor that `Conts (Store s) a`

was pretty close to a continuation passing style version of `State s`

.

Now, we can start spitting out instances for this type.

instance Functor w => Functor (Co w) where fmap f (Co w) = Co (w . fmap (. f)) instance Comonad w => Monad (Co w) where return a = Co (`extract` a) Co k >>= f = Co (k .extend (\wa a -> runCo (f a) wa)) instance Comonad w => Applicative (Co w) where mf < *> ma = mf >>= \f -> fmap f ma pure a = Co (`extract` a)

In my break-out of category-extras, I've split off the semigroupoid structure of Kleisli-, co-Kleisli-, and static- arrow composition as `Bind`

, `Extend`

and `Apply`

respectively, so we can make use of slightly less structure and get slightly less structure in turn:

instance Extend w => Bind (Co w) where Co k >>- f = Co (k .extend (\wa a -> runCo (f a) wa)) instance Extend w => Apply (Co w) where mf < .> ma = mf >>- \f -> fmap f ma

**From comonad-transformers to the mtl**

We can look at how this transforms some particular comonads.

The comonadic version of `State`

is `Store`

. Looking at `Co (Store s) a`

Co (Store s) a ~ forall r. ((s -> a -> r, s) -> r) ~ forall r. (s -> a -> r) -> s -> r ~ forall r. (a -> s -> r) -> s -> r ~ Codensity ((->)s) a ~ State s a

This gives rise to a leap of intuition that we'll motivate further below:

instance ComonadStore s m => MonadState s (Co m) where get = Co (\w -> extract w (pos w)) put s = Co (\w -> peek s w ())

Sadly this breaks down a little for `Writer`

and `Reader`

as the `mtl`

unfortunately has historically included a bunch of extra baggage in these classes. In particular, in reader, the notion of `local`

isn't always available, blocking some otherwise perfectly good `MonadReader`

instances, and I've chosen not to repeat this mistake in `comonad-transformers`

.

instance ComonadEnv e m => MonadReader e (Co m) where ask = Co (\w -> extract w (Env.ask w)) local = error "local"

Ideally, local belongs in a subclass of `MonadReader`

.

class Monad m => MonadReader e m | m -> e where ask :: m a -> e class MonadReader e m => MonadLocal e m | m -> e where local :: (e -> e) -> m a -> m a

Similarly there is a lot of baggage in the `MonadWriter`

. The `Monoid`

constraint isnt necessary for the class itself, just for most instances, and the `listen`

and `pass`

members should be a member of a more restricted subclass as well to admit some missing `MonadWriter`

instances, but we can at least provide the notion of tell that is critical to `Writer`

.

instance (Monoid e, ComonadTraced e m) => MonadWriter e (Co m) where tell m = Co (\w -> Traced.trace m w ()) listen = error "listen" pass = error "pass"

But given the split out

instance Monad m => MonadWriter e m | m -> e where tell :: e -> m () instance MonadWriter e m => MonadListen e m | m -> e listen :: m a -> m (a, w) pass :: m (a, w -> w) -> m a

We could provide this functionality more robustly. (There is a similar subset of `Comonad`

s that can provide listen and pass analogues.)

While I am now the maintainer of the mtl, I can't really justify making the above corrections to the class hierarchy at this time. They would theoretically break a lot of code. I would be curious to see how much code would break in practice though.

**Combinators Please!**

There is a recurring pattern in the above code, so we can also improve this construction by providing some automatic lifting combinators that take certain cokleisli arrows and give us monadic values

lift0 :: Comonad w => (forall a. w a -> s) -> Co w s lift0 f = Co (extract < *> f) lift1 :: (forall a. w a -> a) -> Co w () lift1 f = Co (`f` ())

along with their inverses

lower0 :: Functor w => Co w s -> w a -> s lower0 (Co f) w = f (id < $ w) lower1 :: Functor w => Co w () -> w a -> a lower1 (Co f) w = f (fmap const w)

(The proofs that these are inverses are quite hairy, and lean heavily on parametricity.)

Then in the above, the code simplifies to:

get = lift0 pos put s = lift1 (peek s) ask = lift0 Env.ask tell s = lift1 (tell s)

**Co-Density?**

Co and Codensity are closely related.

Given any Comonad W, it is given rise to by the composition FG for some adjunction `F -| G : Hask -> C`

.

Considering only the case where `C = Hask`

for now, we can find that

Co w a ~ forall r. (f (g (a -> r)) -> r).

Since `f -| g`

, we know that `g`

is `Representable`

by `f ()`

, as witnessed by:

tabulateAdjunction :: Adjunction f u => (f () -> b) -> u b tabulateAdjunction f = leftAdjunct f () indexAdjunction :: Adjunction f u => u b -> f a -> b indexAdjunction = rightAdjunct . const

therefore

Co w a ~ f (g (a -> r)) -> r ~ f (f () -> a -> r) -> r

Since *f* is a left adjoint functor, `f a ~ (a, f ())`

by Sjoerd Visscher's elegant little `split`

combinator:

split :: Adjunction f u => f a -> (a, f ()) split = rightAdjunct (flip leftAdjunct () . (,))

which has the simple inverse

unsplit :: Adjunction f g => a -> f () -> f a unsplit a = fmap (const a)

so we can apply that to our argument:

Co w a ~ forall r. f (f () -> a -> r) -> r ~ forall r. (f () -> a -> r, f ()) -> r

and curry to obtain

Co w a ~ forall r. (f () -> a -> r) -> f () -> r

and swap the arguments

Co w a ~ forall r. (a -> f () -> r) -> f () -> r

then we can tabulate the two subtypes of the form (f () -> r)

Co w a ~ forall r. (a -> g r) -> g r

and so we find that

Co w a ~ Codensity g a

Finally,

Codensity g a ~ Ran g g a

but we showed back in my second article on Kan extensions that given f -| g that

Ran g g a ~ g (f a)

So `Co w ~ Co (f . g) ~ (g . f)`

, the monad given rise to by composing our adjunction the other way!

**Comonads from Monads?**

Now, given all this you might ask

Is there is a similar construction that lets you build a comonad out of a monad?

Sadly, it seems the answer **in Haskell** is no.

Any adjunction from `Hask -> Hask^op`

would require two functions

class (Contravariant f, Contravariant g) => DualContravariantAdjunction f g where leftAdjunct :: (f a -> b) -> g b -> a rightAdjunct :: (g b -> a) -> f a -> b

where **both functors are contravariant**.

Surmounting the intuitionistic impossibility of this, then given any such adjunction, there would be a nice coend we could take, letting us sandwich any `Monad`

in the middle as we did above.

There does exist one such very boring Contravariant Functor.

newtype Absurd a = Absurd (Absurd a) absurdity :: Absurd a -> b absurdity (Absurd a) = absurdity a instance Contravariant Absurd where contramap f (Absurd as) = Absurd (contramap f as) instance DualContravariantAdjunction Absurd Absurd where leftAdjunct _ = absurdity rightAdjunct _ = absurdity

We can safely sandwich IO within this adjunction from `Hask -> Hask^op`

to obtain a comonad.

newtype Silly m a = Silly { runSilly :: Absurd (m (Absurd a)) } instance Monad m => Extend (Silly m) where extend f (Silly m) = absurdity m instance Monad m => Comonad (Silly m) where extract (Silly m) = absurdity m

But for any more interesting such type that actually lets us get at its contents, we would be able to derive a circuitous path to `unsafePerformIO`

!

Since `unsafePerformIO`

should not be constructible without knowing `IO`

specifics, no **useful** `DualContravariantAdjunction`

s should exist.

June 27th, 2011 at 8:10 pm

An interesting consequence of this set of transformations was the long-standing debate on whether or not streams were more appropriately monads or comonads. I believe Dominic Orchard has written on this topic (http://talks.cam.ac.uk/talk/index/31165). I really need to work through this material properly :-)

June 28th, 2011 at 12:28 am

@Edward: I can’t find any links to Dominic’s material on the topic other than his subsequent discussions of codo notation. In there the only thing he has that mixes monads with comonads is a notion of ‘bido’ notation, which is pretty much what sigfpe and Uustalu and Vene have independently advocated as ways to deal with distributive laws over monads and comonads. Sadly, I think that approach doesn’t work out well in practice. I prefer working with comonads over a Kleisli category or monads over a Cokleisli category instead, rather than distributing. This lets me get decent computation sharing.

June 28th, 2011 at 10:54 am

Thank you for an awesome blog post! Though I wonder where the ‘Co’ data type comes from. You just pull it out of a hat. Is there a story behind it?

June 28th, 2011 at 11:26 am

Acutally, it _was_ pretty much pulled out of a hat. ;)

It came out as a happy accident in an email discussion with Russell O’Connor and Jacques Carette about exactly in what sense Store and State were dual.

June 28th, 2011 at 11:38 am

Yeah, looks like he never published the slides on the relevant talk. I’ll bug him about that.

June 28th, 2011 at 8:51 pm

[...] Last time, I showed that we can transform any Comonad in Haskell into a Monad in Haskell. [...]

June 30th, 2011 at 2:20 pm

[...] time before that in Monads from Comonads we observed that for non-transformer version of [...]

June 30th, 2011 at 10:49 pm

[...] Monads from Comonads, we built the comonad-to-monad [...]

June 27th, 2012 at 1:42 pm

Does this do anything?

data LeftCo m f x = forall z. LeftCo (f (m z) -> x) (f z);

November 4th, 2015 at 3:30 pm

It occurs to me that the form of Co w:

Co w a = forall r. w (a -> r) -> r

is to the Cokleisli arrow as the Yoneda encoding of m:

Yoneda m a = forall r. (a -> r) -> m r

is to the Kleisli arrow. Is there a way to generalize this to any ArrowApply?