Lambda the Ultimate

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.

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...

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.

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.

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.

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. ;)

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 '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.

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? :-)

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...