[Haskell-cafe] Re: Playing with delimited continuations

[Dan Doel]

On Thursday 05 July 2007, oleg at 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