From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 95E7EBB84 for ; Thu, 13 Jul 2006 09:09:05 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k6D794YV028698 for ; Thu, 13 Jul 2006 09:09:04 +0200 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id JAA11558 for ; Thu, 13 Jul 2006 09:09:03 +0200 (MET DST) Received: from mail.rsise.anu.edu.au (mail.rsise.anu.edu.au [150.203.208.4]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k6D78xBZ028664 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Thu, 13 Jul 2006 09:09:02 +0200 Received: from localhost (localhost [127.0.0.1]) by mail.rsise.anu.edu.au (Postfix) with ESMTP id 8EE2E541B4 for ; Thu, 13 Jul 2006 17:08:48 +1000 (EST) Received: from mail.rsise.anu.edu.au ([150.203.208.4]) by localhost (mail [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 23037-03 for ; Thu, 13 Jul 2006 17:08:48 +1000 (EST) Received: from pulp.rsise.anu.edu.au (pulp.rsise.anu.edu.au [150.203.208.49]) by mail.rsise.anu.edu.au (Postfix) with ESMTP id 6ACD853F8E for ; Thu, 13 Jul 2006 17:08:43 +1000 (EST) Received: by pulp.rsise.anu.edu.au (Postfix, from userid 1560) id E9AC4A0AFC8; Thu, 13 Jul 2006 17:08:48 +1000 (EST) Date: Thu, 13 Jul 2006 17:08:48 +1000 From: Pietro Abate To: caml-list@inria.fr Subject: Re: (continuation monad) type problem... Message-ID: <20060713070848.GA3885@pulp.rsise.anu.edu.au> Mail-Followup-To: Pietro Abate , caml-list@inria.fr References: <20060712084056.EC61DAC97@Adric.metnet.fnmoc.navy.mil> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20060712084056.EC61DAC97@Adric.metnet.fnmoc.navy.mil> X-Operating-System: GNU/Linux X-Organization: Research School of Information Science and Engineering (Australian National University) User-Agent: Mutt/1.5.11+cvs20060403 X-Virus-Scanned: by amavisd-new-20030616-p10 (Debian) at mail.rsise.anu.edu.au X-Miltered: at concorde with ID 44B5F190.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 44B5F18B.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; anu:01 oleg:01 val:01 sig:01 val:01 struct:01 struct:01 polymorphism:01 gunter:01 oleg:01 ocaml:01 monadic:01 notation:01 ocaml:01 polymorphism:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 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 = > 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