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 [EMAIL PROTECTED]).
Cheers,
Dan Doel
[1]: http://research.microsoft.com/Users/simonpj/papers/control/control.pdf
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module DelCont (DelCont, DelContT, MonadDelCont(..), runDelCont, runDelContT) where
import Control.Monad
import Control.Monad.Trans
import Control.Monad.Identity
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer
import Seq
import qualified Prompt
-- The frame-based implementation from the Dybvig, Peyton-Jones, Sabry paper.
-- It was the one of the three that was called 'properly tail-recursive,' which
-- I expect is a good property.
newtype Frame m r a b = Frame (a -> DelContT r m b)
type Cont r m a b = Seq (Frame m) r a b
newtype SubCont r m a b = SC (Seq (Frame m) r a b)
-- The two exported types. Delimited continuation monad and transformer
-- I changed the names from CC to DelCont, as that seemed like a more MTL-ish
-- name.
newtype DelContT r m a = DCT (forall c. Cont r m a c -> Prompt.P r m c)
newtype DelCont r a = DelCont { unDelCont :: DelContT r Identity a }
deriving (Functor, Monad, MonadDelCont (Prompt.Prompt r) (SubCont r Identity))
runDelCont :: (forall r. DelCont r a) -> a
runDelCont dc = runIdentity (runDelContT (unDelCont dc))
appk :: (Monad m) => Cont r m a c -> a -> Prompt.P r m c
appk EmptyS v = return v
appk (PushP _ k) v = appk k v
appk (PushSeg (Frame f) k) v = let DCT e = f v in e k
appk (PushCO f k) v = appk k (f v)
runDelContT :: (Monad m) => (forall r. DelContT r m a) -> m a
runDelContT dc = Prompt.runP (let DCT e = dc in e EmptyS)
-- The new typeclass for monad stacks that allow delimited control
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
-- DelContT instances for various Monad classes, including, of course,
-- MonadDelCont
instance (Monad m) => MonadDelCont (Prompt.Prompt r) (SubCont r m) (DelContT r m) where
newPrompt = DCT (\k -> Prompt.newPrompt >>= appk k)
pushPrompt p (DCT e) = DCT (\k -> e (PushP p k))
withSubCont p f = DCT (\k -> let (subk, k') = splitSeq p k
DCT e = f (SC subk)
in e k')
pushSubCont (SC subk) (DCT e) = DCT (\k -> e (appendSeq subk k))
-- This instance was cribbed from the implementation of the zipper OS here:
-- http://okmij.org/ftp/Computation/Continuations.html#zipper-fs
instance MonadTrans (DelContT r) where
lift m = DCT (\k -> lift m >>= appk k)
instance (Monad m) => Monad (DelContT r m) where
return v = DCT (\k -> appk k v)
(DCT e) >>= f = DCT (\k -> e (PushSeg (Frame f) k))
instance (MonadState s m) => MonadState s (DelContT r m) where
get = lift get
put = lift . put
instance (MonadReader e m) => MonadReader e (DelContT r m) where
ask = lift ask
local f (DCT dc) = DCT (\k -> local f (dc k))
-- Instances of MonadDelCont for various other monad transformers.
-- Requires transforming prompts and subcontinuations to fit the 'hidden'
-- modifications of the monad transformers.
newtype PairedPrompt s p a = PP { unPP :: p (a, s) }
newtype PairedSubCont s k a b = PSC { unPSC :: k (a, s) (b, s) }
instance (MonadDelCont p s m) =>
MonadDelCont (PairedPrompt t p) (PairedSubCont t s) (StateT t m) where
newPrompt = PP `liftM` lift newPrompt
pushPrompt p m = StateT $ \s -> pushPrompt (unPP p) (runStateT m s)
withSubCont p f = StateT $ \s ->
withSubCont (unPP p) (\k -> runStateT (f (PSC k)) s)
pushSubCont k m = StateT $ \s ->
pushSubCont (unPSC k) (runStateT m s)
instance (MonadDelCont p s m) => MonadDelCont p s (ReaderT r m) where
newPrompt = lift newPrompt
pushPrompt p m = ReaderT $ \r -> pushPrompt p (runReaderT m r)
withSubCont p f = ReaderT $ \r -> withSubCont p (\k -> runReaderT (f k) r)
pushSubCont k m = ReaderT $ \r -> pushSubCont k (runReaderT m r)
instance (MonadDelCont p s m, Monoid w) =>
MonadDelCont (PairedPrompt w p) (PairedSubCont w s) (WriterT w m) where
newPrompt = PP `liftM` lift newPrompt
pushPrompt p m = WriterT $ pushPrompt (unPP p) (runWriterT m)
withSubCont p f = WriterT $
withSubCont (unPP p) (\k -> runWriterT (f (PSC k)))
pushSubCont k m = WriterT $ pushSubCont (unPSC k) (runWriterT m){-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Prompt (P, Prompt, runP, newPrompt, eqPrompt) where
import Control.Monad
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Monad.Trans
import Unsafe.Coerce
-- This implements the P/Prompt code from the Dybvig, Petyon-Jones, Sabry paper,
-- only as a monad transformer, and using the StateT monad (for the clever
-- deriving). I also switched to using unsafeCoerce rather than implementing it
-- with unsafePerformIO as they do in the paper.
data Prompt r a = Prompt Int
eqPrompt :: Prompt r a -> Prompt r b -> Maybe (a -> b, b -> a)
eqPrompt (Prompt i) (Prompt j)
| i == j = Just (unsafeCoerce id, unsafeCoerce id)
| otherwise = Nothing
newtype P r m a = P { unP :: StateT Int m a }
deriving (Functor, Monad, MonadState Int, MonadTrans, MonadReader e,
MonadWriter w, MonadPlus)
runP :: Monad m => (forall r. P r m a) -> m a
runP ps = evalStateT (unP ps) 0
newPrompt :: Monad m => P r m (Prompt r a)
newPrompt = do i <- get ; put (i + 1) ; return (Prompt i){-# OPTIONS_GHC -fglasgow-exts #-}
module Seq (Seq(..), splitSeq, appendSeq) where
import Prompt
-- The generalized sequence type from the Dybvig, Peyton-Jones, Sabry paper.
-- The paper mentions that EmptyS should have the type it does below, but that
-- it isn't possible. However, GADTs do make it possible, so I decided to use
-- them. However, the paper later goes on to use EmptyS in cases where the type
-- is not 'Seq s r a a', and I therefore have to use an extra PushCO. So, in the
-- end, I'm not sure if it's actually a win, but perhaps I'm missing something
-- else important.
data Seq s r a b where
EmptyS :: Seq s r a a
PushP :: Prompt r a -> Seq s r a b -> Seq s r a b
PushSeg :: s r a c -> Seq s r c b -> Seq s r a b
PushCO :: (a -> c) -> Seq s r c b -> Seq s r a b
splitSeq :: Prompt r b -> Seq s r a ans -> (Seq s r a b, Seq s r b ans)
splitSeq p EmptyS = error "Prompt was not found on the stack."
splitSeq p (PushP q sk) =
case eqPrompt q p of
Nothing -> let (subk, sk') = splitSeq p sk
in (PushP q subk, sk')
Just (a2b, b2a) -> (PushCO a2b EmptyS, PushCO b2a sk)
splitSeq p (PushSeg seg sk) =
let (subk, sk') = splitSeq p sk
in (PushSeg seg subk, sk')
splitSeq p (PushCO f sk) =
let (subk, sk') = splitSeq p sk
in (PushCO f subk, sk')
appendSeq :: Seq s r a b -> Seq s r b ans -> Seq s r a ans
appendSeq EmptyS sk = sk
appendSeq (PushP p subk) sk = PushP p (appendSeq subk sk)
appendSeq (PushSeg seg subk) sk = PushSeg seg (appendSeq subk sk)
appendSeq (PushCO f subk) sk = PushCO f (appendSeq subk sk){-# OPTIONS_GHC -fglasgow-exts #-}
module Test where
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer
import DelCont
import Prompt (Prompt)
test 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
pop :: MonadState [a] m => m a
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)
{-
*Test> test 5 [1..10]
(120,[6,7,8,9,10])
*Test> test 5 [0..10]
(0,[1,2,3,4,5,6,7,8,9,10])
*Test> test 10 [1..10]
(3628800,[])
*Test> test 100 ([1..10] ++ [0,0] ++ [1..])
(0,[0,1,2,3,4,5,6..
-}
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)
{-
*Test> runContinue (loop2 [1..10])
"3628800"
*Test> runContinue (loop2 $ [1..10] ++ [0] ++ [1..10])
"The answer must be 0."
*Test> runContinue (loop2 $ [1..10] ++ [1..10])
"13168189440000"
-}
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)
test3 l = runDelCont
(runReaderT
(runWriterT
(newPrompt >>= \p ->
pushPrompt p (local (const p) $ loop3 l))) undefined)
{-
*Test> test3 [1..10]
(3628800,[1,1,2,6,24,120,720,5040,40320,362880])
*Test> test3 ([1..10] ++ [0] ++ [1..10])
(0,[])
*Test>
-}_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
