Re: (continuation monad) type problem...

[oleg@pobox.com]

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.