A Monadic Framework for Subcontinuations

A Monadic Framework for Subcontinuations

Functional and delimited continuations are more expressive than traditional
abortive continuations and they apparently seem to require a framework
beyond traditional continuation or monadic semantics. We show that this is not the
case: standard continuation semantics is sufficient to explain directly the common
control operators for delimited continuations. This implies a monadic framework for
typed and encapsulated functional and delimited continuations which we design and
implement as a Haskell library.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Deja vu

I seem to remember noticing this paper cited on LtU, but am unable to locate that citation. Strange.

Can't see where the paper was linked.

There was an older paper by some of the same authors on Subcontinuations was posted. [Edit note: But I see you refered to that in another recent post]

Glitches in the Matrix

Well, then I guess I planned to cite it myself and forgot about this fact. After posting about the older paper on subcontinuations I decided it would be good to share a link to this one.

I highly recommend it, it really looks like the GUT of control operators (at least to my non-academical sight).

I particularly enjoyed factoring of semantics into two parts, of which one deals with concrete representation of continuations, while the other - with concrete representation of metacontinuations. A real eye-opener (for me).

There's some paper by Steele

There's some paper by Steele proving that all control operators can be implemented by continuations, or so I've heard. Continuations were invented as a way of giving control operators in Algol a formal semantics.

You'd need some state

...in addition to first-class continuations to express at least the most popular control operators. Some channels, or even reference cells. At least one.

Or a reader monad

I suspect you're talking about more complex examples, but I was able to implement the control operators given as examples in the earlier part of the paper by using a CC monad wrapped with a reader monad transformer.

class Monad m => MonadCC p sk m | m -> p sk where
	newPrompt   :: m (p a)
	pushPrompt  :: p a -> m a -> m a
	withSubCont :: p b -> (sk a b -> m b) -> m a
	pushSubCont :: sk a b -> m a -> m b


withCont :: (MonadCC p sk m, MonadReader (p ans) m) => (sk a ans -> m ans) -> m a
withCont e = ask >>= \p -> withSubCont p (\k -> pushPrompt p (e k))

reifyA :: (MonadCC p sk m, MonadReader (p ans) m) => sk a ans -> m a -> m b
reifyA k v = withCont (\_ -> pushSubCont k v)

callcc :: (MonadCC p sk m, MonadReader (p ans) m) =>
	((forall b. m a -> m b) -> m a) -> m a
callcc f = withCont (\k -> pushSubCont k (f (reifyA k)))


Although this paper requires some background, I think it can serve as a good example for understanding monads. Section 4.1 (and figure 8), clearly show how monads simply express and enforce sequencing.

Back to reading

But I still have to understand, why some of the authors suddenly forgot about concurrency issues that were raised in the previous subcontinuations papers. Are forks and parallel-ors already covered, or will they require replacing a sequence as a representation of metacontinuations with a tree, or something more painful? I have to follow my own advice on reading papers, and just go and re-read it.

Why 4 operators?

Another question to myself.

Why Gunter et al. employ just 3 control constructs, while this paper defines 4?

Is it a matter of usability, or all four are strictly necessary?

They're the same

Except that they don't require delimited continuations to be represented as functions, so they use "pushSubCont" to apply them instead of function application.

There is a note to that effect at the top of page 4.