nLab continuation-passing style

Idea

In the theory of programming languages, the idea that procedures may be modelled as mathematical functions is useful for compositional reasoning, but at first seems to rule out programming with more sophisticated control structures which can actually be very useful in practice. For example, we might want to write an integer division routine which raises an exception on division-by-zero, or a procedure that lazily computes the first satisfying assignment to a boolean formula while giving the user the ability to query to obtain additional ones.

Now, an “impure” functional language such as OCaml lets us do some of this directly. For example, we can write the following code for integer division:

let divide : int -> int -> int =
  fun x y -> if y == 0 then raise Division_by_zero else x / y

However, it should be said that the type ascription “int -> int -> int” is a bit misleading here (or at least open to misinterpretation), since divide cannot actually be modelled as a set-theoretic function of type $\mathbb{Z} \to \mathbb{Z} \to \mathbb{Z}$.

Continuation-passing style (or CPS) is a very general technique that allows one to express many different seemingly “non-functional” patterns of control flow within the confines of pure functional programming. The basic idea is that a procedure in CPS takes an additional argument (often named “$k$”) representing the continuation, a functional abstraction of the context in which the procedure is used (or “the rest of the computation”). Whenever a procedure in “direct style” would return a value ($v$), the corresponding procedure in CPS instead invokes the continuation with that value ($k(v)$). However, it is the fact that the procedure has explicit access to the continuation which also allows for the possibility of exceptional behaviors, typically by throwing away the continuation or by invoking it more than once.

To transform the example above into continuation-passing style, first we must fix an “answer type”, that is, the return type of the continuation. In this case, to allow for the possibility of raising a division-by-zero error, the answer type should be a pointed type. For example, we could take

type ans = int option

Now, our division routine can be written as follows in CPS:

let divide_cps : int -> int -> (int -> ans) -> ans =
  fun x y k -> if y == 0 then None else k (x / y)

Observe that we have replaced the (somewhat misleading) original type

divide : int -> int -> int

by the more complicated type

divide_cps : int -> int -> (int -> ans) -> ans

This may be recognized as a form of double negation translation, and indeed under propositions as types, the classical negative translations correspond to different forms of continuation-passing style transformations. Under this correspondence, the “answer type” corresponds to the type of absurdity $\bot$, but as the above example shows, we almost never want the answer type to be empty. As such, CPS translation is best understood in terms of the negative translations from classical logic into minimal logic, where the type of falsehood $\bot$ behaves like a fixed atomic proposition.

Continuation semantics

Whereas “continuation-passing style” refers to a programming technique, the term “continuation semantics” refers to a certain way of assigning denotational semantics to programs, originally in the context of domain theory (Strachey & Wadsworth 1974). The two are very closely related, though, especially if one views the meaning function ⟦-⟧ in a denotational semantics as a “definitional interpreter” in the sense of (Reynolds 1972). In that case, giving a continuation semantics for a language corresponds to writing the definitional interpreter in continuation-passing style.

Related concepts

• Response category?

• continuation monad

• programming language

• functional programming

• Yoneda lemma

• negative translation

• double-negated principle of excluded middle

• monad (in computer science)

• defunctionalization, often used in conjunction with continuation-passing style

References

Some early and historical references for continuations and continuation-passing style include:

• John C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of the ACM National Conference, 1972. (pdf)

• Christopher Strachey and C. P. Wadsworth. Continuations: A Mathematical Semantics for Handling Full Jumps, Technical Monograph PRG-11, Oxford, 1974. (pdf)

• John C. Reynolds. On the Relation Between Direct and Continuation Semantics. Second Colloquium on Automata, Languages, and Programming, Saarbrucken, July 29 - August 2, 1974. (pdf)

• Gordon Plotkin. Call-by-name, call-by-value, and the lambda-calculus. Theoretical Computer Science 1 (1975), 125-159. (pdf)

• John C. Reynolds. The Discoveries of Continuations. LISP and Symbolic Computation 6 (1993), 233-247. (pdf)

Other references include:

• Hayo Thielecke. Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh, 1997. (pdf)

• Josh Berdine?, Peter O'Hearn, Uday Reddy, Hayo Thielecke. Linear Continuation-Passing. Higher-Order and Symbolic Computation 15 (2002), 181-208. (pdf)

• Ulrich Schöpp. On the Relation of Interaction Semantics to Continuations and Defunctionalization. Logical Methods in Computer Science Vol.10(4:10)2014, 1-41. (pdf)

• Wikipedia, Continuation-passing style

For the connection between CPS and the Yoneda lemma, see

• Ralf Hinze, Daniel W. H. James, Reason Isomorphically!, sections 3-4, pdf

• Mike Stay, The Continuation Passing Transform and the Yoneda Embedding, blog post