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.