[Haskell-cafe] Can every monad can be implemented with Cont? (was: New slogan for haskell.org)

[apfelmus]

Don Stewart wrote:
> allbery:
>
>> Didn't someone already prove all monads can be implemented in terms  
>> of Cont?
>>
> 
> Cont and StateT, wasn't it?
> And the schemers have no choice about running in StateT :)

You sure? I want to see the proof :)

Last time I stumbled upon something like this, the "proof" was to embed 
every monad m in the type

   type Cont m a = forall b . (a -> m b) -> m b

with an

   instance Monad (Cont m) where ...

_independent_ of whether m is a monad or not.

The problem I see with it is that we didn't really encode  m  with it 
since we're still dependent on  return  and (>>=) via

   project :: Monad m => Cont m a -> m a
   project f = f return

and

   inject :: Monad m => m a -> Cont m a
   inject x = (x >>=)

I mean, the starting point for a concrete monad M are some primitive 
operations like

   get :: M s
   put :: s -> M ()

and a function

   observe :: M a -> (S -> (a,S))

together with laws for the primitive operations (= operational semantics)

   observe (put s >>= x) = \_ -> observe (x ()) s
   observe (get >>= x)   = \s -> observe (x s ) s

and for return

   observe (return a)    = \s -> (a,s)

Now, implementing a monad means to come up with a type M and functions 
(>>=) and  return  that fulfill the monad laws. (In general, the result 
type of observe is _not_ M a !) This can be done with the standard trick 
of implementing stuff as constructors (see Unimo for details 
http://web.cecs.pdx.edu/~cklin/papers/unimo-143.pdf).

But - and that's the problem - I don't see how it can be done with Cont 
in all cases. It works for the above state monad (*) but what about 
primitives like

   mplus  :: m a -> m a -> m a
   callcc :: ((a -> m r) -> m r) -> m a

that have monadic arguments in a contravariant position (possibly even 
universally quantified)?


Regards,
apfelmus

*: Here you go:

   type Observe s a = s -> (a,s)
   type State s a   = Cont (Observe s) a

   get   = \x -> (\s -> observe (x s ) s)  -- law for get
   put s = \x -> (\_ -> observe (x ()) s)  -- law for put

   observe f = f $ \a -> (\s -> (a,s))  -- law for  observe (return a)