Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
This is the original paper that introduces the "composable" continuation as in improvement over call/cc. They use CPS semantics and provide a CEK machine.
This paper introduces the # (prompt) operator, giving the first treatment of delimited continuations. It is argued that the calculus has the Church-Rosser property. A CEK machine is described for the new calculus.
This paper shows how to use shift/reset to implement a CPS transformer in direct style for lambda calculus plus shift/reset!
This is a scheme paper. It shows how to implement prompt and control using call/cc, then how to implement a bunch of stuff like exceptions, unwind-protect, streams, engines with it. Then addresses the problem of how these operators would interact wrongly with each other. To solve the problem he proposes multiple-prompts indexed by integers.
The next paper goes a bit further with similar stuff.
This shows how to turn direct style code in scheme into monadic code using delimited continuations.
The Subcontinuations paper is aimed at making control operators work together with concurrency. They do this with a
spawn operator that is somewhat similar to
(\p. #_i (p F_i)) with the idea that we have an indefinite supply of matched
F operators. Basically it's a type of multiprompt continuations.
This is the first work to introduce multiple prompt delimited continuations and give it a rigorous treatment. They reference the [Theory and Practice of First-Class Prompts] paper, saying that it provided a single untyped prompt and that they introduced the idea of having multiple typed prompts (in order to make everything work in a well typed fashion). This is done with the
new_prompt operator. Rather than control/prompt or shift/reset, they use set/cupto (control up to) operators. It is discussed that previous multiprompt work used integers instead of an abstract type: this has the disadvantage that of being able to write bad programs (making use of prompts you shouldn't be able to).
This paper shows a practical application of delimited continuations. It's about partial evaluation for lambda calculus with let. The specific problem they address is how to do a "binding time improvement" that enables a dynamic let whose innards are static to be specialized away. An example to make this clear:
1 + (let x = d in 3) is difficult to specialize down to
let x = d in (1 + 3) is much easier. Making a partial evaluator capable of doing this has been solved before by Bondorf, by writing the partial evaluator in CPS. The contribution of this paper is to show how to do without CPS, using shift/reset instead. This allows a much more direct implementation that's easier to understand. At the end they discuss some other binding-time improvements that may be possible, like applications and conditionals.
This is a clever hack. I'd be interested in other approaches to mobile code that use delimited continuations. Unfortunately I couldn't find the source on the authors page. Eijiro is also the author of MinCaml!
This may be the first direct implementation of shift/reset, it documents the implementation in the bytecode based system Scheme48.
Unlike [Continuation-Based Partial Evaluation] this paper use any control operators in its implementation. But it does implement a partial evaluator for a lambda calculus with shift/reset. The paper includes SML source.
This paper has some very helpful equations regarding shift/reset. It also breaks down shift into 2 parts: aborting and delimiting. The equations will help people understand these operators as well as be useful for making test cases. It uses a CPS transform to prove the equations they came up with are sound and complete.
The sequel develops the idea further by applying it to a an indexed hierarchy of control operators. This paper covers the CPS hierarchy, an integer indexed sequence of shift_i/reset_i operators. They motivate the need for this by showing how nondeterminism and stream generators don't compose if they use the same shift/reset. The i'th operator is described in terms of the i'th iterated CPS transformation. At the end he asks whether or not such a hierarchy has any application.
S(\k.k M) = M
<F[S M]> = <M(\x.<F[x]>)>
S(\k.<M>) = S(\k.M)
F[S M] = S(\k.M(\x.<k F[x]>))
S(\k.M k) = S M
(\x.S(\k.N))M = S(\k.(\x.N)M)
I think this is the second paper that addresses multiple first class prompts [(1995) A generalization of exceptions and control in ML-like languages] was the first. They create a monad with
pushSubCont operators. These operators can implement callcc, shift/reset (as well as shift-at/reset-at), control/prompt, abort and so on. The provide semantics using an abstract machine, CPS and monadically.
This is a great application of multiprompt delimited continuations. It shows how to implement dynamic variables, similar to rackets parametrize. Because prompts were used it interacts smoothly with other control operator based constructs.
This is a report on integrating control operators into PLT scheme/racket in so that they interact correctly with the rest of the language: exceptions, dynamic-wind, dynamic binding. It is pointed out that continuations can implement exceptions but not if the language already has call/cc, because of interference. To solve this problem they build a system of prompts and implement exception handling with it. Hieb's control-filters idea from [Subcontinuations] is referenced for dynamic-wind.
This is a useful paper for showing the relationship between the different pairs of control operators. It includes scheme macros to define them in terms of the others.
Application. They implement a virtual filesystem with zipper based cursors done by multiprompt continuations.
This paper shows how to use the technique of logical relations to prove correct a partial evaluation like the one in [(1995) Continuation-Based Partial Evaluation - Julia Lawall, Olivier Danvy] that performs the let binding time improvement. They also extend the partial evaluator to handle shift/reset.
Direct implementation of shift/reset in MinCaml. It's mentioned that Scheme48 and delimcc previously implemented it directly in terms of bytecode VMs, this is the first direct implementation in assembly. The paper basically goes over in detail the 3 important points: How the stack and heap are affected by reset, shift k and calling k. Benchmarking is performed and some key optimizations are identified.
In the sequel they repeat the work for Caml Light which (unlike MinCaml) has data types.
This is one of my favorite implementation papers. They show, with source code rather than mathematical formulations a step by step process of converting a basic evaluator for lambda calculus with shift/reset into a compiler + virtual machine to execute the language directly.
This shows how to define shift/reset in terms and yield/run and vice versa.
This paper presents a minimal lambda calculus theory for multi-prompt delimited continuations. The connection with dynamic binding is stressed.
Good overview of some of the early papers: https://pdfs.semanticscholar.org/ce2b/170225dbcd0e453817a8efa9c5bfddc6edc2.pdf
Some modern directions things are going in are:
- Handling these control operators in a dependently typed setting
- algebraic effect handlers which seem to be more powerful than monad transformer stacks