Continuations and term-rewriting calculi

Thinking is most mysterious, and by far the greatest light upon it that we have is thrown by the study of language.

— Benjamin Lee Whorf.

In this post, I hope to defuse the pervasive myth that continuations are intrinsically a whole-computation device.  They aren't.  I'd originally meant to write about the relationship between continuations and delimited continuations, but find that defusing the myth is prerequisite to the larger discussion, and will fill up a post by itself.

To defuse the myth, I'll look at how continuations are handled in the vau-control-calculus.  Explaining that calculus involves explaining the unconventional way vau-calculi handle variables.  So, tracing back through the tangle of ideas to find a starting point, I'll begin with some remarks on the use of variables in term-rewriting calculi.

While I'm extracting this high-level insight from the lower-level math of the situation, I'll also defuse a second common misapprehension about continuations, that they are essentially function-like.  This is a subtle point:  continuations are invoked as if they were functions, and traditionally appear in the form of first-class functions, but their control-flow behavior is orthogonal to function application.  This point is (as I've just demonstrated) difficult even to articulate without appealing to lower-level math; but it arises from the same lower-level math as the point about whole-computation, so I'll extract it here with essentially no additional effort.

Contents
Partial-evaluation variables
Continuations by global rewrite
Control variables
Insights

Partial-evaluation variables

From the lasting evidence, Alonzo Church had a thing about variables.  Not as much of a thing as Haskell Curry, who developed a combinatorial calculus with no variables at all; but Church did feel, apparently, that a meaningful logical proposition should not have unbound variables in it.  He had an elegant insight into how this could be accomplished:  have a single binding construct —which for some reason he called λ— for the variable parameter in a function definition, and then —I quite enjoyed this— you don't need additional binding constructs for the existential and universal quantifiers, because you can simply make them higher-order functions and leave the binding to their arguments.  For his quantifiers Π and Σ, Π(F,G) meant for all values v such that F(v) is true, G(v) is true; and Σ(F) meant there exists some value v such that F(v) is true.  The full elegance of this was lost because only the computational subset of his logic survived, under the name λ-calculus, so the quantifiers fell by the wayside; but the habit of a single binding construct has remained.

In computation, though, I suggest that the useful purpose of λ-bound variables is partial evaluation.  This notion dawned on me when working out the details of elementary vau-calculus.  Although I've blogged about elementary vau-calculus in an earlier post, there I was looking at a different issue (explicit evaluation), and took variables for granted.  Suppose, though, that one were centrally concerned only with capturing the operational semantics of Lisp (with fexprs) in a term-rewriting calculus at all, rather than capturing it in a calculus that looks as similar as possible to λ-calculus.  One might end up with something like this:

T   ::=   S | s | (T . T) | [wrap T] | A
A   ::=   [eval T T] | [combine T T T]
S   ::=   d | () | e | [operative T T T T]
e   ::=   ⟪ B^* ⟫
B   ::=   s ← T

Most of this is the same as in my earlier post (explicit evaluation), but there are three differences:  the internal structure of environments (e) is described; operatives have a different structure, which is fully described; and there are no variables.

Wait.  No variables?

Here, a term (T) is either a self-evaluating term (S), a symbol (s), a pair, an applicative ([wrap T], where T is the underlying combiner), or an active term (A).  An active term is the only kind of term that can be the left-hand side of a rewrite rule: it is either a plan to evaluate something in an environment, or a plan to invoke a combiner with some operands in an environment.  A self-evaluating term is either an atomic datum such as a number (d), or nil, or an environment (e), or an operative — where an operative consists of a parameter tree, an environment parameter, a body, and a static environment.  An environment is a delimited list of bindings (B), and a binding associates a symbol (s) with an assigned value (T).

The rewrite rules with eval on the left-hand side are essentially just the top-level logic of a Lisp evaluator:

[eval S e]   →   S
[eval s e]   →   lookup(s,e)     if lookup(s,e) is defined
[eval (T₁ . T₂) e]   →   [combine [eval T₁ e] T₂ e]
[eval [wrap T] e]   →   [wrap [eval T e]]

That leaves two rules with combine on the left-hand side:  one for combining an applicative, and one for combining an operative.  Combining applicatives is easy:

[combine [wrap T₀] (T₁ ... T_n) e]   →   [combine T₀ ([eval T₁ e] ... [eval T_n e]) e]

Combining operatives is a bit more complicated.  (It will help if you're familiar with how Kernel's $vau  works; see here.)  The combination is rewritten as an evaluation of the body of the operative (its third element) in a local environment.  The local environment starts as the static environment of the operative (its fourth element); then the ordinary parameters of the operative (its first element) are locally bound to the operands of the combination; and the environment parameter of the operative (its second element) is locally bound to the dynamic environment of the combination.

[combine [operative T₁ T₂ T₃ T₄] V e]   →   [eval  T₃  match(T₁,V) · match(T₂,e) · T₄]     if the latter is defined

where match(X,Y) constructs an environment binding the symbols in definiend X to the corresponding subterms in Y;  e_child · e_parent  concatenates two environments, producing an environment that tries to look up symbols in e_child, and failing that looks for them in e_parent;  and a value (V) is a term such that every active subterm is inside a self-evaluating subterm.

Sure enough, there are no variables here.  This calculus behaves correctly.  However, it has a weak equational theory.  Consider evaluating the following two expressions in a standard environment e₀.

[eval  ($lambda (x) (+ 0 x))  e₀]
[eval  ($lambda (x) (* 1 x))  e₀]

Clearly, these two expressions are equivalent; we can see that they are interchangeable.  They both construct an applicative that takes one numerical argument and returns it unchanged.  However, the rewriting rules of the calculus can't tell us this.  These terms reduce to

[wrap [operative  (x)  #ignore  (+ 0 x)  e₀]]
[wrap [operative  (x)  #ignore  (* 1 x)  e₀]]

and both of these terms are irreducible!  Whenever we call either of these combiners, its body is evaluated in a local environment that's almost like e₀; but within the calculus, we can't even talk about what will happen when the body is evaluated.  To do so we would have to construct an active evaluation term for the body; to build the active term we'd need to build a term for the local environment of the call; and to build a term for that local environment, we'd need to bind x to some sort of placeholder, meaning "some term, but we don't know what it is yet".

A variable is just the sort of placeholder we're looking for.  So let's add some syntax.  First, a primitive domain of variables.  We call this domain x_p, where the "p" stands for "partial evaluation", since that's what we want these variables for (and because, it turns out, we're going to want other variables that are for other purposes).  We can't put this primitive domain under nonterminal S because, when we find out later what a variable stands for, what it stands for might not be self-evaluating; nor under nonterminal A because what it stands for might not be active.  So x_p has to go directly under nonterminal T.

T   ::=   x_p

We also need a binding construct for these variables.  It's best to use elementary devices in the calculus, to give lots of opportunities for provable equivalences, rather than big monolithic devices that we'd then be hard-put to analyze.  So we'll use a traditional one-variable construct, and expect to introduce other devices to parse the compound definiends that were handled, in the variable-less calculus, by function match.

S   ::=   ⟨λ x_p.T⟩

governed by, essentially, the usual β-rule of λ-calculus:

[combine ⟨λ x_p.T⟩ V e]   →   T[x_p ← V]

That is, combine a λ-expression by substituting its operand (V) for its parameter (x_p) in its body (T).  Having decided to bind our variables x_p one at a time, we use three additional operative structures to deliver the various parts of the combination one at a time (a somewhat souped-up version of currying):  one structure for processing a null list of operands, one for splitting a dotted-pair operand into its two halves, and one for capturing the dynamic environment of the combination.

S   ::=   ⟨λ₀.T⟩ | ⟨λ₂.T⟩ | ⟨ε.T⟩

The corresponding rewrite rules are

[combine ⟨λ₀.T⟩ () e]   →   T
[combine ⟨λ₂.T₀⟩ (T₁ . T₂) e]   →   [combine [combine T₀ T₁ e] T₂ e]
[combine ⟨ε.T₀⟩ T₁ e]   →   [combine [combine T₀ e ⟪⟫] T₁ e]

Unlike the variable-less calculus, where the combine rewrite rule initiated evaluation of the body of an operative, here evaluation of the body must be built into the body when the operative is constructed.  This would be handled by the δ-rules (specialized operative-call rewrite rules) for evaluating function definitions.  For example, for variables x,y and standard environment e₀,

[eval ($lambda (x) (+ 0 x)) e₀]   →⁺   [wrap ⟨ε.⟨λy.⟨λ₂.⟨λx.⟨λ₀.[eval  (+ 0 x)  ⟪x ← x⟫ · e₀]⟩⟩⟩⟩⟩]

Variable y is a dummy-variable used to discard the dynamic environment of the call, which is not used by ordinary functions.  Variable x is our placeholder, in the constructed term to evaluate the body, for the unknown operand to be provided later.

The innermost redex (reducible expression) here, [eval  (+ 0 x)  ⟪x ← x⟫ · e₀], can be rewritten through a series of steps,

[eval  (+ 0 x)  ⟪x ← x⟫ · e₀]
    →   [combine  [eval  +  ⟪x ← x⟫ · e₀]  (0 x)  ⟪x ← x⟫ · e₀]
    →   [combine  [wrap +]  (0 x)  ⟪x ← x⟫ · e₀]
    →⁺ [combine  +  (0 x)  ⟪x ← x⟫ · e₀]

Where we can go from here depends on additional information of one or another kind.  We may have a rule that tells us the addition operative + doesn't use its dynamic environment, so that we can garbage-collect the environment,

    →   [combine  +  (0 x)  ⟪⟫]

If we have some contextual information that the value of x will be numeric, and a rule that zero plus any number is that number back again, we'd have

    →   x

At any rate, we only have the opportunity to even start the partial evaluation of the body, and contemplate these possible further steps, because the introduction of variables allowed us to write a term for the partial evaluation in the first place.

[edit:  I'd goofed, in this post, on the combination rule for λ₀; it does not of course induce evaluation of T.  Fixed now.]

Continuations by global rewrite

The idea of using λ-calculus to model programming language semantics goes back at least to Peter Landin in the early 1960s, but there are a variety of programming language features that don't fit well with λ-calculus.  In 1975, Gordon Plotkin proposed a remedy for one of these features — eager argument evaluation, whereas ordinary λ-calculus allows lazy argument evaluation and thereby has different termination properties.  Plotkin designed a variant calculus, the λ_v-calculus, and proved that on one hand λ_v-calculus correctly models the semantics of a programming language with eager argument evaluation, while on the other hand it is comparably well-behaved to traditional λ-calculus.  Particularly, the calculus rewriting relation is compatible and Church-Rosser, and satisfies soundness and completeness theorems relative to the intended operational semantics.  (I covered those properties and theorems a bit more in an earlier post.)

In the late 1980s, Matthias Felleisen showed that a technique similar to Plotkin's could be applied to other, more unruly kinds of programming-language behavior traditionally described as "side-effects":  sequential control (continuations), and sequential state (mutable variables).  This bold plan didn't quite work, in that he had to slightly weaken the well-behavedness properties of the calculus.  In both cases (control and state), the problem is to distribute the consequences of a side-effect to everywhere it needs to be known; and Felleisen did this by having special constructs that would "bubble up" through the term, carrying the side-effect with them, until they encompassed the whole term, at which point there would be a whole-term rewriting rule to distribute the side-effect to everywhere it needed to go.  The whole-term rewriting rules were the measure by which the well-behavedness of the calculus would fail, as whole-term rewriting isn't compatible.

For sequential control (our central interest here), Felleisen added two operators, C and A, to λ_v-calculus.  The syntax of λ_v-calculus, before the addition, is just that of λ-calculus:

T   ::=   x | (λx.T) | (TT)

In place of the classic β-rule of λ-calculus, λ_v-calculus has β_v, which differs in that the operand in the rule is a value (redexes have to be inside λ-terms):

((λx.T)V)   →   T[x ← V]

The operational semantics, which acts only on whole terms, uses (per Felleisen) an evaluation context E to uniquely determine which subterm is reduced:

E   ::=   ⎕ | (ET) | ((λx.T)E)

E[((λx.T)V)]   ↦   E[T[x ← V]]

For the control calculus, the term syntax adds A and C,

T   ::=   x | (λx.T) | (TT) | (AT) | (CT)

Neither of these operators has the semantics of call-with-current-continuation.  Instead, (AT) means "abort the surrounding computation and just do T", while (CT) means "abort the surrounding computation and apply T to the (aborted) continuation".  Although it's possible to build conventional call-with-current-continuation out of these primitive operators, the primitives themselves are obviously intrinsically whole-term operators.  Operationally, evaluation contexts don't change at all, and the operational semantics has additional rules

E[(AT)]   ↦   T
E[(CT)]   ↦   T(λx.(AE[x]))    for unused variable x

The compatible rewrite relation, →, has rules to move the new operators upward through a term until they reach its top level.  The compatible rules for A are dead easy:

(AT₁)T₂   →   AT₁
V(AT)   →   AT

Evidently, though, once the A operator reaches the top of the term, the only way to get rid of it, so that computation can proceed, is a whole-term rewrite rule,

AT   ᐅ   T

The whole-term rule for C is easy too,

CT   ᐅ   T(λx.(Ax))

but the compatible rewrite rules for C are, truthfully, just a bit frightening:

(CT₁)T₂   →   C(λx₁.(T₁(λx₂.(A(x₁(x₂T₂))))))    for unused x_k
V(CT)   →   C(λx₁.(T(λx₂.(A(x₁(Vx₂))))))    for unused x_k

This does produce the right behavior (unless I've written it out wrong!), but it powerfully perturbs the term structure; Felleisen's description of this as "bubbling up" is apt.  Imho, it's quite a marvelous achievement, especially given the prior expectation that nothing of the kind would be possible — an achievement in no way lessened by what can now be done with a great deal of hindsight.

The perturbation effect appears to me, in retrospect, to be a consequence of describing the control flow of continuations using function-application structure.  My own approach makes no attempt to imitate function-application and, seemingly as a result, its constructs move upward without the dramatic perturbation of Felleisen's C.

Various constraints can be tampered with to produce more well-behaved results.  Felleisen later proposed to adjust the target behavior — the operational semantics — to facilitate well-behavedness, in work considered formative for the later notion of delimited continuations.  The constraint I've tampered with isn't a formal condition, but rather a self-imposed limitation on what sort of answers can be considered:  I introduce a new binding construct whose form doesn't resemble λ, and whose rewriting rules use a different substitution function than the β-rule.

Control variables

Consider the following Scheme expression:

(call/cc (lambda (c) (c 3)))

Presuming this is evaluated in an environment with the expected binding for call/cc, we can easily see it is operationally equivalent to 3.  Moreover, our reasoning to deduce this is evidently local to the expression; so why should our formalism have to rewrite the whole surrounding term (perturbing it in the process) in order to deduce this?

Suppose, instead of Felleisen's strategy of bubbling-up a side-effect to the top level of a term and then distributing it from there, we were to bubble-up (or, at least, migrate up) a side-effect to some sort of variable-binding construct, and then distribute it from there by some sort of substitution function to all free occurrences of the variable within the binding scope.  The only problem, then, would be what happens if the side-effect has to be distributed more widely than the given scope — such as if a first-class continuation gets carried out of the subterm in which it was originally bound — and that can be solved by allowing the binding construct itself to migrate upward in the term, expanding its scope as much as necessary to encompass all instances of the continuation.

I did this originally in vau-calculus, of course, but for comparison with Felleisen's A/C, let's use λ_v-calculus instead.  Introduce a second domain of control variables, x_c, disjoint from x_p, and "catch" and "throw" term structures (κx.T) and (τx.T).

T   ::=   x_p | (TT) | (λx_p.T) | (κx_c.T) | (τx_c.T)

Partial-evaluation variables are bound by λ, control variables are bound by κ (catch).  Control variables aren't terms; they can only occur free in τ-expressions, where they identify the destination continuation for the throw.  κ and τ are evaluation contexts; that is,

E   ::=   ... | (κx.E) | (τx.E)

The rewrite rules for τ are pretty much the same as for Felleisen's A, except that there is now a compatible rewrite rule for what to do once the throw reaches its matching catch, rather than a whole-term rewrite for eliminating the A once it reaches the top of the term.

(τx.T₁)T₂   →   τx.T₁
V(τx.T)   →   τx.T
κx.(τx.T)   →   κx.T

What about rewrite rules for κ?  One simple rule we need, in order to relate expressions with κ to expression without, is "garbage collection":

κx.T   →   T    if x does not occur free in T

We also want rules for κ to migrate upward —non-destructively— when it occurs in an evaluation context; but κ may be the target of matching τ expressions, and if we move the κ without informing a matching τ, that τ will no longer do what it was meant to.  Consider a κ, poised to move upward, with a matching τ somewhere in its body (embedded in some context C that doesn't capture the control variable).

V(κx.C[τx.T])

If C happens to be an evaluation context, then it is possible for the τ to move upward to meet the κ and disappear; and, supposing x doesn't occur free in T, we'd have (VT).  Even if C isn't an evaluation context, (τx.T) thus represents the potential to form (VT).  If we move the κ over the V, then, in order for the τ to still represent the same potential it did before, we'd have to change it to (τx.(VT)).  And this has to happen for every matching τ.  So let's fashion a substitution function for control variables, T[x ← C] where C doesn't capture any variables:

y[x ← C]   →   y
(T₁T₂)[x ← C]   →   ((T₁[x ← C])(T₂[x ← C]))
(λy.T)[x ← C]   →   (λy.(T[x ← C]))    where y isn't free in C
(κy.T)[x ← C]   →   (κy.(T[x ← C]))    where y isn't x or free in C
(τy.T)[x ← C]   →   (τy.(T[x ← C]))    if y isn't x
(τx.T)[x ← C]   →   (τx.C[T[x ← C]])

The "where" conditions are met by α-renaming as needed.  Now we're ready to write our rewrite rules for moving κ upward:

(κx.T₁)T₂   →   κx.(T₁[x ← ⎕T₂] T₂)    where x isn't free in T₂
V(κx.T)   →   κx.(V(T[x ← V⎕]))    where x isn't free in V
κy.(κx.T)   →   κy.(T[x ← y])

As advertised, κ moves upward without perturbing the term structure (contrast with the bubbling-up rules for C).  If we need a first-class continuation, we can simply wrap τ in λ:  (λy.(τx.y)).  The δ-rule for call/cc would be

(call/cc T)   →   κx.(T(λy.(τx.y)))    for unused x

If this occurs in some larger context, and the first-class continuation escapes into that larger context, then the matching κ will have had to move outward before it over some evaluation context E, and substitutions will have transformed the continuation to (λy.(τx.E[y])).

Insights

The orthogonality of continuation control-flow to function application is, in the lower-level math, rather explicitly demonstrated by the way κ moves smoothly upward through the term, in contrast to the perturbations of the bubbling-up rules for C as it forcibly interacts with function-application structure.  The encapsulation of a τ within a λ to form a first-class continuation seals the deal.

The notion that continuations are a whole-term phenomenon —or, indeed, that any side-effect is a whole-term phenomenon— breaks down under the use of floating binding-constructs such as κ, which doesn't require the side-effect to remain encapsulated within a particular subterm, but does allow it to do so and thus allows local reasoning about it to whatever extent its actual behavior remains local.  Whether or not that makes traditional continuations "undelimited" is a question of word usage:  the κ binding-construct is a delimiter, but a movable one.

As a matter of tangential interest here, the vau-calculus handling of sequential state involves two new kinds of variables and four new syntactic constructs (two of which are binders, one for each of the new kinds of variables).  Here's a sketch:  Mutable data is contained in symbol-value assignments, which in turn are attached to environments; the identity of an environment is a variable, and its binding construct defines the region of the term over which that environment may be accessible.  Assignments are a separate, non-binding syntactic construct, which floats upward toward its matching environment-binding.  When a symbol is evaluated in an environment, a pair of syntax elements are created at the point of evaluation:  a query construct to seek an assignment for the given symbol in the given environment, which binds a query-variable, and within it a matching result construct with a free occurrence of the query-variable.  The result construct is an indivisible term.  The query is a compound, which migrates upward through the term looking for an assignment for the symbol in the environment.  When the query encounters a matching assignment, the query is annihilated (rather as a τ meeting its matching κ), while performing a substitution that replaces all matching result-constructs with the assigned value (there may by this time be any number of matching result-constructs, since the result of the original lookup may have been passed about in anticipation of eventually finding out what its value is).

As a final, bemusing note, there's a curious analogy (which I footnoted in my dissertation) between variables in the full side-effectful vau-calculus, and fundamental forces in physics.  The four forces of nature traditionally are gravity, electromagnetism, strong nuclear force, and weak nuclear force; one of these —gravity— is quite different from the others, with a peculiar sort of uniformity that the others lack (gravity is only attractive).  Whilst in vau-calculus we have four kinds of variables (partial-evaluation, control, environment, and query), of which one —partial-evaluation— is quite different from the others, with a peculiar sort of uniformity that the others lack (each of the other kinds of variable has an α-renaming substitution to maintain hygiene, and one or more separate kinds of substitution to aid its purpose in rewriting; but partial-evaluation variables have only one kind of substitution, of which α-renaming is a special case).

[Note: I later explored the physics analogy in a separate post, here.]

Guarded continuations

Go to, let us go down, and there confound their language, that they may not understand one another's speech.

— Genesis 11:7 (King James Version)

I've been asked about Kernel's guarded continuations.  In writing that section of the Kernel Report, I knew it wasn't as lucid as one might like, but getting it all down while I had it clearly in mind was something of an achievement in itself.  I'm not sure I've ever seen a really lucid explanation of continuations; explaining them should probably be considered a major challenge in its own right, above and beyond figuring out how the mechanism should work.  It's high time I tried to do better, though; however many tries it takes to get the explanation to come clear, I won't get there if my number of tries never increases.

On my Kernel web page I describe guarded continuations as 'Exception handling "done right"'.  For an ultra-short tag line, that may be about as good as any; but guarded continuations are more a simultaneous blend-and-improvement on Scheme continuations and Java exception handling, rather than a supposedly-optimal exception facility.  We may still be several generations of exception facilities away from getting exceptions right; but as may be, I think guarded continuations have something to add to the discussion.

It's also worth saying up front that guarded continuations are lower-level than a good exception facility would be.  Kernel tries for very simple low-level facilities plus the ability to build higher-level abstractions from them.  It's an open, and fascinating, question how well Kernel's abstraction facilities will actually apply to exception handling — and I hope to learn a lot from that question.  (I expect shortcomings of Kernel's abstractive facilities to be not about the facilities' power (which I maintain is extraordinary) but about the directions in which that power can be applied.  When I figure out what the missing directions are, I mean to go that way.)

Stacks and trees

Classically, programming languages deal with function calls using a stack.  There are two kinds of stuff on the stack:  local variables (data), and return addresses (control).  The local data for a function call produces a single set of local variables; but the algorithm for that same call may produce many different return addresses, one for each point in the algorithm where it, in turn, calls a function.  In principle, one might have two stacks, one for data and one for control; but classically, all local variables and all return addresses are use-once, to be discarded in the same order they were introduced, so it may seem natural to store both on a single stack (with resultant security problems, malware accessing data as control and vice versa).

First-class (lexically scoped) functions require local data to be stored, in general, as a tree rather than a stack.  When a first-class function is returned as the result of a function call (in vintage parlance, as an upward funarg), lexical scoping expects that function to have access to —in general— the entire column of variables that were on the stack when the function was created, even though some of the function calls that created those variables have since ended.  So data that used to be popped off the stack must now, potentially, persist.  A set of local variables, which used to be the data part of a stack frame, is now an environment, with a fixed set of ancestors (variables further up the column) and potentially any number of children (one for each call to any function defined in that environment).  (In Kernel, btw, environments are first-class objects; there was a lively LtU discussion on first-class environments, here.)

First-class continuations do to the control stack what first-class functions did to the data stack:  they turn it into a tree.  (First-class continuations do this to the data stack too, but I'm not aware of any language that has first-class continuations without first-class functions.)  Just as first-class functions required entire columns of local variables to persist after the ends of function calls that created them, first-class continuations require entire columns of "return addresses" to persist after the ends of function calls that created them.

In visualizing the tree of continuations, the actual algorithms of the program hover in the areas beneath the nodes of the tree (possibly, multiple algorithms under a single node).  Each child continuation is a socket waiting for a value to be plugged into it, to be chewed on by the algorithm above that child — which may, eventually, terminate and plug a value into its parent continuation.  Primitive operations hover beneath the leaves of the tree.  Kernel pretty much only needs one non-primitive operation: combination evaluation, which spins off a subtree to evaluate the operator, spins off subtrees as appropriate to evaluate operands, and finally hands the situation over to another algorithm to make the operative call (using for the operative call its parent continuation, in properly tail-recursive fashion).

Guards

When a function f calls another function g, f gives up some of its ability to regulate the future evolution of the computation.  The programmer tends to assume that not all such power has been lost — that  (1) the call to g won't terminate without control passing back through the point at which f called it, and  (2) that particular call to g won't return through that point more than once.  In the presence of first-class continuations, though, even these weak assumptions needn't hold.  Once f calls g, the dynamic extent of that call might be exited, and/or later reentered any number of times, in ways that bypass f entirely.  Perhaps f opens a file, calls g, and then closes the file before relinquishing control to whoever called f; if g terminates bypassing f, the file might not be closed outside the call to f, and if g is reentered bypassing f, the file might not be open inside the call to g.

Scheme addresses this sort of problem by means of dynamic-wind, a device that causes specified actions to be performed whenever a continuation-call tries to enter or leave the dynamic extent of the call to g.  In R5RS Scheme (the version Kernel primarily diverged from), there were a couple of problems with dynamic-wind.

• Although dynamic-wind allowed something to be done every time the dynamic extent of the call to g was entered, and every time it was exited, these before and after actions were unable to observe (let alone affect) what value was being passed into or out of the dynamic extent, so failing to support context-sensitive regulation of access to/from the dynamic extent.  (In Javascript terms <shudder>, before and after are akin to finally rather than catch.)
• The R5RS was explicitly baffled by what would happen if continuations were used to pass into or out of the dynamic extents of the calls to before and after — which suggested to me that the whole thing was something of a kludge.  The correct behavior in such cases ought to follow naturally from the conceptual framework, and if it didn't follow naturally one had to wonder if the conceptual framework was altogether coherent.

Java exception handling differs from this arrangement in several ways.

• Mostly obviously and trivially, it only allows exiting a dynamic extent, not reentering one.
• An intercepting catch has access to the value being thrown (unlike the after of dynamic-wind).
• A catch selectively intercepts throws, based on the "target" (one might even say, "destination") of the throw.  Whereas Lisp cleanly separates the target of an abnormal transfer of control from the value being transferred —the continuation called, versus the value passed to it— Java entangles them in a single thrown object whose type is the "target".
• Once a Java exception is caught, that's the end of the exception unless it is explicitly rethrown — in contrast to the after of dynamic-wind, which ordinarily does not disrupt the abnormal transfer of control during which it is called.

Interestingly, one fairly intricate characteristic shared by both Scheme's dynamic-wind and Java's catch is that the target is a node of a tree.  This is, perhaps, all the more interesting since the trees are seemingly very different in nature.  The Java target is a type in a tree of exception types; the Scheme target is a continuation in a tree of continuations.

Kernel's guarded continuations drew on both these models for inspiration.  An applicative guard-continuation allows the construction of a continuation with entry- and exit-guard clauses.  Exit-guard clauses selectively intercept continuation-calls from inside to outside the guarded dynamic extent (the branch of the continuation tree descending from the guarded continuation), and are therefore analogous to Java catch clauses, with some adjustments.  Entry-guard clauses are symmetrically designed to selectively intercept continuation-calls from outside to inside the guarded extent.

Each guard clause has a selector continuation.  Keep in mind that a continuation-call has two ends:  it goes from one point in the continuation-tree to another, and in this case we know that one end of the call is inside the guarded extent, while the other end is outside.  A continuation-call matches the selector of a clause just if the outside end of the call lies within the tree branch descending from the selector.  For an exit-guard clause this means that the called continuation must be in the selector's branch of the tree.  For an entry-guard, the starting point of the continuation-call must be within the selector's branch of the tree.

Because entry guards are selected based on the source of the continuation-call, a list of interceptors selected when the continuation-call is initiated will be different, in general, from what one would get by stopping at some intermediate interceptor and then "rethrowing" the call (in Java catch style).  This suggests that normal termination of an intercepting guard should continue along the path of the original continuation-call, reserving explicit diversion for when the interceptor doesn't want to follow the original path.  Secondarily, although we do want it to be convenient (as well as possible) for an interceptor to continue along the path of the original continuation-call, we don't really want to give the interceptor first-class continuations for either end of the call (source or destination).  We may have built some abstract device on top of the continuation primitives, and as a result, the source/destination continuations may be internal details that really oughtn't be casually spread about.

Therefore, normal termination of an intercepting guard continues along the path of the continuation-call, and the interceptor when called is provided with an explicit continuation for diverting control to just outside the guarded extent (Java-style).

For versatile guard selection, each guarded gateway (entry or exit for a dynamic extent) has a list of guard clauses.  When a continuation-call goes through the gate (entering or exiting), the selectors of these clauses are checked, one at a time, until one is found that matches the call, or until there are no more clauses so that no interception occurs.  No more than one clause is selected.  A root continuation is provided, which can be used as a selector that matches all possible calls.  Using the root continuation, plus the ability for an interceptor to continue along the continuation-call path, one can (for example) arrange that a clause will be selected except when the call matches some narrower selector (for example, the error continuation, which is the ancestor of all evaluation-aborting error handlers).  One provides a clause that catches errors and causes them to continue along their path, followed by a clause that catches everything and does whatever it is one wants done only in non-error situations.

When a continuation-call is made, a list of intercepting guard clauses can be immediately constructed, since continuation guards are fixed at the time the guarded continuation is constructed.  The list doesn't have to be constructed then, of course, exactly because all the relevant parts of the continuation tree are immutable; but if it isn't constructed immediately, one will have to store the information needed to select the clauses later — which includes the source of the call as well as its destination (destination to select exit guards, source to select entry guards).

The Kernel Report carefully works out subtleties of the device, such that when a guard intercepts an entry/exit to dynamic extent d, and then itself makes a continuation-call, that call does not select any guard on d.

The traditional Scheme device for acquiring a first-class continuation object is call/cc, which calls a procedure and passes to that procedure the continuation to which that call would normally return.  Frankly, this was always a very clumsy way to work with continuations; one might almost suspect it was devised as an "esoteric programming language" feature, akin to INTERCAL's COME FROM statement.  With guarded continuations, though, dependence on call/cc finally becomes untenable.  If I'm working in Java, and I want to create a new class of exception, I do that by adding a subtype to the tree of exception types; to do the same thing in Kernel, it seems I want to add a new continuation to the tree branch of continuations descending from the error continuation.  If I had to use call/cc to acquire continuations, I could only add a new descendant of the error continuation if I were actually in the dynamic extent of the error continuation — so, to define a new "type" of error during normal computation, I'd have to first "throw" an error exception, passing through all the exit- and entry-guards to get to the point in the tree where I want to add the new continuation.  What's wanted is ability to add a child continuation to an existing continuation without having to be inside the dynamic extent of the parent.  Kernel provides just that ability, with extend-continuation (to add some algorithm between child and parent) and guard-continuation (to add guards between child and parent).  (Interestingly, call/cc still has to be provided as a primitive, since it can't be derived from the other primitives.)

An illustrative example

Alas, no.  Source code for continuation guarding is generally bulky and hard to read, and attempting to illuminate the basic concepts of continuation guarding that way would more likely just create an unhelpful mess.  For me, at least, it's all best understood by visualizing the tree of nested dynamic scopes, whereas the source code only directly reveals a tree of nested static syntax; the dynamic tree then has to be deduced, and the two trees don't correspond as closely as one might think.

How best to arrange for a clear illustration, I'll have to give some more thought.  Meanwhile, imagine there was an illustration here that made it all crystal clear to you.

Delimited continuations

I've also been asked to discuss guarded continuations versus delimited continuations.  <cough>  That's a rather large topic.  I'd probably have to start by explaining why I think "delimited continuations" is a misnomer — by my reckoning, delimited continuations aren't continuations at all.  They're functions, and functions are a completely different sort of creature than continuations.  Continuations only have one side (input), which is why it's simply meaningless to talk about composing them.  (Can you see I'm working up to a major rant, here?)

So I'm going to end this post here —it's already the longest post I've yet written on this blog— and hope to put together something on delimited continuations later.  Perhaps that post will also help to further clarify guarded continuations, but we'll see.  It's yet another item for my collection of in-development blog posts (along with guarded environments, another interesting topic this has reminded me of).