jeff p wrote:
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 :)
I think this is referring to Andrzej Filinski's paper "Representing Layered Monads" in which it shown that stacks of monads can be implemented directly (no layering) by using call/cc and mutable state.
Thanks for the reference! I still don't understand Filinski's papers enough to say whether there's more to the embedding than just type Cont m a = forall b . (a -> m b) -> m b reify :: Monad m => Cont m a -> m a reify f = f return reflect :: Monad m => m a -> Cont m a reflect x = (x >>=) Does this already give a performance benefit without further inlining? I doubt it. Anyway, all this leads to a fun and easy way to implement monads, for example the state monad. We have the primitive operations type State s a get :: State s s put :: s -> State s () together with the usual monad laws and the operational semantics evalState :: State s a -> (s -> a) evalState (return x) = \_ -> x evalState (get >>= k) = \s -> evalState (k s ) s -- make the state s available to k evalState (put s >>= k) = \_ -> evalState (k ()) s -- use a new state s Why "operational semantics"? Well, we're just specifying what happens when we "execute" a get or put "instruction" by saying how the execution proceeds with the next instruction k pointed out by >>=. We're not using the "usual" and "elaborate" type like s -> (a,s) to thread the state around, we're using a humble function s -> a to specify that a value a depends on some state s . The operational semantics will do the state plumbing for us. In other words, the we don't have to come with a special implementation like s -> (a,s) that works, we will *mechanically* get one from our intended operational semantics. Now, how to implement? Well, the best way to start is to represent each primitive operation with a new constructor: (GADT notation, needs the -XGADTs flag) data State :: * -> * -> * where Return :: a -> State s a (:>>=) :: State s a -> (a -> State s b) -> State s b Get :: State s s Put :: s -> State s a With this _term representation_, we can implement the operational semantics by evalState ((m :>>= n) :>>= k) = evalState (m :>>= (n :>>= k)) -- monad law associativity evalState (Return x :>>= k) = evalState (k x) -- monad law left unit evalState (Get :>>= k) = \s -> evalState (k s ) s -- semantics of get evalState (Put s :>>= k) = \_ -> evalState (k ()) s -- semantics of put evalState (Return x) = \_ -> x -- semantics of return evalState m = evalState (m :>>= Return) -- monad law right unit Neat, isn't it? Every law and every specification for the primitive instructions has been used exactly once. Simple and painless, but not fully optimized yet. With the first equation, using :>>= left-associatively has similar problems like using ++ left-associatively. Both concat' = foldl (++) [] sequence_' = foldl (>>) (return ()) would show quadratic time behavior. So, just like with difference lists, the idea is to represent the operations in the monad together with the _context_ they are commonly used in. For concatenating lists, the context is (xs ++ _) so that every list xs is represented by \ys -> (xs ++ ys) For our state monad, the context is evalState (m :>>= _) i.e., we make evaluation and sequencing "built-in". More specifically, we also make the evaluation of the next instructions built-in, so that every monadic action m will be represented by \k -> evalState (m :>>= k') where k = evalState . k' In other words, we will represent the type State s a by State' s a = forall b . (a -> (s -> b)) -> (s -> b) But this is just the continuation monad! data Cont m a = Cont (forall b . (a -> m b) -> m b) type State' s a = Cont (s ->) a with m a = s -> a the result type of our semantics evalState . So, we already get >>= and return for free, knowing that they fulfill the monad laws return x = \k -> k x m >>= f = \k -> m (flip f k) Our custom primitive operations get and put are straightforward to implement get = \k -> evalState (Get :>>= k') = \k -> \s -> evalState (k' s ) s = \k -> \s -> k s s put s = \k -> \_ -> k () s These definitions are crystal clear from their operational semantics, given some practice reading them. Last but not least, there is evalState which implements the behavior of the Return instruction evalState m = evalState (m' :>>= Return) = (\k -> evalState (m' :>>= k')) (evalState . Return) = m (\x -> evalState (Return x)) = m (\x -> \_ -> x) That's it for the state monad. For reference, here's the full implementation type State s a = Cont ((->) s) a get = \k s -> k s s put s = \k _ -> k () s evalState m = m const We get >>= and return for free from the predefined Cont (assuming that the "done right"-version with universal quantification would be in the libraries, that is). Of course, this approach isn't limited to the state monad. Here are some parser combinators type Result a = String -> [a] type Parser a = Cont (Result) a run p = p (\x i -> if null i then [x] else []) symbol = \k i -> case i of { c:cs -> k c; [] -> []; } fail = \k i -> [] p +++ q = \k i -> p k i ++ q k i Can you see the operational semantics? (Think of p k as run (p >>= k)). If not, stick to the term implementation and check out Unimo below for a free >>= :) This simple way of implementing monads by their operational semantics is known for quite some time John Hughes. The Design of a Pretty-printing Library. http://citeseer.ist.psu.edu/hughes95design.html Chuan-kai Lin. Programming Monads Operationally with Unimo. http://web.cecs.pdx.edu/~cklin/papers/unimo-143.pdf and is in fact related to the good old continuation passing style of IO and parser combinators. But I think it's powerful and I'd like it to be well-known. Regards, apfelmus PS: Put differently, the question of the original thread "Can every monad can be implemented with Cont?" is whether Unimo can implement strictly more monads than Cont.