[Haskell-cafe] Re: Playing with delimited continuations

[oleg at pobox.com]

The ZFS library contains the most up-to-date implementation of the CC
monad and the transformer. I have a few other versions scattered
around, but they are probably not relevant. I found the CC_FrameT.hs
to be the fastest one.

> Is that you can think of normal continuations as delimited
> continuations with a global prompt p0 that denotes the end of the
> computation. You can emulate this using the reader monad to store the
> prompt:

Alternatively, one can use implicit parameters. They are quite handy
in this case.


> So, I suppose my first question is if anyone can see a better way of
> generalizing the types of the control operators to work with the
> arbitrarily nested monad stacks typically used in MTL.

I believe the answer to this question is NO. That means, (delimited)
continuations expose the fundamental limitation of monadic
transformers. Monadic transformation approach imposes the strict
separation of layers. They layers are fixed at compile time and can't
dynamically change. Alas, there are many _practically significant_
circumstances where the layers have to change dynamically, have to
interleave. Our ICFP06 paper discusses this point a bit, and the
accompanying code contains the relevant examples. 
	http://okmij.org/ftp/packages/DBplusDC-README.txt
Please see the README file and the file reader.hs in the source code.

When we first realized that monadic transformers had a significant
limitation, we too felt odd. Please see also below.

> First, the prompt module needs to use unsafeCoerce, or something equivalent.
> But, of course, unsafeCoerce feels dirty to me, and it'd be nice if some cool
> type system hackery could be used instead of going around the type system.

Alternatively, if we have reference cells available (STRef or IORef),
then we don't need unsafeCoerce. The whole code is pure Haskell with
no unsafe operations, and is type safe and sound. This outcome is not
an accident: given monadic style, the CC monad and reference cells are
`equivalent'. Given one, we can get the other. Any type system that is
capable of typing reference cells will give us delimited continuations
(provided we have the monadic style so we can deal with the
`stack'). One part of that claim, from multi-prompt delimited
continuations to reference cells, was formulated and proven in the
ICFP06 paper. The converse was formulated in an appendix to the paper,
which was taken out because we ran out of space-time. The proof
was done by construction, which is not generally available (although
the pure OCaml implementation of CC shows how that can be done).

The only drawback of using STRef or IORef to implement CC is that CC
is no longer a transformer (because neither ST nor IO are). That may
not be such a big drawback as the only benefit of CC being transformer
(for us, at least) is that we can lay it out over the IO monad. Well,
actually there is another benefit, of limiting the effects of the
code: even if the CC m code will execute in the IO monad, the code
cannot know that. 

Incidentally, there is actually little need to mix CC with other monad
transformers like reader, writer, RWST, Error, etc. The CC monad
subsumes them all! That is the important theoretical result by
Filinski: delimited continuations can express every expressible monad. 
This has important practical benefits: we can use real names (variables
of the type Prompt) to operate various pieces of state, environment,
errors, etc. We no longer need to count the number of 'lift'. The
overall performance may be better, too: each monadic layer adds at
least one closure. CC monad can implement threads, and I have a hunch
CC monad can implement STM.

> Second is a minor point. There's a sequence datatype in the paper that
> represents the delimited stack:
>
> > data Seq s r a b ...
>
> Which represents a sequence of frames that take a value of type 'a' to
> a value of type 'b'. The paper mentions that the empty constructor
> should have type 'Seq s r a a', but that it's impossible to do that,
> so they instead have it take a function that provides evidence of the
> equivalence between a and b, using 'id' and a smart constructor to
> have the same effect. But, with GADTs, it's now possible to have a
> constructor with the right type directly, so I did that in my
> implementation.

Have you checked the latest draft of the paper from Amr Sabry's home
page? They might have changed that point. Anyway, there is an
implementation 

> data Seq s r a = PushP (Prompt.Prompt r a) (Seq s r a)
>                | forall c. PushSeg (s r a c) (Seq s r c)
>                | forall c. PushCO (a -> c) (Seq s r c)
>
> type SubSeq s r a b = Seq s r b -> Seq s r a

that has no EmptyS constructor as you can see. So, the trouble you
have encountered goes away. The authors are aware of that minor
point. The point is truly minor so perhaps it is not bothering
with. If you'd like that code, please check with the authors first,
because it is wholly based on their work.