Findler & Felleisen (2002) — Contracts for Higher-Order Functions

The paper

R. B. Findler and M. Felleisen, “Contracts for higher-order functions,” ICFP02: International Conference on Functional Programming, pp. 48–59, 2002.

doi:10.1145/581478.581484

A summary of the paper and how gen uses it.

Paper Summary

Findler and Felleisen address a fundamental gap in assertion-based programming: while Design by Contract (Meyer’s Eiffel philosophy) was well-established for first-order procedural and object-oriented languages, no principled mechanism existed for enforcing contracts on higher-order functions. The difficulty is twofold: (1) predicates on function values are undecidable in general, so a contract on a function-typed argument cannot be checked at the call site; and (2) blame assignment — identifying which party violated a contract — becomes entangled when functions pass through multiple boundaries.

The paper’s central insight is that contract enforcement for higher-order values must be deferred: rather than checking a function contract when a higher-order argument is received, the contract system wraps the function so that its domain contract is checked when the function is eventually applied, and its range contract is checked when it returns. This wrapping can cascade — each arrow in a contract type induces a distribution step at the corresponding application site during evaluation.

The formal vehicle is lambda-CON, a typed lambda calculus with first-class contracts. The calculus introduces obligation expressions e^{c,p,n} where c is the contract, p is the positive party (value producer), and n is the negative party (value consumer). Two reduction rules are central: the flat rule checks a predicate contract on a first-order value and blames the positive party on failure; the hoc (higher-order contract) rule distributes a function contract (C_D -> C_R) at an application by moving C_D to the argument and C_R to the result, while swapping the blame labels on the domain portion. This swap is the formal encoding of contravariance in blame assignment.

The paper establishes the even-odd rule for blame: a base predicate appearing an even number of times to the left of an arrow is in covariant (positive) position — the function itself is responsible. An odd number of nestings puts it in contravariant (negative) position — the caller is responsible. This directly parallels the variance of function types in subtyping theory.

The authors prove type soundness for lambda-CON (Theorem 6.2) via standard preservation and progress lemmas, and then prove compiler correctness (Theorem 6.7): the compiled implementation (using the wrap meta-function that recursively wraps values according to their contracts) produces the same observable results as the instrumented calculus semantics. The proof introduces an intermediate semantics (wrap-reduction) and shows E = E_fw = E_fh — the three evaluators (compiled, wrap-based, and hoc-based) agree on all programs.

Section 7 extends the calculus with dependent contracts — range contracts that are functions of the input value. The dependent contract reduction applies the range function to the actual argument before wrapping the result, enabling stateful pre/post-condition patterns (e.g., checking that a callback preserves invariants by capturing state before the call and comparing after).

Section 8 discusses the interaction with tail recursion: post-condition checking inherently breaks tail-call optimization for contracted functions. The authors argue this is acceptable because contracts are most valuable at module boundaries, which are rarely in tight loops — a conjecture supported by experience in the DrScheme codebase.

Throughout, the paper grounds its contributions in real examples from DrScheme’s implementation: preferences panel callbacks, mixin contracts for IDE extensions, and thread-safety contracts for plugin thunks. These examples demonstrate that the contract system captures invariants that no existing type system (including OCaml’s and OML’s) could express statically.

Key Concepts

• Deferred enforcement: Higher-order contracts cannot be checked at the call site; they must be deferred until a first-order value is produced or consumed. Each arrow in a contract type induces a wrapper that distributes checking to the appropriate application.

• Blame labels and the even-odd rule: Every obligation carries two labels (positive/negative). Flat contract failures blame the positive party. At each arrow distribution, labels swap on the domain side — encoding covariant (even depth) and contravariant (odd depth) blame assignment.

• The wrap function: A recursive contract compiler that case-splits on flat vs. function contracts. For flat contracts, it tests the predicate and blames the positive party on failure. For function contracts, it builds a wrapper lambda that recursively wraps both the argument (with swapped blame) and the result.

• lambda-CON calculus: Typed lambda calculus with obligation expressions, two contract reduction rules (flat and hoc), and a type system that ensures contracts match the types of their subjects. Type soundness proved via Wright-Felleisen method.

• Compiler correctness (Theorem 6.7): The compiled form (using wrap) is observationally equivalent to the instrumented calculus. Proved via an intermediate wrap-reduction semantics that bridges the two.

• Dependent contracts: Range contracts parameterized by input values, enabling pre/post-condition patterns with captured state. Formally, C_D ->d (lambda(arg) C_R) where the range contract is computed from the actual argument.

• First-class contracts: Contracts are values — they can be abstracted, composed, and passed to functions. This enables reusable contract patterns (e.g., mixin-contract/intf in DrScheme).

• Contravariance as blame inversion: The fundamental connection between type-theoretic variance and runtime blame assignment. Domain position is contravariant; each nesting inverts who is responsible.

How gen uses this

gen-bind

gen-bind applies Findler’s blame tracking and blame assignment to the values it injects into NixOS modules.

Provenance as blame labels (S2.3, S4). A wrap call can carry provenance, { source; scope ? null; }, which plays the role of Findler’s blame labels. When a contract fails or a collision is detected, the error names the responsible source and scope, as λCON’s blame("p") names the responsible definition. provenance.format renders it, and it appears in both contract failures and collision errors.

Blame in collision handling (S2.3). When a binding’s name collides with an argument the module system already supplies, gen-bind’s merge strategy decides which party is responsible:

• bind-wins (the default): the binding shadows the module-system argument, so the binding’s provider answers for the value.
• system-wins: the module-system argument wins and the binding is dropped.
• error: neither side accepts the collision, and gen-bind throws with both parties named.

mkMergeValidator builds a validator that checks module arguments for collisions and attributes them according to the strategy. This is a two-party form of Findler’s blame assignment, with the binding source on one side and the module system on the other.

Lazy contract wrapping (S5; see also Chitil 2012). contract.mk builds assertions that fire when a value is demanded, not when it is wrapped. For a flat contract this matches wrap in Figure 9: test the predicate and blame the positive party on failure. gen-bind runs in a lazy language, so Nix’s evaluation provides the deferral that Findler’s system builds from explicit wrapper lambdas. The contract functions are contract.mk, contract.hasFields, contract.isType, contract.nonEmpty and contract.apply.

Signatures as contract interfaces (S3-4; see also Cardelli 1997). buildSignature returns { requires, bound, unsatisfied, declaredMergeStrategies }, a lightweight analogue of an obligation’s contract component. It records what a module expects and what was provided, and its unsatisfied entries are the candidates for blame.

gen-schema

gen-schema applies Findler’s predicate contracts to typed registries.

Refinement contracts (S1-2, S3). refined attaches predicate contracts to a type. A refinement { check = self: self > 0; message = "must be positive"; } corresponds to Findler’s contract(lambda x. x >= 0), a flat predicate contract guarding a base type. check is the predicate and message is the blame annotation. Several refinements on one type must all pass, which is conjunction of flat contracts. Instance registries check refinements when they validate their fields.

Lazy refinements (S5; see Chitil 2012). A refinement with lazy = true is not checked at validation time. The field’s value is wrapped with builtins.addErrorContext and a check that throws on access. In Findler’s terms the obligation travels with the value until a first-order observation occurs.

Blame records. blame builds a record { __blame = true; field; message; } that names the field and the violation. The field component plays the part of the variable names in Findler’s obligation expressions (e^{c,p,n}, where p identifies the responsible definition). It is producer-side attribution and does not implement higher-order blame.

Validators (S2.1-2.2). A validator from mkValidator { name; pred; message; } is a named flat contract evaluated against every instance of a kind. validateInstances collects all failures into an Either ({ right = instances; } or { left = [ failure ]; }) instead of throwing on the first. Collecting every error goes beyond Findler’s fail-fast semantics and suits configuration validation, where users want all errors at once.

Contracts at the evaluation boundary

gen-bind carries values computed on a scope graph into NixOS modules, and that crossing is a trust boundary. Its contracts guard the boundary as Findler’s contracts guard module boundaries in λCON, and the provenance can carry the producing scope’s identity (for example "host=igloo,user=tux") so blame traces back to the node that produced the value.

A contract is installed when the value is bound and fires only when the consuming module demands the argument. Hosts whose configurations are never evaluated pay nothing, which matches Findler’s principle that contract overhead should follow actual use.

gen-bind’s mkThunk defers a binding until evalModules supplies config. A thunk can capture scope state when it is defined and compare it with module-system state when it resolves, which gives the pre- and post-condition pattern of Findler’s dependent contracts (Section 7).

Appendix: Follow-up Work

Unexploited Ideas

Dependent contracts for cross-entity invariants (S7, Figure 12). Findler’s C_D ->d (lambda(arg) C_R) makes the range contract a function of the input. gen-bind’s contracts are flat and check one binding in isolation. Dependent contracts would express invariants such as “if the host binding has role = "web", the port binding must be between 80 and 443”, with the contract capturing the host value and producing a port-specific range check. contract.mk would need to accept a function from binding context to contract.

First-class contract composition (S2.4, Figure 3). The paper treats contracts as first-class values that can be abstracted, parameterised and composed. gen-bind’s hasFields, isType and nonEmpty are individual predicates with no combinators. and, or, not and implies combinators would express complex binding contracts compositionally, like Findler’s mixin-contract/intf pattern where contract factories produce specialised contracts.

Contract monitoring across boundaries (S2.2, S4). Findler’s system follows a contract from establishment to discovery across distant call sites. gen-bind checks a contract at one point, when the binding is demanded. A monitoring mode that follows a value from scope-graph emission through wrapping to evalModules would help debug deep configuration paths. The value would carry obligation-style wrappers that survive lazy evaluation.

Blame for nested function contracts (S2.3, S4 hoc-reduction). gen-bind handles flat contracts and no function contracts. Parametric aspects ({ host, ... }: { nixos = ...; }) cross scope boundaries. A contract on such a function, for example “given a host with system = "x86_64-linux", the aspect must produce a nixos key”, needs the full hoc-reduction with blame labels swapped at each application.

Potential New Libraries or Features

A shared contract algebra. Contract constructors (flat, function, dependent), combinators (and, or, not, implies), blame label management and a wrap that works on Nix attrsets and functions. It would give gen-bind’s contracts and gen-schema’s refinements one foundation, and could extend to aspect-level invariants in gen-aspects.

Dependent contracts in gen-bind. Add contract.dependent, taking a function from the full binding attrset to a contract so predicates can span fields. For example: contract.dependent (bindings: contract.mk { message = "public hosts need valid ports"; } (v: v.port > 0 || !bindings.host.isPublic)).

A monitoring mode for gen-bind. A debug wrapper that records obligation metadata on bound values (source scope, contract, where it was established). A failing contract would then report the full provenance chain: where the value was produced and every scope it passed through, not only where it was bound.

Research Directions

Contract inference from NixOS types. gen-schema refinements are declared explicitly. An inference pass could derive flat contracts from option types: types.int implies builtins.isInt, types.enum values implies membership, types.port implies the range 0-65535. This would give every gen-bind binding a baseline contract without annotation, in line with Findler’s observation that contracts and types play “synergistic roles” (Section 3).

Blame propagation through resolution. When gen-scope resolves a name (D < I < P specificity), the resolution path identifies the scope that contributed the value. Reifying that path as a blame chain would let a later contract violation trace back to the declaring scope, joining Findler’s blame tracking with Néron’s scope-graph resolution.

Contracts for parametric aspects. Parametric aspects are higher-order in Findler’s sense: functions from scope arguments to configuration. A contract on one needs the full hoc-reduction. The domain contract checks the scope arguments and the range contract checks the produced configuration. By the even-odd rule, a bad output blames the aspect and bad arguments blame the entity declaration.