Fri Feb 19 13:16:04 CET 2010

State / Continuation monad

Multi-stage programming with functors and monads[1] uses the following
state-continuation monad, described in Fig.1 on page 11:

  type ('p,'v) monad = 's -> ('s -> 'v -> 'w) -> 'w
       constraint 'p = <state : 's; answer :'w; ..>

The monad is represented by a function taking two arguments: a state
's and a continuation ('s -> 'v -> 'w), and producing a value 'w.  The
continuation takes two arguments, a state 's and a value 'v and
produces a value 'w.

  let ret (a :'v) : ('p,'v) monad = fun s k -> k s a

Unit creates a function that when invoked, passes the value to the

  let bind (m : ('p,'v) monad) (f : 'v -> ('p,'u) monad) : ('p,'u) monad
      = fun s k -> m s (fun s' b -> f b s' k)

Bind creates a function that when invoked, invokes the monadic value m
with the provided state s and a constructed continuation.  That
continuation applies the function f to the value it receives to
produce a new monadic value, which it then applies to its provided
state s' and the original continuation.

  let fetch s k = k s s
  let store v _ k = k v ()

State access.

  let k0 _ v = v
  let runM m = fun s0 -> m s0 k0

Run a monad providing it an initial state and the initial continuation
which returns the value.

  let retN (a : ('c,'v) code) :
   (<classif: 'c; answer: ('c,'w) code; ..>, ('c,'v) code) monad
     = fun s k -> .<let t = .~a in .~(k s .<t>.)>.

Control effect.

  let ifL test th el = ret .< if .~test then .~th else .~el >.
  let ifM test th el = fun s k ->
    k s .< if .~test then .~(th s k0) else .~(el s k0) >.

The monad is documented also in [2].  First, let's gain some more
intuition about the state-continuation monad.  (I'm still just reading
the definition; not understanding it intuitively).

What _is_ this monad?  It is a computation producing a value,
parameterized by an initial state s and a continuation k.  Let's focus
on both in isolation, and then combine them to see how they interact.

The computation encoded in the monad is written in CPS, meaning that
when it is done, it will pass its result to k.  The simplest such
computation is created by `ret' which passes state and value to the
continuation, effectively "returning".

To get a better idea of the CPS monad, it might help to switch to the
continuation monad in Haskell, and explain its bind operator[3]:

  -- r is the final result type of the whole computation 
  newtype Cont r a = Cont { runCont :: ((a -> r) -> r) } 
  instance Monad (Cont r) where 
      return a       = Cont $ \k -> k a                       -- i.e. return a = \k -> k a 
      (Cont c) >>= f = Cont $ \k -> c (\a -> runCont (f a) k) -- i.e. c >>= f = \k -> c (\a -> f a k) 

With tagging/untagging removed (also see Haskell comments above) and
translated to OCaml this is:

  type ('a,'r) monadK = ('a -> 'r) -> 'r

  let retK a    = fun k -> k a
  let bindK m f = fun k -> m (fun a -> f a k)

The type is more clear now: the monad value is a CPS computation that
takes a continuation ('a -> 'r) and produces a value.  The continuation
is a function that takes a value 'a and produces a result 'r.

  * retK creates a computation that takes a continuation k and passes
    it the value a

  * bindK takes a computation m and a function f and chains them
    together such that first m is performed, and its output is piped
    through f before continuing with k

Similarly for the state monad[4]:

  newtype State s a = State { runState :: (s -> (a,s)) } 
  instance Monad (State s) where 
      return a        = State $ \s -> (a,s)
      (State x) >>= f = State $ \s -> let (v,s') = x s in runState (f v) s' 

Converted to untagged OCaml

  type ('s, 'a) monadS = ('s -> ('a * 's))

  let retS a    = fun s -> (a,s)
  let bindS x f = fun s -> let (v,s') = x s in (f v) s'

[1] http://www.cas.mcmaster.ca/~carette/publications/scp_metamonads.pdf
[2] http://www.cs.rice.edu/~taha/publications/conference/pepm06.pdf
[3] http://www.haskell.org/all_about_monads/html/contmonad.html
[4] http://www.haskell.org/all_about_monads/html/statemonad.html