Re: (continuation monad) type problem...

[Pietro Abate <Pietro.Abate@anu.edu.au>]

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