How to remove a dynamic prompt: static and dynamic delimited continuation operators are equally expressible

The report (by Oleg Kiselyov) shows that shift, control, shift0, etc. delimited continuation operators are macro-expressible in terms of each other. The report thus confirms the result first established by Chung-chieh Shan in Shift to Control. The operators shift, control, control0, shift0 are the members of a single parameterized family, and the standard CPS is sufficient to express their denotational semantics.

The report uses a more uniform method and it formally proves that 'control' implemented via 'shift' indeed has its standard reduction semantics. It is common knowledge that first-class continuations are quite tricky -- and delimited continuations are trickier still. Therefore, a formal proof is a necessity.

On the practical side, the report shows the simplest known Scheme implementations of control, shift0 and control0 (similar to `cupto'). The method in the report lets us design 700 more delimited control operators, which compose stack fragments in arbitrary ways.

I love this sort of thing, and since section 4 includes Scheme code, you can try to skip the theory if you find it intimidating.

I know this stuff can look a bit hairy. If there's interest, I hope Oleg would agree to help people new to this sort of material in understanding sections 2 and 3. But you have to ask nicely...

Comment viewing options

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

No interest in delimited continuations?

Thanks for pointing out this paper, Ehud, it is an interesting read.

Dariusz Biernacki and Olivier Danvy have recently found an application of programming with control and prompt that actually takes advantage of the difference between them and static delimited continuations: breadth-first traversal. On the Dynamic Extent of Delimited Continuations.

Another Subject...

...that I'm interested in, but feel utterly incompetent to comment on.

Also, I have to confess that I managed to miss whatever the introduction to "shift," "control," "cupto," etc. was supposed to have been, so a lot of the material I see on delimited continuations means literally nothing to me.

At the moment I'm afraid I'm suffering from overload: I'm trying to work through TAPL and get onto ATITAPL, trying to become conversant in MetaPRL, and trying to become at least conversant enough in monadic programming that State, IO, Resumption, and their composability (via transformers? Coproducts?) become intuitive across languages that I actually use, i.e. not Haskell.

I greatly appreciate everyone's effort to provide yet more interesting material to pursue, even when I don't have anything to add (yet!) to the discussion.

nothing to be afraid of

For all the hushed reverence given to the family of assorted control operators, it's reassuring to note that they're really just the set of combinations of the obvious design choices when you look at the reduction semantics of control operators.

Control operators are one place where an operational semantics really clarifies things--go figure. Here's the semantics for call/cc (all my examples will assume CBV lambda calculus):

C[call/cc v] -> C[(v \x.(abort C[x]))]
C[abort e] -> e

Control operators bring the program context into consideration in the operational semantics. The semantics of call/cc is to apply its (evaluated) argument to a reified representation of the current context C; if the reified continuation is used, it uses abort to abandon whatever context it is currently in and replace it with the original, saved context.

Delimited continuations are about saving and discarding only a portion of the current context. Historically, the idea came about from running code that contains call/cc from a REPL. If the code being executed discards the current context, you don't want it to abort the REPL. You only want it to abort "up to the prompt." So you need a way to install delimiters, like exception handlers, that limit the extent of control effects.

One such mechanism is control and prompt. The semantics relies on a slight refinement of the definition of contexts: we have arbitrary evaluation contexts M, which may contain instances of control effects, and "pure" evaluation contexts C, which contain no instances of control effects. This is just to allow us to express "the innermost occurrences of a control effect."

M[prompt v] -> M[v]
M[prompt C[control f . e]] -> M[prompt e']
  where e' = let f = \x.C[x] in e

What are the differences from call/cc? For one, call/cc doesn't immediately abandon the current context, and in fact has no control effects unless you actually use the captured continuation. By contrast, control immediately abandons the current context (up to the dynamically nearest enclosing prompt). The other difference, of course, is that the context that is abandoned and reified is delimited.

There are several choices to make in the design space for control operators:

  1. Are continuations delimited?
  2. When does the context get abandoned?
  3. Does the delimiter get reinstalled when a control effect occurs (i.e., on the RHS of the second reduction rule above)?
  4. Does the reified continuation get wrapped in another delimiter? (This is the only difference between shift/reset and control/prompt.)

These are the main choices, and trying them in various combinations gets you most of the well-known control operators.

Contexts

I think once you understand what C and M are, you are home free. But I am sure not everyone wnats to discover what they are by guessing...

good point

Yeah, you're right -- and I've never been happy with the standard way people explain program contexts. I think I'll write a tutorial on contexts some time.

The context C[] is more complex than it appears

Dave Herman wrote:

One such mechanism is control and prompt. The semantics relies on a
slight refinement of the definition of contexts: we have arbitrary
evaluation contexts M, which may contain instances of control effects,
and "pure" evaluation contexts C, which contain no instances of
control effects.

That is not entirely correct. The correct definition for the context
C[] is that it does not cross the boundary of an active
prompt. And that's it. That does not mean that C[] is
pure and has no control effects. Let's consider the following

  (+ 1 (reset (begin (shift f (f #f)) (shift g 2))))

Here, the context M[] is (+ 1 []) and the
context C[] is (begin [] (shift g 2)). One
can't call such a context containing no instances of control
effects. Another example:

   (prompt ((control f f)))

Here, the context C[] is ([]) and so
f will be (lambda (x) (x)).
That seems pure enough. Now, let's apply f to another pure value:
(lambda () (control f #f)). And all of the sudden,
(f (lambda () (control f #f))) will have a control effect. The
behavior of the example changes if we replace `control' with shift.

Here's the complete example

  (let ((f (prompt ((control f f)))))
   (prompt (begin (f (lambda () (control f #f))) #t)))
; ==> #f

  (let ((f (reset ((shift f f)))))
   (reset (begin (f (lambda () (shift f #f))) #t)))
; ==> #t

As you can see, delimited continuations are quite tricky, and so one
essentially has to use formal tools. Intuition by itself often fails.
This is not to say that the use of the formal tools is easy: proving
theorems about prompt and control is quite challenging too. The
hardest part is to figure out what exactly is to prove.

yes -- but it's still nothing to fear

That is not entirely correct. The correct definition for the context C[] is that it does not cross the boundary of an active prompt. And that's it. That does not mean that C[] is pure and has no control effects.

Yes, thanks for the clarification. I'm looking for the right level of artful lying, as they say, for a tutorial -- but clearly my explanation was not so artful.

So the notion of purity is just wrong. I should say, as you suggest, that C[] represents contexts in which no active delimiters have been installed, and that this allows us to describe the "innermost" or "most recently installed" delimiter. It would probably also help to make an analogy to exception handlers, since most people have an intuition for that and they can be specified in an operational semantics in exactly the same way.

As you can see, delimited continuations are quite tricky, and so one essentially has to use formal tools. Intuition by itself often fails.

I agree that using delimited continuations can be difficult, and I couldn't agree more that formal tools are the best way to understand them. In fact, that's part of what I was trying to show: these things are made far clearer with an operational semantics than with, say, code samples.

On the other hand, my point was that the world of control operators is not so much a deep, mysterious mine with gems scattered randomly in the muck. Rather, they can all pretty much be derived by trying the various combinations of design decisions. And the design decisions are made clear by the operational semantics.

evaluation contexts

Oleg:That is not entirely correct. The correct definition for the context C[] is that it does not cross the boundary of an active prompt. And that's it.

Perhaps it would be worth spelling out the decomposition of expressions into arbitrary evaluation contexts, delimited evaluation contexts, and potential redexes.

Also, is there any compelling reason to give the C[] delimited evaluation contexts outside-in (in Felleisen and Flatt's terminology), and the M[] arbitrary evaluation contexts inside-out?

Dave Herman:I should say, as you suggest, that C[] represents contexts in which no active delimiters have been installed, and that this allows us to describe the "innermost" or "most recently installed" delimiter. It would probably also help to make an analogy to exception handlers, since most people have an intuition for that and they can be specified in an operational semantics in exactly the same way.

The other intuition which may be useful is the C[] contexts are the defunctionalized continuations of a compositional evaluator, and M[] contexts (after some massaging to require that each reduction always decomposes an expression into M[], C[] and redex; and recognizing that the M[]'s are then lists of C[]'s) are the defunctionalized metacontinuations.

Oleg's simulation of dynamic delimited continuations in terms of shift and reset can be seen in light of the continuation-passing evaluator (or equivalently the CPS transformer) for shift and reset, and that makes the trampolining jump right out (to me at least).

On the other hand, my point was that the world of control operators is not so much a deep, mysterious mine with gems scattered randomly in the muck. Rather, they can all pretty much be derived by trying the various combinations of design decisions.

What you describe sounds like a uniform muck. Just because it's possible to enumerate all the possibilities doesn't mean that there aren't any gems in the muck. ;)

Useful context

This thread is good background reading. (sorry about the pun, I couldn't help myself)

Use in Web applications

A while back I wrote a short note on how partial continuations could be used in web applications. I used 'splitter' in this case:

http://www.double.co.nz/scheme/partial-continuations/partial-continuations.html

Nice

Thank you for that example.

The question I would like to ask (OK, I'm asking it) is why you chose dynamic delimited continuations. And why you chose "splitter" instead of one of the myriad other possibilities?

Since your example does not make use of the dynamicity of splitter, it could be simplified with static delimited continuations:

;;; replace:
; (define current-mark #f)
;;; with:
; nothing

;;; replace:
; (define (click-web-url url)
;   (splitter
;     (lambda (mark)
;       (set! current-mark mark)
;       ((url->continuation url) mark)))
;   (display "Exiting click-web-url\n"))
;;; with:
(define (click-web-url url)
  ((url->continuation url) #f)
  (display "Exiting click-web-url\n"))

;;; replace:
; (define (show page-function)
;   (call/pc
;    current-mark
;    (lambda (pk)
;      (let ((url (continuation->url pk)))
;        (page-function url)
;        (abort current-mark (lambda () #f)))))
;   (display "User returned from url...\n"))
;;; with:
(define (show page-function)
  (shift pk
    (let ((url (continuation->url pk)))
      (page-function url)))
  (display "User returned from url...\n"))

;;; replace:
; (define (start-web-example thunk)
;   (click-web-url
;     (continuation->url (lambda (ignore) (thunk)))))
;;; with:
(define (start-web-example thunk)
  (click-web-url
    (continuation->url (lambda (ignore) (reset (thunk))))))

It's not tested, other than on your example, but I think it's the same.

I was reading the paper about

I was reading the paper about 'splitter' at the time as worked through the article to help with my understanding of it. At the end I realised that the code wasn't simplified much due to having to store the 'current-mark'. Afterwards I did more reading on shift/reset and realised it would make things easier in that regard. I briefly mention that with the other operators things might be cleaner.

Although if shift/reset is used then it would mean code written by the user of the web framework may not be able to use shift/reset as nesting the calls might prevent the framework from using the right 'reset' point. Is that correct? I haven't really explored that possibility in detail.

System/user border

I believe a whole class of applications of delimited continuations is protecting the system's foot from user's gun (you wouldn't want to give call/cc to your children).

More specific examples include: separating scheduler from scheduled threads, persister from persisted objects, OS from processes, J2EE container from EJBs... err, the last one is a bad example :-)

OTOH, can we generalize it further: are delimited continuations useful for mutually untrusting processes? Should we sell this to erights people? :-)

Categorical Structure of Continuation

Myself: Should we sell this to erights people?

Categorical Structure of Continuation is an interesting reading by itself, but it also discusses, how dynamic control operators (namely prompt and abort) in some sense violate visibility of names. This can be seen as unfriendliness to capabilities...