[Haskell-cafe] Playing with delimited continuations
Dan Doel
dan.doel at gmail.com
Wed Jul 4 04:13:33 EDT 2007
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 at ...).
Cheers,
Dan Doel
[1]: http://research.microsoft.com/Users/simonpj/papers/control/control.pdf
-------------- next part --------------
A non-text attachment was scrubbed...
Name: DelCont.hs
Type: text/x-hssrc
Size: 4412 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20070704/450a8bb4/DelCont-0001.bin
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Prompt.hs
Type: text/x-hssrc
Size: 1095 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20070704/450a8bb4/Prompt-0001.bin
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Seq.hs
Type: text/x-hssrc
Size: 1631 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20070704/450a8bb4/Seq-0001.bin
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Test.hs
Type: text/x-hssrc
Size: 2082 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20070704/450a8bb4/Test-0001.bin
More information about the Haskell-Cafe
mailing list