[<<][meta][>>][..]
Mon Jan 17 14:16:22 EST 2011

State Continuation Monad

In OCaml it's this:

'a monad = state -> (state ->'a -> answer) -> answer
let ret a     = fun s k -> k s a
let bind a f  = fun s k -> a s (fun s' x -> f x s' k)

To Haskellify it we introduce some wrappers:

               


-- State Continuation monad.  The State and Answer types are dummy
-- types for now..
type State  = Integer
type Answer = Integer

-- See defs in 
-- [1] http://www.cs.rice.edu/~taha/publications/conference/pepm06.pdf

data SC a = 
    SC {runSC :: (State -> (State -> a -> Answer) -> Answer)}

instance Monad SC where
    return a = SC (\s k -> k s a)
    (SC a) >>= f = SC(\s k -> a s (\s' x -> (runSC (f x)) s' k))
                   


The thing to see here is that the monad structure does not depend on
the State and Answer types.  These are just passed around.
Additionally, the SC type constructor takes one parameter, which will
be the type implementing values/target_code or any other abstract
domain.

This is something I found hard to understand at first, and I'm still
clumsy at expressing it: The monad interface shows only how certain
wrapping structure can be composed.  All the other typing context can
be completely in the background.

How to make those params abstract then?  It's actually quite
straightforward.  This type-checks fine:



data SC s r c = 
    SC {runSC :: (s -> (s -> c -> r) -> r)}

instance Monad (SC s r) where
    return a = SC (\s k -> k s a)
    (SC a) >>= f = SC (\s k -> a s (\s' x -> (runSC (f x)) s' k))
                   

So, what does this do?  A state-continuation object (SC) is a function
that takes a state and a continuation and produces a result.  The
continuation of type (s -> c -> r) is _another_ function that takes a
state and an input (c, code) and produces a result.  In the following
it is important to distinguish these two function types.

The Monad operation `return' creates a SC that passes the state along
with the value argument to the continuation.  The Monad operation
`bind' creates a new SC by composing two functions in CPS form with
additional threaded state.

(SC a) >>= f = SC (\s k -> a s (\s' x -> (runSC (f x)) s' k))

`a' is a state-continuation function (SC)
`f' is a function that produces an SC given an object

The updated state is produced by the `a' SC function and passed to the
anonymous continuation function (\s' x -> (runSC (f x)) s' k).  This
latter continuation function invokes the SC created by `f' from the
input argument `x' which is also passed to the anonymous continuation
function by `a'.

A more loose interpration: The `body code' that belongs to the SC `a'
and the SC produced by `f' is performed in sequence.  This sequential
nature is a property of code written in continuation passing style.
The state is simply "along for the ride" and is updated and passed on
appropriately.

So what does the SC do?  It can be any operation that takes a state
and a continuation object, performs some computation and passes the
updated state and a result to a continuation.


[1] http://www.cs.rice.edu/~taha/publications/conference/pepm06.pdf




[Reply][About]
[<<][meta][>>][..]