Defunctionalization

Defunctionalization, introduced by Reynolds in 1972, turns a higher-order program into a first-order one^[1]. A function value can only have been created by one of the finitely many lambda expressions in the program. Each lambda therefore becomes a constructor of one data type, whose arguments are the lambda's free variables, and applying a function value becomes calling apply, which matches on the constructor and evaluates that lambda's body. The program's behaviour is unchanged, but function values are now ordinary data that can be compared, printed or stored.

Summing a tree in continuation-passing style creates two kinds of continuation, and the initial one is the identity. Defunctionalizing gives three constructors and an apply that does what each lambda did^[2].

type tree = Leaf | Node of tree * int * tree
 
(* Direct style: the pending additions live on the call stack. *)
let rec sum = function Leaf -> 0 | Node (l, x, r) -> sum l + x + sum r
 
(* CPS: the pending work is a closure. *)
let rec sum_k t k =
  match t with
  | Leaf -> k 0
  | Node (l, x, r) -> sum_k l (fun sl -> sum_k r (fun sr -> k (sl + x + sr)))
 
(* Defunctionalized: one constructor per lambda above, holding its free
   variables, and apply doing what the lambda's body did. *)
type cont =
  | Done                          (* fun v -> v *)
  | Left of int * tree * cont     (* fun sl -> sum_k r (fun sr -> k (sl + x + sr)) *)
  | Right of int * int * cont     (* fun sr -> k (sl + x + sr) *)
 
let rec sum_d t k =
  match t with
  | Leaf -> apply k 0
  | Node (l, x, r) -> sum_d l (Left (x, r, k))
 
and apply k v =
  match k with
  | Done -> v
  | Left (x, r, k) -> sum_d r (Right (v, x, k))
  | Right (sl, x, k) -> apply k (sl + x + v)
 
(* The continuation is data, so it can be inspected. *)
let rec show = function
  | Done -> "Done"
  | Left (x, _, k) -> Printf.sprintf "Left (%d, _, %s)" x (show k)
  | Right (sl, x, k) -> Printf.sprintf "Right (%d, %d, %s)" sl x (show k)

In sum_d every call is a tail call, and the continuation, a linked list of Left and Right frames, is exactly the stack that the direct version kept implicitly. The pair sum_d and apply is an abstract machine for summing trees.

open D1_tree

sum 6, sum_k 6, sum_d 6
  leaf, k = Left (1, _, Left (2, _, Done))
  leaf, k = Right (0, 1, Left (2, _, Done))
  leaf, k = Left (3, _, Right (1, 2, Done))
  leaf, k = Right (0, 3, Right (1, 2, Done))
direct: Stack_overflow
defunctionalized: 500000500000

The direct recursion overflows the native stack; the defunctionalized version keeps its stack on the heap and finishes. The trace shows the continuation as data at each leaf: Left (x, _, k) is waiting to sum a right subtree, and Right (sl, x, k) has the left sum and is waiting for the right one.

Danvy and his coauthors showed that defunctionalizing the CPS form of an evaluator mechanically produces a known abstract machine: the CEK machine from a call-by-value evaluator, the Krivine machine from a call-by-name one, and others^[2][3]. The inverse transformation, refunctionalization, turns an abstract machine back into a higher-order evaluator.

Compilers use defunctionalization to implement first-class functions without closures as code pointers. MLton, a whole-program Standard ML compiler, represents function values this way, which lets later passes see exactly which functions can be called at each point^[4]. The same idea makes function values serializable, for example for sending a continuation over a network.

In a typed language the apply function is not always typable with ordinary data types, because the constructors carry functions of different types. Bell, Bellegarde and Hook handled the monomorphic case^[6], and Pottier and Gauthier showed that polymorphic programs can be defunctionalized type-correctly using GADTs^[5].

John Reynolds introduced defunctionalization in his 1972 paper on definitional interpreters, as a way to define a higher-order language with a first-order interpreter^[1]. The paper was reprinted with commentary in 1998. Danvy and Nielsen revived the technique in 2001 as a tool for deriving programs^[2], and Ager, Biernacki, Danvy and Midtgaard used it in 2003 to connect evaluators with abstract machines^[3].

• Continuation-passing styleContinuation-passing style (CPS) is a way of writing programs in which no function returns: each takes an extra argument, its continuation, a function that represents the rest of the computation, and calls it with the result. Every call becomes a tail call, evaluation order is made explicit, 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.
• ClosureA closure is a function value together with the environment in which it was created: the bindings of the free variables its body refers to. Closures are what make functions first-class values in a lexically scoped language. Compilers implement them by closure conversion, which turns each function into a code pointer paired with a record of captured values.
• Tail callA tail call is a call made as the last action of a function, whose result the caller returns unchanged. Since the caller has nothing left to do, its stack frame can be reused, and the call compiled as a jump; a language that does this for every tail call is properly tail recursive, and loops can be written as recursion without the stack growing. OCaml, Scheme and most functional languages guarantee it; the JVM, Python and most JavaScript engines do not.

1. [1]J. C. Reynolds, “Definitional interpreters for higher-order programming languages”, Proceedings of the ACM Annual Conference (1972); reprinted in Higher-Order and Symbolic Computation 11 (1998).
2. [2]O. Danvy, L. R. Nielsen, “Defunctionalization at work”, PPDP (2001).
3. [3]M. S. Ager, D. Biernacki, O. Danvy, J. Midtgaard, “A functional correspondence between evaluators and abstract machines”, PPDP (2003).
4. [4]H. Cejtin, S. Jagannathan, S. Weeks, “Flow-directed closure conversion for typed languages”, ESOP (2000).
5. [5]F. Pottier, N. Gauthier, “Polymorphic typed defunctionalization”, POPL (2004).
6. [6]J. M. Bell, F. Bellegarde, J. Hook, “Type-driven defunctionalization”, ICFP (1997).

last updated 1 October 2026