(continuation monad) type problem...

(continuation monad) type problem...

[oleg]

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

Re: (continuation monad) type problem...

[Pietro Abate]

Hi. Thank you for your reply !

On Wed, Jul 12, 2006 at 01:40:56AM -0700, oleg@pobox.com wrote:
[...]
> 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>

After a bit of struggling and with the help of Dirk Thierbach on
comp.lang.functional I came up with this solution...

module type Monad = sig
  type 'a m
  val return : 'a -> 'a m
  val bind : 'a m -> ('a -> 'b m) -> 'b m
end

module ListM : Monad = struct
  type 'a m = 'a list
  let return a = [a]
  let bind m k = List.concat (List.map k m)
end;;

module ContT (M : Monad) = struct
  type res = unit
  type 'a k = Cont of (('a -> 'a m) -> 'a m)
  and 'a m = (res * 'a k M.m) M.m

  let return a = Cont (fun c -> c a)
  let bind m k = Cont (fun c ->
    let (Cont m')  = m   in m' (fun a ->
    let (Cont ka') = k a in ka' c))
end;;

module ContListM = ContT (ListM);;

but ContT is not a monad as the type inferred for bind is not
polymorphic : bind : 'a k -> ('a -> 'a k) -> 'a k

And I think this is true in general as soon as I define a monad type
recursively. For example I'm also trying with a state compound monad
along these lines:
type 'a m = Cons of 'a m -> ('a * 'a m) M.m
where M.m is, for example a list monad, and I have the same problem.

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

Is this the same problem I'm facing here ? I'll study your code a bit more.
Dropping polymorphism is acceptable in a program, but not if I want to
prove proprieties about this monad. In particular I think the ContT
monad as it stands, it is not commutative...

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

The point of the ContListM is to capture a list of computations ('a m),
where each element (res * 'a k M.m) has the result of the computation up
to a certain point (res in the example) and the list of all the
continuations on that branch ('a k M.m). Each element of the list ('a m)
corresponds to a computation branch. The idea is to create a fsa that
stops at each state, asks for new input and resumes the computation
following an external procedure.  Alternation in the fsa gives the need
to have an outer monad list to account different possible
branches/computations that the fsa can choose. This is very much an
embryonic idea, I hope it will work out :)

pietro
-- 
++ Blog: http://blog.rsise.anu.edu.au/?q=pietro
++ 
++ "All great truths begin as blasphemies." -George Bernard Shaw
++ Please avoid sending me Word or PowerPoint attachments.
   See http://www.fsf.org/philosophy/no-word-attachments.html

Re: [Caml-list] Re: (continuation monad) type problem...

[Jacques Carette]

It seems that a small modification to the definition of ContT can 
restore polymophism:

module ContT (M : Monad) = struct
  type res = unit
  type ('a,'b) k = Cont of (('a -> 'b m) -> 'b m)
  and 'a m = (res * ('a,res) k M.m) M.m

  let return a = Cont (fun c -> c a)
  let bind m k = Cont (fun c ->
    let (Cont m')  = m   in m' (fun a ->
    let (Cont ka') = k a in ka' c))
end;;

The main change is that to have 2 type parameters in your 
continuation.   Also note that while 'a m is defined in terms of res (ie 
unit) for its second parameter, we know this doesn't matter (since 
continuations never really "return"), and thus ocaml is able to infer a 
polymorphic type for bind:

val bind : ('a, 'b) k -> ('a -> ('c, 'b) k) -> ('c, 'b) k

Jacques

Re: (continuation monad) type problem...

[oleg]

Pietro Abate wrote:
> but ContT is not a monad as the type inferred for bind is not
> polymorphic : bind : 'a k -> ('a -> 'a k) -> 'a k
> And I think this is true in general as soon as I define a monad type
> recursively. 

That polymorphism problem is inherent; to avoid it we need to add
extra parameters to our continuation (as Jacques Carette pointed
out), or do something else. Namely, turn to delimited continuations
with multiple prompts. Truly undelimited continuations are hardly ever
called for. Multi-prompt delimited continuations are strictly more
expressive; they also have clear operational and denotational
semantics. The latter is the consequence of CPS transforms.  Also,
multi-prompt delimited continuations have no typing problems and they
are available in the CC monad, which is truly a monad with no
reservations.

	http://www.cas.mcmaster.ca/~carette/pa_monad/
	http://www.cas.mcmaster.ca/~carette/pa_monad/test-cc.ml


> The point of the ContListM is to capture a list of computations ('a m),
> where each element (res * 'a k M.m) has the result of the computation up
> to a certain point (res in the example) and the list of all the
> continuations on that branch ('a k M.m). Each element of the list ('a m)
> corresponds to a computation branch. The idea is to create a fsa that
> stops at each state, asks for new input and resumes the computation
> following an external procedure.  Alternation in the fsa gives the need
> to have an outer monad list to account different possible
> branches/computations that the fsa can choose. 

I'm afraid I could not understand the problem. Why the conventional
FSA implementations won't work? I should point out that the
phrase ``result of the computation up to a certain point'' is
evocative of delimited continuations. Incidentally, delimited
continuations can be used to realize the LogicT monad (transformer,
actually) -- which is MonadPlus with additional operations supporting
a `look-ahead' in a non-deterministic computation. The latter is
needed to implement committed choice and "don't care"
nondeterminism. The implementation indeed maintains the tree of
continuations (each `mplus' builds a fork). The current
implementation is in Haskell
	http://pobox.com/~oleg/ftp/Computation/monads.html#LogicT
but it can be quite easily ported to OCaml, now that CC monad is
available here too.