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)