Continuation-passing style

Continuation-passing style (CPS) is a way of writing programs in which no function returns. Each function takes an extra argument, its continuation, a function that represents the rest of the computation, and passes its result to that continuation instead of returning it. In CPS every call is a tail call, the order of evaluation is written out explicitly, and control operators such as exceptions, backtracking and call/cc become ordinary functions. Compilers for functional languages use CPS, or the closely related A-normal form, as an intermediate language^[8].

§ 01

Overview

In $1 + f (x) \times 2$ , once $f (x)$ has been computed, what remains is to multiply it by 2 and add 1. That remaining work, as a function of the value of $f (x)$ , is the continuation of the call: $λ v . 1 + v \times 2$ . Every expression in a program has a continuation, and in direct style it is implicit: the language's runtime keeps it on the call stack, as the frames waiting for results. CPS passes it explicitly as an argument.

Factorial and Fibonacci in direct style and in CPS.

(* Direct style: the multiplication waits for the recursive call. *)
let rec fact n = if n = 0 then 1 else n * fact (n - 1)
 
(* CPS: the waiting work moves into the continuation k, and every call
   is a tail call. *)
let rec fact_k n k = if n = 0 then k 1 else fact_k (n - 1) (fun r -> k (n * r))
 
(* Fibonacci has two recursive calls; CPS fixes their order. *)
let rec fib_k n k =
  if n < 2 then k n else fib_k (n - 1) (fun a -> fib_k (n - 2) (fun b -> k (a + b)))

Running it.

fact 10                    ->  3628800
fact_k 10 (fun x -> x)     ->  3628800
fact_k 5 string_of_int     ->  "120"
fib_k 20 (fun x -> x)      ->  6765

In fact_k the multiplication that direct-style fact performs after its recursive call is moved into the continuation fun r -> k (n * r), and the recursive call is the last thing the function does. The final continuation decides what happens to the answer: the identity returns it, string_of_int converts it. In fib_k the two recursive calls, which direct style would leave in an unspecified order, are sequenced: the second starts inside the continuation of the first.

§ 02

Definition

A term is in CPS when every function takes a continuation parameter, every call is in tail position, and every intermediate result is named. The types change systematically. For a fixed answer type $R$ , a computation producing an $A$ becomes a function that takes an $A$ -consumer:

[[A]] = (A^{*} \to R) \to R (A \to B)^{*} = A^{*} \to (B^{*} \to R) \to R int^{*} = int

so a function of type int -> int, like fact, becomes int -> (int -> 'r) -> 'r, like fact_k.

The CPS transform

Any program can be converted to CPS mechanically. Plotkin's call-by-value transform^[2] is defined by induction on terms, where $k, f, v$ are fresh variables:

[[x]] [[λ x . e]] [[e_{1} e_{2}]] = λk . k x = λk . k (λ x . [[e]]) = λk . [[e_{1}]] (λ f . [[e_{2}]] (λ v . f v k))

Variables and λ-abstractions are values, and a value is passed straight to the continuation. An application evaluates the function, then the argument, then calls the function with the argument and the application's own continuation. The transformed program is run by applying it to the identity continuation. Plotkin proved that the transform is correct: $[[e]] (λ x . x)$ evaluates to the translation of the value of $e$ , and it does so under call-by-name and call-by-value alike, because every argument in a CPS term is already a value^[2].

The transform for a small language with addition, and an evaluator to check it.

(* A small call-by-value language and Plotkin's CPS transform of it. *)
type term =
  | Const of int
  | Var of string
  | Lam of string * term
  | App of term * term
  | Add of term * term
 
let counter = ref 0
let fresh base = incr counter; Printf.sprintf "%s%d" base !counter
 
(* [x] = \k. k x        [\x.e] = \k. k (\x. [e])
   [e1 e2] = \k. [e1] (\f. [e2] (\v. f v k))
   [e1 + e2] = \k. [e1] (\a. [e2] (\b. k (a + b)))  *)
let rec cps = function
  | Const n -> let k = fresh "k" in Lam (k, App (Var k, Const n))
  | Var x -> let k = fresh "k" in Lam (k, App (Var k, Var x))
  | Lam (x, e) -> let k = fresh "k" in Lam (k, App (Var k, Lam (x, cps e)))
  | App (e1, e2) ->
      let k = fresh "k" and f = fresh "f" and v = fresh "v" in
      Lam (k, App (cps e1, Lam (f, App (cps e2, Lam (v, App (App (Var f, Var v), Var k))))))
  | Add (e1, e2) ->
      let k = fresh "k" and a = fresh "a" and b = fresh "b" in
      Lam (k, App (cps e1, Lam (a, App (cps e2, Lam (b, App (Var k, Add (Var a, Var b)))))))
 
(* A call-by-value evaluator for both the source and the transformed term. *)
type value = Int of int | Clo of string * term * (string * value) list
 
let rec eval env = function
  | Const n -> Int n
  | Var x -> List.assoc x env
  | Lam (x, e) -> Clo (x, e, env)
  | App (e1, e2) -> (
      match eval env e1 with
      | Clo (x, body, cenv) -> eval ((x, eval env e2) :: cenv) body
      | Int _ -> failwith "not a function")
  | Add (e1, e2) -> (
      match (eval env e1, eval env e2) with Int a, Int b -> Int (a + b) | _ -> failwith "not a number")
 
let rec show = function
  | Const n -> string_of_int n
  | Var x -> x
  | Lam (x, e) -> "\\" ^ x ^ ". " ^ show e
  | App (e1, e2) -> "(" ^ show e1 ^ ") (" ^ show e2 ^ ")"
  | Add (a, b) -> show a ^ " + " ^ show b
 
let rec size = function
  | Const _ | Var _ -> 1
  | Lam (_, e) -> 1 + size e
  | App (a, b) | Add (a, b) -> 1 + size a + size b

Running it.

program            (\x. x + 1) (41)
direct result      42
cps program, run with the identity continuation:  42
term size          6 before, 36 after the transform
cps of 41          \k11. (k11) (41)

Administrative redexes

The transform above is correct but wasteful: the term grows from 6 nodes to 36, most of them λs that are immediately applied, such as the $(λk . k x) (λ f . \dots)$ produced for every variable in function position. These administrative redexes can be reduced at transformation time. Danvy and Filinski gave a one-pass transform that uses functions of the metalanguage for the continuations known at transformation time and so produces no administrative redexes at all^[9]. Flanagan, Sabry, Duba and Felleisen observed that a compiler which transforms to CPS, optimizes and transforms back computes the same thing as one that only names every intermediate result, which they called A-normal form^[10]:

(f (g x)) + 1 ⇝ let a = g x in let b = f a in b + 1

§ 03

Properties

Every call is a tail call

No function in CPS has anything left to do after a call, so every call can be compiled as a jump and the stack does not grow. The work that direct style keeps in stack frames is in the continuation closures instead, which live on the heap. A recursive function that would exhaust the stack therefore runs in CPS, at the cost of one allocation per pending frame:

Summing a tree of depth one million in direct style, in CPS, and with the continuation defunctionalized.

type tree = Leaf | Node of tree * int * tree
 
(* Direct style: one stack frame per level of the tree. *)
let rec sum = function Leaf -> 0 | Node (l, x, r) -> sum l + x + sum r
 
(* CPS: every call is a tail call; the pending work lives in closures
   on the heap. *)
let rec sum_k t k =
  match t with
  | Leaf -> k 0
  | Node (l, x, r) -> sum_k l (fun a -> sum_k r (fun b -> k (a + x + b)))
 
(* Defunctionalizing the continuation: one constructor per lambda above,
   and an [apply] that does what the lambda did. The result is a loop
   over an explicit stack. *)
type cont = Done | Right of tree * int * cont | Combine of int * int * cont
 
let rec sum_d t k =
  match t with Leaf -> apply k 0 | Node (l, x, r) -> sum_d l (Right (r, x, k))
 
and apply k v =
  match k with
  | Done -> v
  | Right (r, x, k) -> sum_d r (Combine (v, x, k))
  | Combine (a, x, k) -> apply k (a + x + v)
 
(* A left spine of n nodes: depth n. *)
let spine n =
  let rec go i acc = if i > n then acc else go (i + 1) (Node (acc, i, Leaf)) in
  go 1 Leaf

Running it with an 8 MB system stack.

sum   (depth 1,000,000)  ->  Stack_overflow
sum_k (depth 1,000,000)  ->  500000500000
sum_d (depth 1,000,000)  ->  500000500000

The direct version needs one frame per level and fails once the depth exceeds the stack limit (OCaml 5 runs OCaml code on its own stacks, limited by the l parameter of OCAMLRUNPARAM instead of the system stack). See tail call.

Defunctionalized continuations

The continuations of a particular CPS program are created by a fixed set of λs, so they can be replaced by a data type with one constructor per λ, holding its free variables, and an apply function, as in sum_d above^[12]^[13]. The continuation data type is then exactly an explicit stack, and the program a loop that pushes and pops it. Applied to an interpreter, CPS followed by defunctionalization turns a recursive evaluator into an abstract machine, which is how Ager, Biernacki, Danvy and Midtgaard derived the CEK and Krivine machines from evaluators^[17].

Evaluation order

Direct style leaves some evaluation order to the language: OCaml evaluates the operands of a + b in an unspecified order (in practice right to left). A CPS term fixes it, since the only way to get a value is to be passed it by a continuation, and a continuation is called by one computation after it has finished. This is why the result of Plotkin's transform is independent of the evaluation strategy used to run it, and why a CPS transform for call-by-name differs from the call-by-value one: it decides when arguments are evaluated.

§ 04

Control operators

Because the continuation is a value, a function in CPS can choose not to call it, call a different one, or call it more than once. Control flow that direct style needs special constructs for is expressed by these choices.

Exceptions and backtracking

With two continuations, one for success and one for failure, a function reports an error by calling the failure continuation, which skips the rest of the success path. When the failure continuation means "try the next alternative", the same pattern is backtracking search:

Exceptions and backtracking with success and failure continuations.

(* Two continuations: one for success, one for failure. Exceptions without
   an exception mechanism. *)
let safe_div a b ~ok ~err = if b = 0 then err "division by zero" else ok (a / b)
 
let calc a b c ~ok ~err =
  safe_div a b ~err ~ok:(fun x -> safe_div x c ~err ~ok:(fun y -> ok (x + y)))
 
(* Backtracking: the failure continuation says what to try next. Find a
   subset of the list summing to a target. *)
let rec subset_sum xs target ~found ~fail =
  if target = 0 then found []
  else
    match xs with
    | [] -> fail ()
    | x :: rest ->
        subset_sum rest (target - x)
          ~found:(fun s -> found (x :: s))
          ~fail:(fun () -> subset_sum rest target ~found ~fail)
 
(* Counting every solution: on success, record it and ask for the next. *)
let count_solutions xs target =
  let n = ref 0 in
  let rec go xs target ~found ~fail =
    if target = 0 then found ()
    else match xs with
      | [] -> fail ()
      | x :: rest -> go rest (target - x) ~found ~fail:(fun () -> go rest target ~found ~fail)
  in
  go xs target ~found:(fun () -> incr n) ~fail:(fun () -> ());
  !n

Running it.

calc 100 5 2        ->  ok 30
calc 100 0 2        ->  error: division by zero
subset_sum [8; 6; 7; 5; 3] 16  ->  [8; 5; 3]

In subset_sum each choice to include an element passes on a failure continuation that retries without it, so when a branch fails the search resumes at the most recent choice. This is the standard implementation of Prolog-style backtracking and of the backtracking alternative in parser combinators.

call/cc

Scheme's call-with-current-continuation gives a direct-style program access to its own continuation. callcc f calls f with a function that, when called with $v$ , abandons whatever it is doing and makes callcc f return $v$ . In an interpreter written in CPS it is a single case, because the interpreter already holds the continuation:

A CPS interpreter with call/cc.

(* An interpreter written in CPS. Because the interpreter holds the
   continuation as a value, it can hand it to the program: call/cc. *)
type expr =
  | Num of int
  | Var of string
  | Lam of string * expr
  | App of expr * expr
  | Add of expr * expr
  | Mul of expr * expr
  | Callcc of expr (* callcc (fun k -> ...) *)
 
type value = Int of int | Fn of (value -> (value -> value) -> value)
 
let rec eval env e (k : value -> value) : value =
  match e with
  | Num n -> k (Int n)
  | Var x -> k (List.assoc x env)
  | Lam (x, body) -> k (Fn (fun v k' -> eval ((x, v) :: env) body k'))
  | App (f, a) -> eval env f (fun fv -> eval env a (fun av -> match fv with Fn g -> g av k | Int _ -> failwith "apply"))
  | Add (a, b) -> arith ( + ) env a b k
  | Mul (a, b) -> arith ( * ) env a b k
  | Callcc f ->
      (* The captured continuation, as a function, ignores the continuation
         of its own call and jumps to k. *)
      eval env f (function Fn g -> g (Fn (fun v _ -> k v)) k | Int _ -> failwith "callcc")
 
and arith op env a b k =
  eval env a (fun x -> eval env b (fun y -> match (x, y) with Int x, Int y -> k (Int (op x y)) | _ -> failwith "arith"))
 
let run e = match eval [] e Fun.id with Int n -> string_of_int n | Fn _ -> "<fun>"

Running it.

1 + callcc (fun k -> 10 * k 5)  ->  6
1 + callcc (fun k -> 10 * 5)    ->  51

In the first program the call k 5 discards the pending multiplication and returns 5 to the addition. The continuation is undelimited: it is the entire rest of the program. Delimited continuations capture only the part up to an enclosing delimiter; Danvy and Filinski's shift and reset are defined by a CPS transform applied twice^[15]. OCaml 5's effect handlers are delimited continuations in which the handler is the delimiter, and they are implemented with separately allocated stack segments, not by CPS^[16].

§ 05

Logic

Under the Curry–Howard correspondence, the type translation with the answer type $R$ taken as falsity $⊥$ is a double-negation translation:

A ⟼ (A \to ⊥) \to ⊥ = \neg\neg A

Double negation embeds classical logic into intuitionistic logic, and CPS embeds programs with control operators into programs without them. Griffin showed that call/cc has the type of Peirce's law, a classical tautology that has no intuitionistic proof^[14]:

callcc : ((A \to B) \to A) \to A

so adding call/cc to a typed λ-calculus makes its type system correspond to classical logic.

§ 06

The continuation monad

The type $(A \to R) \to R$ is a monad:

return a = λk . k a m > > = f = λk . m (λa . f a k)

and writing a program with it is writing it in CPS with the plumbing hidden. It is universal in a precise sense: any monad whose operations can be written in the language can be embedded in the continuation monad with a suitable answer type, which is how delimited continuations implement other effects^[18].

§ 07

Uses

Compilers

Steele's Rabbit compiler for Scheme converted programs to CPS before generating code^[7], and Appel's Standard ML of New Jersey compiler used a CPS intermediate language throughout^[8]. In CPS every intermediate value has a name, every control transfer is a call, and a function's return is a call to a known continuation, which makes inlining, dead-code elimination and register allocation uniform. Later compilers mostly use A-normal form, which records the same information without closures for continuations^[10], or a CPS form with second-class continuations that are compiled as jumps^[11].

Asynchronous programming

Callbacks in event-driven code are continuations written by hand: readFile(path, (err, data) => ...) in Node.js takes the rest of the computation as its last argument, and the error-first convention is the two-continuation pattern above. Deeply nested callbacks are CPS written out manually. Promises and async/await in JavaScript, C#, Python and Rust let the programmer write in direct style while the compiler performs a CPS-like transformation of the function into a state machine whose states are its continuations.

§ 08

History

Continuations were discovered several times independently in the 1960s and early 1970s; Reynolds wrote a history of the discoveries^[4]. Van Wijngaarden described a transformation of Algol 60 that eliminated procedure returns in 1964^[5]. Strachey and Wadsworth used continuations to give a denotational semantics to jumps in 1974^[3], and Fischer^[6] and Reynolds^[12] used them in 1972 to make an interpreter independent of the evaluation order of the language it was written in. Plotkin proved the transforms correct in 1975^[2], and Sussman and Steele, in the report introducing Scheme the same year, coined the name continuation-passing style^[1].