Reynolds (1972) -- Definitional Interpreters for Higher-Order Programming Languages

The paper

J. Reynolds, “Definitional interpreters for higher-order programming languages,” the ACM annual conference, vol. 2, pp. 717–740, 1972.

doi:10.1145/800194.805852

A summary of the paper and how gen uses it.

Reynolds, John C. “Definitional Interpreters for Higher-Order Programming Languages.” In Proceedings of the ACM Annual Conference, Vol. 2, 717-740. Boston, 1972. Reprinted with retrospective in Higher-Order and Symbolic Computation 11, 363-397 (1998). https://doi.org/10.1023/A:1010027404223

Paper Summary

The problem Reynolds addresses is deceptively fundamental: when we define a programming language L by writing an interpreter in a metalanguage M, the interpreter implicitly inherits properties of M. If M is a higher-order language (one where functions are values), an interpreter for L written in M can use M’s closures to implement L’s closures, M’s calling convention to implement L’s calling convention, and M’s variable binding to implement L’s variable binding. This inheritance is convenient but dangerous — it means the definition of L is entangled with implementation choices of M, and the interpreter does not actually specify how L’s higher-order features work.

Reynolds identifies two orthogonal dimensions along which definitional interpreters vary: (1) whether the interpreter itself uses higher-order functions, and (2) whether the evaluation order (call-by-value vs. call-by-name) of the defined language L depends on the evaluation order of the defining language M. These two dimensions produce four classes of interpreters. Reynolds shows constructive transformations between all four classes, establishing that one can always move from a “parasitic” interpreter (which inherits M’s properties) to a “self-contained” one (which explicitly specifies L’s behavior).

The central technical contribution is defunctionalization: a systematic transformation that eliminates higher-order functions from a program by replacing them with first-order tagged data and an explicit dispatch function (called apply). Each lambda abstraction in the source program is replaced by a data constructor carrying the free variables of that lambda (its closure environment). All function application sites are replaced by calls to a single apply function that dispatches on the tag to execute the appropriate body. The transformation is global — every closure-creating site produces a distinct tag, and the apply function has a branch for each tag.

Reynolds demonstrates this on a simple applicative language with lambda, apply, let, letrec, conditionals, and primitive operations. Starting from a direct (higher-order, order-dependent) interpreter, he derives:

1. A higher-order, order-independent interpreter by introducing explicit continuations (continuation-passing style, CPS), which disentangles L’s evaluation order from M’s.
2. A first-order, order-dependent interpreter by defunctionalizing the direct interpreter — replacing environment closures with data records and the value domain with a tagged union of constants and closures.
3. A first-order, order-independent interpreter by applying both transformations: first CPS to expose control flow, then defunctionalization to eliminate all remaining higher-order functions (both closures and continuations become first-order data).

The first-order, order-independent interpreter is the paper’s culminating artifact: it specifies L completely without inheriting any semantic property from M. It is essentially an abstract machine — Reynolds notes its similarity to Landin’s SECD machine, which was originally derived by different (less systematic) means.

The paper also discusses extensions for imperative features: assignment requires threading a store through the interpreter, and jumps (goto/labels) require first-class continuations in M or, after defunctionalization, explicit continuation data structures. The J operator (Landin’s jump operator for non-local returns) receives particular attention as a test case for the CPS + defunctionalization methodology.

Reynolds’ defunctionalization and CPS transformation became foundational techniques in programming language theory and compiler construction. Defunctionalization was later formalized by Danvy and Nielsen (2001) and connected to the broader theory of program transformations. The CPS transformation Reynolds introduces (building on work by Fischer, Plotkin, and others) became central to denotational semantics and compiler intermediate representations.

Key Concepts

• Definitional interpreter (S1) — An interpreter for language L written in metalanguage M. Serves as L’s formal definition. The interpreter’s structure implicitly determines whether L’s semantics depends on M’s evaluation order and higher-order features.

• Higher-order vs. first-order interpreters (S1) — A higher-order interpreter uses M’s functions to represent L’s functions (closures are implicit in M). A first-order interpreter represents L’s functions as data (closures are explicit records). The distinction determines whether L’s closure semantics is defined or inherited.

• Order-dependent vs. order-independent interpreters (S1) — An order-dependent interpreter inherits M’s evaluation strategy (CBV or CBN) for L. An order-independent interpreter explicitly specifies L’s evaluation order, typically via continuations or explicit sequencing.

• Defunctionalization (S6) — The transformation from higher-order to first-order: replace each lambda abstraction with a data constructor carrying free variables, replace all application sites with calls to a dispatch function (apply) that branches on the constructor tag. The number of tags equals the number of syntactically distinct lambda forms in the program.

• Closure as data (S6) — After defunctionalization, a closure is a record: { tag, env } where tag identifies which lambda body to execute and env carries the captured free variables. This makes closure structure inspectable and comparable — properties that higher-order closures in M lack.

• Continuation-passing style (S7) — Transform the interpreter so every function takes an explicit continuation argument representing “what to do with the result.” This disentangles L’s control flow from M’s call stack. After CPS, the interpreter specifies L’s evaluation order regardless of M’s.

• Defunctionalized continuations (S8) — Continuations, being functions, can themselves be defunctionalized. Each continuation-creation site becomes a data constructor; the continuation dispatch function branches on tags. The result is a first-order abstract machine with an explicit continuation stack.

• Environment representation (S6) — In the first-order interpreter, environments become explicit data structures (association lists or records mapping variable names to values) rather than being implicit in M’s lexical scoping.

• The four interpreter classes (S5-8) — The 2x2 matrix of {higher-order, first-order} x {order-dependent, order-independent}. Reynolds shows constructive transformations between all four quadrants, establishing their equivalence as language definitions.

• Store threading for assignment (S10) — Imperative features require passing an explicit store parameter through the interpreter. After defunctionalization, the store becomes a first-class data structure (array or map) threaded through the abstract machine.

• J-operator and non-local control (S9) — Landin’s J-operator for non-local returns serves as a test case. In the CPS interpreter, J-continuations are just values. After defunctionalization, they become tagged data in the continuation stack — demonstrating that the methodology handles non-trivial control operators.

How gen uses this

gen-aspects: guard defunctionalization

A guard decides whether an aspect’s content applies in a given context.

Defunctionalized guards (lib/guard.nix) apply Reynolds’ transformation directly, in the form Danvy & Nielsen 2001 formalize. guard pred body pairs a condition with a body, and both are terms of gen-algebra’s one first-order term algebra (lib/guard-term.nix is gen-aspects’ instance of it). The condition is built from a closed vocabulary of constructors (pred.class, pred.tagEq, pred.eq, pred.has, pred.all, pred.any, pred.always, pred.not), each emitting a core term. A custom condition is a Nix function that builds a term from these at declaration, never a new interpreted form. A body is a term or first-order data, lifted to its term and checked against the configuration’s declared names where the guard meets its cnf. One interpreter, gen-algebra’s resolver, reads every condition through the read environment gen-aspects supplies: the role of Reynolds’ apply. Because the condition and the body are data, a guard’s identity is the mint over the two and never has to hash a closure.

Context closures such as { host, ... }: { nixos = ...; } are not a second guard form. gen-aspects refuses one by name at an aspect position: a closure crosses the gen-rules door, which lowers it to a door node, so the one closure crossing sits at that door. A context-dependent aspect is written as a guard, guard (pred.has "host") { … }, whose body reads the context through read terms.

canTake (lib/can-take.nix) reads a function’s formals to decide whether the available context satisfies its required parameters. This inspects first-order data instead of trying the call.

gen-bind: partial application as closure manipulation

gen-bind’s wrap performs partial application: given a module function { host, config, lib, ... }: { ... } and bindings { host = ...; }, it produces a function that still accepts config and lib from the module system with host pre-bound. In Reynolds’ terms it constructs a new closure whose environment includes the bound values.

builtins.functionArgs is Nix’s analogue of Reynolds’ formal parameter reflection. A definitional interpreter knows each lambda’s parameter names because it processes the abstract syntax. In Nix, builtins.functionArgs exposes the same information at runtime, so gen-bind can read a function’s interface without calling it.

Every wrap result carries a signature (lib/signature.nix): what the module still requires from the module system, what gen-bind bound, what is unsatisfied, and the declaredMergeStrategies per bound name. It is the first-order record of the module’s binding state, like the environment record of a defunctionalized closure, tracking which variables are bound and which are still free.

Further directions

Unexploited Ideas

Systematic CPS for pipeline control flow (S7-8): Reynolds’ CPS transformation makes control flow explicit and first-order. gen-scope uses Nix’s native call stack for attribute evaluation order. Applying CPS transformation to attribute computations would make the evaluation schedule inspectable and controllable — enabling explicit scheduling policies (breadth-first vs. depth-first attribute evaluation), better error reporting (the continuation stack is data, not an opaque call stack), and potentially incremental re-evaluation (continuations can be checkpointed).

Defunctionalized continuations as reified evaluation traces (S8): After both CPS and defunctionalization, the continuation stack is a list of tagged data records. In gen, this would mean every pending attribute computation is represented as an inspectable record: what attribute, on which node, waiting for what. This reified evaluation trace could power debugging tools (show the user exactly why a particular attribute is being computed), cycle detection (inspect the continuation stack for duplicate entries), and profiling (count and categorize pending computations).

Store-passing for mutable-like semantics (S10): Reynolds’ store-threading technique for imperative features has not been exploited in the gen ecosystem. A store-passing interpretation could enable gen-scope attributes that accumulate side-channel state (counters, logs, warnings) threaded through the evaluation in a controlled manner, rather than relying on Nix’s builtins.trace or throwing errors.

Defunctionalization of collection fold functions: Collection attributes in gen-scope use traversal functions (fold/map over children, imports, ancestors). These fold functions are opaque Nix closures. Defunctionalizing them into tagged traversal descriptors (e.g., { __traversal = "children"; __combine = "append"; }) would make collection attribute semantics inspectable — enabling optimization (skip traversal when no contributors exist), composition (merge two collection traversals without creating a new closure), and serialization (collection semantics as data for diagram generation).

The four-quadrant framework applied to NixOS module evaluation (S5-8): NixOS evalModules is a higher-order, order-dependent evaluator — it uses Nix closures for module functions and inherits Nix’s lazy evaluation order. Reynolds’ framework suggests three alternative evaluator designs: first-order (modules as data records), order-independent (explicit module evaluation scheduling), or both. A first-order, order-independent evalModules would make module evaluation fully inspectable and controllable — relevant for debugging, optimization, and incremental evaluation of large NixOS configurations.

Research Directions

Defunctionalization as a design methodology for Nix libraries: Reynolds’ transformation is typically applied to compiled programs. In gen, it is applied as a design pattern: guard predicates are defunctionalized into first-order data, and other closures are wrapped into attrsets with __functor. Formalizing when and why Nix library designers should defunctionalize (inspectability requirements, comparison requirements, serialization requirements) could yield design guidelines for the broader Nix ecosystem, where opaque closures are a frequent source of debugging difficulty.

Relationship between defunctionalization and Nix’s builtins.functionArgs: Nix provides limited native function inspection via builtins.functionArgs (formal parameter names and default-presence flags). This is a subset of what full defunctionalization provides (parameter names but not closure contents, not the function body). Characterizing exactly what builtins.functionArgs enables versus what full defunctionalization enables would clarify the theoretical position of gen-bind (which relies on native inspection) versus gen-aspects’ guard vocabulary (which defunctionalizes predicates fully).

Defunctionalization and the expression problem in Nix: Reynolds’ defunctionalization is closed — the apply function must enumerate all tags. Adding a new lambda form requires modifying apply. gen-aspects’ guard interpreter is closed in the same way, and deliberately so: a new interpreted form would need a case in the one apply function, so a configuration extends the vocabulary by a function that composes existing constructors into a term, and a condition no term can state is written as a guard function and crosses at the gen-rules door. The expression problem (adding both new data variants and new operations without modifying existing code) is relevant here. Investigating how Reynolds’ transformation interacts with Nix’s open attrset model (where new keys can always be added) could yield patterns for extensible defunctionalization — defunctionalized dispatch that is open to new tags without modifying the dispatch function.

Partial defunctionalization and selective opacity: Not all functions in a program need to be defunctionalized — only those requiring inspection or comparison. Reynolds’ transformation is all-or-nothing (all closures in a given type become first-order). A theory of partial defunctionalization that identifies which functions benefit from the transformation and which should remain opaque (for performance or encapsulation) would formalize the choices gen makes case by case: guard predicates are defunctionalized (they need identity and inspection), module functions are not, and collection fold functions are not (see above).