(continuation monad) type problem...
 oleg@p...
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20060712 (08:43) 
From:  oleg@p... 
Subject:  (continuation monad) type problem... 
Pietro Abate wrote about the problem typing the continuation monad. The problem is that we have to specifically keep in mind the answer type. For example: let id x = x;; module CONT = struct (* type 'a m = {cont: 'w . ('a > 'w) > 'w } *) type ('w,'a) m = {cont: ('a > 'w) > 'w } let return x = {cont = fun k > k x} let (>>=) m f = {cont = fun k > m.cont (fun x > (f x).cont k) } let reset e = {cont = fun k > k (e.cont id)} let shift e = {cont = fun k > (e (fun v > {cont = fun c > c (k v)})).cont id} let run m = m.cont id end;; With these shift/reset in place, we can express call/cc (assuming that the whole program is wrapped in reset) let callcc1 proc = CONT.shift (fun f > CONT.(>>=) (proc (fun v > CONT.shift (fun _ > f v))) f);; whose inferred type val callcc1 : (('a > ('b, 'c) CONT.m) > ('b, 'a) CONT.m) > ('b, 'a) CONT.m = <fun> seems quite right. We can test as follows: let test1 = let module M = struct open CONT let result = run ( let proc k = (k 10) >>= (fun v > return (v+100)) in reset ((callcc1 proc) >>= (fun v > return (v + 5))) ) end in M.result ;; (* ==> 15 *) The lack of polymorphism may be acceptable at times. If not, we have to explicitly introduce typed prompts  as was first proposed by Gunter, Remy and Riecke. You can see the implementation of that in http://pobox.com/~oleg/ftp/Computation/Continuations.html#camlshift (the second solution: ccmonad, which is fully OCaml). The latter is included in the monadic notation for OCaml, recently announced on this list. Pietro Abate's message also showed an attempt to mix the continuation and backtracking monad. That seems puzzling: the continuation monad can express any other monad that could be expressed at all in the language (see Filinski, Representing Monads, POPL94). Thus, the continuation monad alone is sufficient for backtracking (as well as many other things).