How can the continuation monad be expressed using the free monad?

26
votes

Supposedly, all monads can be expressed using Free (if this isn't true, what is a counter-example and why)? How can the continuation monad or its corresponding transformer be expressed using Free or FreeT - what would be the corresponding functor? Or if they can't, what's the reason why?

Update: By expressed I mean basically isomorphic to Free F where F is a functor we're looking for, like for example Writer w is isomorphic to Free ((,) w).

4
haskellmonadscontinuationsfree-monad
maybe you should move this to the computer science section (scicomp.stackexchange.com) - most likely you will get an answer there – Random Dev
But Writer w isn't isomorphic to Free ((,) w), merely a quotient of it. After all, Writer w is ((,) w). Furthermore, Cont r is isomorphic to a quotient of Free (Cont r) as I demonstrated below. Can you clarify further? – Tom Ellis
@TomEllis Good point, I'll need to think about it. – Petr

4 Answers

15
votes

The continuation monad is the counterexample you are looking for. I'm not knowledgeable enough to provide a full proof but I'll give you a couple of references to look up.

The idea is that monads have a concept of "rank" associated with them. "Rank" roughly means the number of operations needed to provide the full functionality of the monad.

I suspect that, with the exception of continuation-derived monads, all the monads we deal with in Haskell have rank, e.g. Identity, Maybe, State s, Either e, ..., and their combinations through their transformers. For example, Identity is generated by no operations, Maybe is generated by Nothing, State s by get and put s and Either e by Left e. (Perhaps this shows they all in fact have finite rank, or perhaps put s counts as a different operation for each s, so State s has the rank of the size of s, I'm not sure.)

Free monads certainly have rank because Free f is explicitly generated by the operations encoded by f.

Here is a technical definition of rank, but it's not very enlightening: http://journals.cambridge.org/action/displayAbstract?aid=4759448

Here you can see the claim that the continuation monad does not have rank: http://www.cs.bham.ac.uk/~hxt/cw04/hyland.pdf. I'm not sure how they prove that, but the implication is that the continuation monad is not generated by any collection of operations and thus cannot be expressed as (a quotient of) a free monad.

Hopefully someone can come along and tidy up my technicalities, but this is the structure of the proof you want.

2
votes

Here's a silly answer that shows that both your question and my earlier answer need work.

Cont can easily be expressed using Free:

import Control.Monad.Free
import Control.Monad.Trans.Cont

type Cont' r = Free (Cont r)

quotient :: Cont' r a -> Cont r a
quotient = retract

Cont is a (quotient of) the free monad on itself (of course). So now you have to clarify precisely what it is you mean by "express".

2
votes

See my answer to a question of yours from last year. Let's consider r = Bool (or more generally any type r which admits a nontrivial automorphism).

Define m (up to newtype wrappers) as m :: (() -> Bool) -> Bool; m f = not (f ()). Then m is nontrivial but m >> m is trivial. So Cont Bool is not isomorphic to a free monad.

The full computation in Haskell:

rwbarton@morphism:/tmp$ ghci
GHCi, version 7.8.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> import Control.Monad.Cont
Prelude Control.Monad.Cont> let m :: Cont Bool (); m = ContT (\f -> fmap not (f ()))
Loading package transformers-0.3.0.0 ... linking ... done.
Prelude Control.Monad.Cont> runCont m (const False) -- m not trivial
True
Prelude Control.Monad.Cont> runCont (m >> m) (const False)
False
Prelude Control.Monad.Cont> runCont (m >> m) (const True) -- (m >> m) trivial
True
1
votes

Here's a couple tiny proofs that there doesn't exist a Functor f such that for all a :: * and m :: * -> * FreeT f m a is equivalent to ContT r m a using the normal interpretation of FreeT.

Let m :: * -> * such that there is no instance Functor m. Due to instance Functor (ContT r m) there is an instance Functor (ConT r m). If ContT r and FreeT f are equivalent, we would expect Functor (FreeT f m). However, using the normal interpretation of FreeT, instance (Functor f, Functor m) => Functor (FreeT f m), there is no Functor (FreeT f m) instance because there is no Functor m instance. (I relaxed the normal interpreation of FreeT from requiring Monad m to only requiring Functor m since it only makes use of liftM.)

Let m :: * -> * such that there is no instance Monad m. Due to instance Monad (ContT r m) there is an instance Monad (ConT r m). If ContT r and FreeT f are equivalent, we would expect Monad (FreeT f m). However, using the normal interpretation of FreeT, instance (Functor f, Monad m) => Monad (FreeT f m), there is no Monad (FreeT f m) instance because there is no Monad m instance.

If we don't want to use the normal interpretation of Free or FreeT we can cobble together monsters that work just like Cont r or ContT r. For example, there is a Functor (f r) such that Free (f r) a can be equivalent to Cont r a using an abnormal interpretation of Free, namely Cont r itself.