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.
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
