Re: (continuation monad) type problem...
 oleg@p...
[
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:  20060720 (01:25) 
From:  oleg@p... 
Subject:  Re: (continuation monad) type problem... 
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. Multiprompt delimited continuations are strictly more expressive; they also have clear operational and denotational semantics. The latter is the consequence of CPS transforms. Also, multiprompt 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/testcc.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 `lookahead' in a nondeterministic 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.