Lorenzen et al. (2025) — First-Order Laziness

Paper Summary

Lorenzen, Leijen, Swierstra, and Lindley address a fundamental tension in strict functional languages: efficient purely functional data structures (as catalogued by Okasaki 1998) require laziness, but the standard implementation via higher-order thunks (closures that defer computation) carries three costs — closures cannot be inspected or printed for debugging, they require extra memory allocation (indirection nodes between every pair of adjacent elements), and reasoning about their performance is notoriously subtle. These costs discourage adoption of lazy data structures even where they provide asymptotic benefits.

The paper introduces lazy constructors: first-order data constructors that carry their arguments as inspectable tagged data, with an associated computation that executes on demand. Unlike traditional thunks (which wrap an opaque closure), a lazy constructor like SAppend(s1, s2) stores its operands as plain fields. The runtime never exposes lazy constructors to pattern matching — when a match encounters one, the associated computation fires automatically. The result is memoized (overwriting the constructor in place), so subsequent matches see the computed value. The key insight is that most lazy data structures use only a small, fixed set of deferred operations (e.g., append and reverse for queues). By defunctionalizing these operations into named constructors, all laziness becomes first-order: no closures, no opaque thunks.

The paper’s contributions span programming methodology, formal semantics, compiler optimizations, and empirical evaluation:

Programming methodology (Section 2). The authors reimplement Okasaki’s Bankers Queue and Realtime Queue using lazy constructors, showing how the approach arises naturally. They demonstrate progressive refinement: amortized constant-time (via basic lazy constructors), logarithmic worst-case (via eval-one that forces a single step), and true constant worst-case (via a schedule parameter, following Okasaki’s technique). They also address the practical problem of stack overflow from recursive evaluation of nested lazy constructors — a problem they discovered affects OCaml and Koka 3.1.3 on real workloads.

Formal semantics (Section 4). The authors formalize lazy constructors as an extension of Launchbury’s (1993) natural semantics for lazy evaluation. The core calculus is a first-order lambda calculus (no closures) with a new type A ->_F B representing a lazy computation: input type A, evaluation function F, result type B. Introduction forms are lazy_F v (deferred) and memo v (already computed); elimination is step v (force one level). The formalization proceeds in stages: first, non-recursive lazy constructors; then recursive lazy constructors modeled as A ->_F B := mu alpha. A ->_F (B + alpha) (a delay monad / trampoline structure); finally, a refined type with first-class indirection nodes that can be safely short-cut. The authors prove:

Theorem 1 (Type Soundness): Well-typed expressions evaluate to correctly-typed values, established via a step-indexed logical relation.
Theorem 2 (Referential Transparency): Evaluating lazy constructors in the store does not change the observable result of any expression. Formally: if Gamma : e => Delta : v and Gamma <= Gamma', then Gamma' : e => Delta' : v with Delta <= Delta'.
Theorem 3 (Short-cutting indirections is referentially transparent): Extends Theorem 2 to the refined calculus with indirection short-cutting rules cut_i and cut_m.

Compiler optimizations (Section 5). The first-order nature enables optimizations impossible with general closures: (1) in-place reuse of lazy constructor memory cells for their results (avoiding indirection nodes entirely when the result constructor fits); (2) tail-recursive evaluation via a Schorr-Waite traversal stored in the lazy constructors themselves (solving the stack overflow problem); (3) a small-step implementation calculus with lazy match and memoize primitives, connected to the high-level semantics via Lemma 2 (the low-level calculus implements the high-level calculus) and Lemma 3 (small-step implements big-step). The tail-recursive evaluation (Section 5.5-5.6) uses in-place pointer reversal (link/unlink primitives) to traverse nested lazy constructors without stack growth.

Benchmarks (Section 6). All of Okasaki’s lazy queues and heaps benchmarked in a sequential setting across Koka, OCaml, and Haskell. Traditional thunks incur 110-150% overhead versus strict versions. Lazy constructors reduce this to 43% average overhead in Koka, and in some cases under 25%, approaching strict performance while maintaining superior theoretical (amortized/persistent) properties.

Key Concepts

Lazy constructors — First-order data constructors with associated computations. Tagged data (not closures) that evaluate on demand and memoize results. Inspectable before forcing via debug-show / lazy match.
Defunctionalization of thunks — Lazy constructors arise as the defunctionalization (Reynolds 1972) of explicit thunks. Each distinct closure passed to delay becomes a named constructor with its free variables as fields.
Fusion of streams and stream cells — By inlining the stream cell type into the stream type (removing the Memo wrapper), indirection nodes between adjacent elements are eliminated. This is impossible with traditional thunks where every cell boundary requires an indirection for memoization.
In-place reuse — The compiler overwrites a lazy constructor’s memory cell with its result when the result constructor fits (same or smaller size). Combined with Perceus reference counting, this enables zero-allocation lazy evaluation in favorable cases.
Schorr-Waite evaluation — Nested lazy constructors are evaluated tail-recursively by reversing pointers in-place (storing the continuation zipper in the locked cells themselves), eliminating stack overflow.
eval-one — A compiler-generated function that forces exactly one lazy constructor without recursion. Enables logarithmic worst-case bounds by incrementally advancing nested computations.
Recursive lazy constructors — Modeled as A ->_F B := mu alpha. A ->_F (B + alpha), a delay monad where eval iterates step until a normal constructor is reached.
Indirection short-cutting — Rules cut_i (redirect indirection chains) and cut_m (replace indirections pointing to memoized values). Proven referentially transparent (Theorem 3).
Quotient type interpretation — Lazy constructors A ->_F B can be viewed as a quotient type over A + B quotiented by step. Recursive lazy constructors are quotiented by eval. Mutation under the quotient preserves referential transparency.

How gen uses this

gen-aspects

The paper’s central idea, a lazy constructor that can be inspected before it is forced, is how gen-aspects stores class content (lib/types.nix).

An aspect’s keys are classified by cnf.keySemantics. Each key whose category is class (e.g. nixos) gets a deferredModule option, built from gen-merge’s types:

classOptions = prelude.genAttrs (keyOf "class") (
  _:
  merge.mkOption {
    description = "Class content (deferred module); `null` when the class is declared but never given content";
    default = null;
    type = t.nullOr t.deferredModule;
  }
);

A declared class with no content reads null, so absence is visible without forcing anything.

This maps to the paper as follows:

Paper concept (S1-2.3)	gen-aspects realization
Lazy constructor (tagged data)	`deferredModule`, module content held as data until a module evaluation imports it
Inspectable before forcing	gen can examine aspect metadata, includes, identity and which class keys carry content without running the class’s module evaluation
Evaluated on demand	The `deferredModule` is forced only when the consuming NixOS, Darwin or Home Manager evaluation imports it
Memoization	Nix memoizes the forced value; once evaluated, the result is shared by every consumer
Defunctionalization (S3.1)	A guard is first-order data, a condition term and a body term, read by one interpreter (Reynolds 1972). A context closure (`{ host, ... }: { ... }`) is not wrapped: gen-aspects refuses it by name, and it crosses the gen-rules door, which lowers it to a door node

The paper’s fusion optimization (S3.3, eliminating indirection nodes between stream cells and streams) has an analogue: class options are declared directly on the aspect submodule, so no intermediate container sits between an aspect and its class content.

Further directions

Unexploited Ideas

eval-one for incremental forcing (S2.4). The paper’s eval-one primitive forces exactly one lazy constructor without recursion, enabling logarithmic worst-case bounds. gen-aspects has no analogue — deferredModule is either fully unforced or fully forced by the consuming module evaluation. An eval-one equivalent could enable incremental validation: force one level of a deferred module to check its top-level option declarations without evaluating nested imports or config values.

Schorr-Waite traversal for nested deferred modules (S2.5, S5.5-5.6). When aspects include other aspects that include further aspects, the chain of deferred modules can nest deeply. The paper’s Schorr-Waite technique evaluates nested lazy constructors in constant stack space by reversing pointers in-place. While Nix’s lazy evaluation handles this via thunk chains, the conceptual model of in-place pointer reversal could inform a more memory-efficient scope graph traversal for deep inclusion chains.

Fusion / indirection elimination (S3.3). The paper shows how inlining stream cells into streams eliminates indirection nodes, halving memory usage. gen has an indirection between the aspect node in the graph and its class content as a deferredModule. Fusing these — making the scope graph node directly carry its class content without an intermediate option layer — could reduce the per-aspect evaluation overhead.

Quotient type interpretation (S7). Lazy constructors as quotient types (quotienting A + B by the forcing function) provide a clean semantic model for any “inspectable deferred value” pattern. This interpretation has not been applied to gen-schema’s deferred refs or gen-bind’s thunks (mkThunk), both of which are deferred values that could benefit from the quotient framing.

In-place reuse with reference counting (S3.5). Koka’s combination of lazy constructor reuse with Perceus reference counting achieves zero-allocation forcing in favorable cases. While Nix lacks reference counting, the concept of reusing the “shell” of a deferred value for its result could inform future Nix evaluator optimizations or custom evaluation strategies in gen-scope.

Research Directions

Lazy constructors in a pure lazy language. The paper targets strict languages where laziness must be explicitly introduced. Nix is already lazy, so deferredModule achieves its effect by leveraging Nix’s native thunk mechanism rather than implementing lazy constructors per se. The interesting research question is whether the first-order aspect — making deferred computations inspectable as tagged data — can be achieved more systematically in Nix. Currently, deferredModule achieves inspectability by being an attrset (which Nix can introspect without forcing nested values). A formal treatment of which Nix attrset patterns preserve inspectability-before-forcing would strengthen the theoretical foundation.

Interaction with demand-driven AG evaluation. The paper’s lazy constructors interact with Launchbury’s semantics. gen-scope’s demand-driven evaluation interacts with Nix’s native laziness. Formalizing the relationship — showing that gen-scope’s _eval cache is a correct implementation of the paper’s memoization store under Nix’s evaluation semantics — would connect the two formal systems.

Open lazy constructors (S8). The paper notes that lazy constructors must be declared up-front in the data type, and suggests open data types as a solution. This limitation mirrors gen-aspects, where class keys must be declared in cnf.keySemantics. Exploring open lazy constructors could enable dynamic class registration — aspects contributing to classes not known at type-definition time. This connects to the broader question of extensible scope graphs and open-world AG evaluation.

Palettes adapted from Catppuccin (Macchiato) (MIT), Tokyo Night (Apache-2.0), gruvbox (MIT), Catppuccin (Latte) (MIT), Rosé Pine (Dawn) (MIT).