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 nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id AAA0FBB83 for ; Thu, 20 Jul 2006 03:25:24 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.6/8.13.6) with ESMTP id k6K1PNpJ027730 for ; Thu, 20 Jul 2006 03:25:24 +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 DAA25429 for ; Thu, 20 Jul 2006 03:25:23 +0200 (MET DST) Received: from selenite.metnet.navy.mil (selenite.metnet.navy.mil [192.16.167.32]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k6K1PGW3014400 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Thu, 20 Jul 2006 03:25:22 +0200 Received: (qmail 15022 invoked by uid 107); 20 Jul 2006 01:25:03 -0000 Received: from vwmetnet.metnet.navy.mil (192.16.167.21) by selenite.metnet.navy.mil with SMTP; 20 Jul 2006 01:25:03 -0000 Received: from Adric.metnet.fnmoc.navy.mil ([10.100.105.102]) by vwmetnet.metnet.navy.mil (NAVGW 2.5.2.9) with SMTP id M2006072001362908061 for ; Thu, 20 Jul 2006 01:36:29 GMT Received: by Adric.metnet.fnmoc.navy.mil (Postfix, from userid 760) id 9E633A9B4; Wed, 19 Jul 2006 18:22:50 -0700 (PDT) To: caml-list@inria.fr Subject: Re: (continuation monad) type problem... Reply-To: oleg@pobox.com Errors-To: oleg@okmij.org From: oleg@pobox.com Message-Id: <20060720012250.9E633A9B4@Adric.metnet.fnmoc.navy.mil> Date: Wed, 19 Jul 2006 18:22:50 -0700 (PDT) X-Miltered: at nez-perce with ID 44BEDB83.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 44BEDB7C.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; oleg:01 polymorphism:01 delimited:01 delimited:01 semantics:01 computations:01 corresponds:01 computations:01 point'':01 haskell:01 oleg:01 monads:01 ocaml:01 prompts:98 wrote: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.2 required=5.0 tests=NO_REAL_NAME autolearn=disabled version=3.0.3 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.