[Haskell-cafe] Implementing the State Monad (Was: Can every monad can be implemented with Cont?)

[apfelmus]

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.