(continuation monad) type problem...

oleg@p...
 Pietro Abate
[
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:  20060713 (07:09) 
From:  Pietro Abate <Pietro.Abate@a...> 
Subject:  Re: (continuation monad) type problem... 
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#camlshift > (the second solution: ccmonad, 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/nowordattachments.html