Hello, My interest was recently caught reading some of Oleg Kiselyov's material on delimited continuations, and so I decided to look into them a little closer. Don Stewart also mentioned in passing on #haskell that'd it'd be nice to have support for delimited continuations either in the standard library, or in some other easily installable package. So, I thought I'd see what such a beast might look like, and dug up the Dybvig, Petyon-Jones, Sabry paper[1] on the subject that I'd read long ago, but probably not understood much. :) After a day or so of hacking, I have (what I think is) a proper implementation of the monad and transformer, along with a suitable typeclass, and instances for the various transformers in the MTL. However, I have by no means tested it extensively (as I don't have a lot of ideas off hand for monad stacks involving delimited continuations), and I'm not totally thrilled with the results I have, so I thought I'd ask for advice/commentary here. Code is attached. First, I guess, should come an example of code using the delimited continuations:
pop = do (h:t) <- get put t return h
abortP p e = withSubCont p (\_ -> e)
loop 0 _ = return 1 loop n p = do i <- pop if i == 0 then abortP p (return 0) else do r <- loop (n-1) p return (i*r)
test1 n l = runDelCont (runStateT (newPrompt >>= \p -> pushPrompt p (loop n p)) l)
test2 n l = runState (runDelContT (newPrompt >>= \p -> pushPrompt p (loop n p))) l
So, loop finds the product of the first n numbers stored in a list in the state, but aborts immediately if it sees a 0. test1 and test2 stack the monads in the opposite order, but the results are the same in this case (it isn't a very sophisticated example). Another example, from the paper, 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:
type Continue r b a = ReaderT (Prompt.Prompt r b) (DelCont r) a
runContinue :: (forall r. Continue r b b) -> b runContinue ct = runDelCont (newPrompt >>= \p -> pushPrompt p (runReaderT ct p))
callCC' f = withCont (\k -> pushSubCont k (f (reify k))) where reify k v = abort (pushSubCont k (return v)) abort e = withCont (\_ -> e) withCont e = ask >>= \p -> withSubCont p (\k -> pushPrompt p (e k))
loop2 l = callCC' (\k -> loop' k l 1) where loop' _ [] n = return (show n) loop' k (0:_) _ = k "The answer must be 0." loop' k (i:t) n = loop' k t (i*n)
So, the loop computes the product of a list of numbers, returning a string representation thereof, but aborts with a different message if it sees 0. Again, nothing special, but it seems to work. However, this is where I started to run into some uglines that followed from my design choices. Most flows from the typeclass: class (Monad m) => MonadDelCont p s m | m -> p s where newPrompt :: m (p a) pushPrompt :: p a -> m a -> m a withSubCont :: p b -> (s a b -> m b) -> m a pushSubCont :: s a b -> m a -> m b So, 'm' is the delimited control monad in question, 'p' is the type of prompts associated with said monad, and 's' is the associated type of subcontinuations that take an 'a', and produce a 'b'. Those four functions are the generalizations of the four control operators from the paper. The crux of the matter is the way the prompts and subcontinuations are typed. A prompt 'p a' can have values of type 'a' returned through it, which is fine in the vanilla DelCont monad. However, in a monad transformed by a StateT, a computation 'm a' isn't returning an 'a' through the prompt. It's actually returning an '(a,s)', due to the state threading. And the same is an issue with the subcontinuation. So, I came up with a couple wrappers: newtype PairedPrompt s p a = PP { unPP :: p (a, s) } newtype PairedSubCont s k a b = PSC { unPSC :: k (a, s) (b, s) } And then you can declare instances like so: instance (MonadDelCont p s m) => MonadDelCont (PairedPrompt t p) (PairedSubCont t s) (StateT t m) where ... Where the declarations not only lift the delimited control actions, but wrap and unwrap the prompts and subcontinuations appropriately. However, this has two issues: 1) It seems kind of kludgy at first glance, although maybe that's just me. 2) It doesn't always work correctly. Consider the following code:
loop3 l = callCC' (\k -> loop' k l 1) where loop' _ [] n = return n loop' k (0:_) _ = k 0 loop' k (i:t) n = tell [n] >> loop' k t (i*n)
It does almost the same thing as loop2, only it has some writer output, too. And we'd like to write:
test3 l = runContinue (runWriterT (loop3 l))
but we can't, because that's a type error, because the prompt is created outside of runWriterT, where it will have type 'Prompt r (a, w)', but used inside runWriterT, where it needs to have type 'PairedPrompt w (Prompt r) a'. Instead, we have to write:
test3 l = runDelCont (runReaderT (runWriterT (newPrompt >>= \p -> pushPrompt p (local (const p) $ loop3 l))) undefined)
So that the prompt is created and used in the same monadic context. This is hardly ideal. 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. Nothing's come to my mind immediately, but I've stopped thinking about it very hard for the time being, and I'm sure there are people here who are much better acquainted with the theory of this sort of thing than I am. I suppose my other issues have to do with the original implementation itself, although I don't really feel very qualified to criticize it, and I can see why all the things were done the way that they were... First, the prompt module needs to use unsafeCoerce, or something equivalent. Prompts are, internally, just Ints, but they have a phantom type (I think that's the right term) denoting the type of value that can be returned through them. Then we eventually want to split the call stack using a prompt of type 'Prompt r a', but there be many prompts on the stack, which will have type 'Prompt r b' for some b (and the actual type of b is forgotten by the stack, I believe, as it's an existential type). However, since the internal Ints are unique identifiers, when we find that the identifiers match, 'a' and 'b' must be the same. So, the implementation uses unsafeCoerce to forge evidence that they are. 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. But I've really no idea whether there's any substitute for unsafeCoerce here, so I thought I'd ask some of the experts here. 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. However, after saying that in the paper, they go on to use the empty constructor with the coerced evidence functions produced above to produce empty sequences of type 'Seq s r a b' where we have some evidence that 'a' and 'b' are the same. So, using the GADT approach, where in the original paper there'd be a single EmptyS constructor, there is now required an extra coercion constructor on top of it in most cases where empty sequences are used. So, I suppose my second question is whether there is any sense in restricting the type to 'Seq s r a a' at all, since it just seems to require extra baggage? I suppose this might tie in with the above question, as the coercions of types Haskell's type system can't prove equal are what's being used. Third, just as a general question, is the paper I'm using the most definitive and recent on the subject of implementing delimited continuations in Haskell? I did some quick google searches, but nothing much turned up besides this paper, and some papers using the implementation in examples of using delimited continuations. It's also the implementation Oleg uses in his recent zipper file system, so I assume there haven't been any particularly radical developments since it was written (which wasn't that long ago, I suppose). Anyhow, I'd appreciate any discussion or thoughts anyone had on the above, or on delimited continuations in haskell in general, as it's a topic that's interested me lately. The attached code is certainly in no shape to be put in a library yet, but perhaps if the issues above can be fixed, or it's decided that they don't matter, it could pave the way. Apologies for the length, and I hope I'm posting to the right place (this didn't seem formal enough for haskell@...). Cheers, Dan Doel [1]: http://research.microsoft.com/Users/simonpj/papers/control/control.pdf