On Thursday 05 July 2007, oleg@pobox.com wrote:
I believe the answer to this question is NO. That means, (delimited) continuations expose the fundamental limitation of monadic transformers.
I suppose this is a bit disheartening, but I suppose it's also good to know I wasn't totally off track. Closure is nice.
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.
I stuck this on my reading list during my brief searches a few days ago. I'll have to get busy reading it.
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.
Good to know. I suppose ST gives me less of an icky feeling than unsafeCoerce.
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!
This had actually crossed my mind, although making CC work more like the rest of the monads in MTL, rather than the somewhat more isolated ST seemed like a noble goal. Perhaps time would be better spent working out analogues/instances of classes using just the CC monad, though, for times when you want to use the interfaces (but not necessarily the actual transformers, due to the issues above) along with delimited continuations. I suppose it's something to think about.
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.
As a matter of fact, I had two versions of the paper, but neither was the latest. The newest version (if it's what I now have) does use GADTs to enforce the 'Seq s r a a' type of EmptyS, but more surprisingly than that (to me, at least), it no longer has a coercion constructor, as they no longer use functions for evidence. Instead, it uses another GADT as the evidence, and unsafeCoerce on that. Eliminating PushCO and such altogether seems attractive. Anyhow, thanks for the input, and the pointers to the papers and such (and writing so many of them in the first place. :) Incidentally, I really enjoyed your "Delimited continuations in operating systems" paper. Reading that one really made things click for me as to how delimited continuations can actually show up in real systems, as opposed to just being an esoteric, abstract construct). Regards, Dan Doel