[<<][meta][>>][..]Fri Feb 19 13:16:04 CET 2010

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 continuation. 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

[Reply][About]

[<<][meta][>>][..]