(continuation monad) type problem...

[oleg@pobox.com]

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#caml-shift

(the second solution: cc-monad, 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).