Chitil (2012) — Practical Typed Lazy Contracts

Paper Summary

Chitil addresses a gap in the functional programming toolbox: prior to this work, no practical contract system existed for lazy functional languages. Contracts — pre- and post-conditions for functions — had become standard equipment for eager languages like Racket following Findler and Felleisen’s seminal 2002 work, but three obstacles blocked their adoption in Haskell and similar lazy languages.

First, Racket’s contract system relies on macros for ergonomic integration (e.g., automatic source location capture), and other languages lack equivalent metaprogramming facilities. Second, statically typed languages with Hindley-Milner type systems demand that contract combinators have simple parametrically polymorphic types — adding a contract should never change a function’s type signature, yet prior approaches (e.g., HOOD’s observe) introduced class constraints that propagated through entire programs. Third, and most critically, eager contracts are fundamentally incompatible with lazy evaluation: asserting list nat over [4, -1, 2] should yield [4, error, 2] (replacing only the violating element), not a monolithic error that prevents access to the valid prefix. Without this property, contracts on infinite data structures (e.g., the Fibonacci sequence) are impossible, and adding contracts anywhere in a program can change its semantics even when no contract is violated.

The paper’s core contribution is a contract type Contract a = a -> Maybe a that supports both conjunction (&) and — critically — disjunction (|>), the combinator that prior lazy contract systems could not implement correctly. The Maybe wrapper allows a pattern contract to report “this constructor doesn’t match” (returning Nothing) without raising an error, enabling the disjunction combinator to try the next alternative. This is the key insight: the earlier contract type a -> a suffices for all combinators except disjunction, because composition of partial identities cannot catch and recover from failures in a purely functional setting.

Chitil introduces pattern contracts — combinators like pNil, pCons that match on the outermost data constructor and attach sub-contracts to its fields. Pattern contracts compose via disjunction to define contracts that mirror algebraic data type definitions:

list c = pNil |> pCons c (list c)

The paper builds on this structural parallel between type definitions and contract definitions, identifying contracts as a practical subtyping system for algebraic data types, particularly useful for compiler passes that operate on overlapping AST variants.

The central theoretical result is that contracts are projections — they are both partial identities and (claimed) idempotent. Lemma 4.1 proves the partial identity property: assert c <= id in the information-theoretic ordering, meaning a contract can only reduce information (replace parts with bottom), never add it. Claim 4.2 asserts idempotence: assert c . assert c = assert c. The paper provides a proof appendix (Appendix A) establishing the partial identity property by structural induction on contract combinators, and shows that idempotence follows from idempotence of conjunction (c & c = c), which is claimed but left as requiring stronger proof methods than equational reasoning.

The algebra of contracts (Figure 4) is rich: conjunction is associative with true as identity and false as annihilator; disjunction is associative with false as identity; function contracts distribute with conjunction via (c1 >-> c2) & (c3 >-> c4) = (c3 & c1) >-> (c2 & c4). Importantly, neither conjunction nor disjunction is commutative — paralleling the non-commutativity of && and || on lazy Booleans, and the paper uses this parallel systematically to predict which lattice properties hold and which fail.

The paper extends the basic system with blame tracking (Section 5.1, following Findler-Felleisen’s covariant/contravariant blame assignment), witness tracing (Section 5.2, reporting the path through the data structure to the violation point), Template Haskell code generation for pattern contracts (Section 6), IO monad contracts (Section 7.2), and treatment of strict data types where lazy contracts naturally degenerate to eager behavior (Section 7.3). The dependent function contract combinator >>-> is presented as future work — it necessarily breaks laziness because the post-condition may force evaluation of the function argument.

Key Concepts

Lazy contract semantics: Asserting a contract over a data structure replaces only violating parts with bottom; unevaluated parts can never violate a lazy contract. This preserves the lazy evaluation semantics of the host language — adding contracts is a no-op when contracts are satisfied.
Contract type a -> Maybe a: The Maybe wrapper is the minimal extension over a -> a that enables disjunction. Just v means the outermost constructor matches (with sub-contracts attached to fields); Nothing means mismatch at the top constructor; bottom means non-termination or deeper failure. The Maybe monad’s >>= implements conjunction and mplus implements disjunction.
Pattern contracts: Per-constructor combinators (pNil, pCons, pAnd, etc.) that test only the outermost constructor. This shallow inspection is what makes contracts lazy — they never look deeper than one constructor level before returning.
Contracts as projections (Lemma 4.1 + Claim 4.2): assert c is a partial identity (assert c v <= v) and is idempotent (assert c . assert c = assert c). This means applying a contract twice is the same as applying it once, and a contract can only remove information from a value.
The false contract and its blame direction: false always blames the client, which is practically useful in contra-variant positions: true >-> false >-> true on const correctly blames the server (the function definition) if the second argument is demanded, because false is in a contra-variant position where blame is flipped.
Witness tracing (Section 5.2): Beyond binary blame, the contract system reports a witness — the path through constructors from root to the violation point. This is strictly more informative than Findler-Felleisen blame.
Strict data types degenerate to eager contracts (Section 7.3): When all constructor arguments are strict, demanding the top constructor forces the entire structure, so lazy and eager contracts produce identical behavior. The system adapts automatically.
Non-commutativity parallels lazy Booleans: The contract algebra mirrors the algebra of && and || over lazy Booleans — neither conjunction nor disjunction commutes, the standard distribution laws fail, but guarded commutativity and absorption laws hold. This parallel is both a proof technique and an intuition guide.

How gen uses this

gen-bind: contracts on injected arguments

gen-bind cites Chitil’s central result, contracts as partial identities (S4.2), for its lazy contracts on the values it injects into NixOS modules.

contract.mk creates a contract record around a check predicate. The predicate is Chitil’s prop combinator for flat types (S2): it tests a value without forcing anything beyond what the predicate demands.
contract.apply is assert c, the partial identity: it returns the value unchanged when the check passes and throws with blame information when it fails. Its provenance argument carries the source and scope into the error message, which is the blame tracking of S5.1.
contract.hasFields, contract.isType and contract.nonEmpty are ready-made flat contracts, specific instances of prop.
wrap applies contracts inside each binding’s thunk, so an assertion runs only when evalModules forces that argument. This is Chitil’s core guarantee that unevaluated parts never violate a contract (S2, the Fibonacci example). A module that takes { host, ... }: and never reads host.system never triggers a contract on system.
wrapAll computes contracts once for a list of modules. Sharing them is sound because a contract is idempotent (Claim 4.2).

gen-bind’s contracts are flat assert-style checks. It does not implement the a -> Maybe a contract type, pattern contracts or disjunction, since the values passed through a binding are mostly flat attrsets and Nix has no user-defined algebraic data types to pattern-match on.

gen-schema applies Chitil’s lazy semantics to refinement types on registry instances.

refined attaches refinements { check; message; lazy ? false; } to a type. Each refinement is a predicate that acts as a partial identity on the type’s values.
When an instance registry validates its fields, a refinement with lazy = true does not run at validation time. The field’s value is wrapped with builtins.addErrorContext and a check that throws on access, so the value behaves exactly like the unwrapped one until the violating part is demanded. This is Lemma 4.1, assert c v <= v. Refinements without lazy fail immediately.
A list of refinements on one type is a conjunction: every refinement must pass. Lemma A.5, assert c2 . assert c1 = assert (c1 & c2), is why checking them in sequence is correct.

blame builds a { field, message } record for field-level error attribution. It is producer-side reporting of which field and which predicate failed, and does not implement Chitil’s higher-order blame or witness tracing.

gen-schema uses builtins.addErrorContext and a deferred throw as its laziness mechanism, where the paper constructs Maybe-wrapped values. The guarantee is the same: the check runs only when the value is demanded.

Why laziness matters here

A gen configuration is evaluated on demand. Scope-graph attributes are computed only when something needs them, and class content stays as deferredModule thunks until evalModules imports it. Lazy contracts keep that property.

Contracts add no demand. If contracts were eager, attaching one to a binding would force the binding, which forces the attribute behind it and possibly a whole subtree. Lemma 4.1 says assert c v is no more defined than v, so a contract cannot introduce new demand.
Unbuilt hosts cost nothing. A fleet may declare hundreds of hosts while one nix build targets one host. The other hosts’ bindings are never demanded, so their contracts never run. This is the S2 property: “a computation may succeed without any contract violation error, if it only demands those data structure parts that meet the contract.”
Checks run where values are used. A lazy refinement on a registry field, for example a port with check = p: p > 0 && p < 65536; lazy = true;, fires when that host’s port is read, as part of normal evaluation, with no separate pass that materialises the whole graph.
Repeated application is safe. The same aspect can be reached along several scope-graph paths. Idempotence (Claim 4.2) means a contract applied twice to a value behaves as if applied once, independent of wrapIdentity deduplication.

Appendix: Follow-up Work

Unexploited Ideas

Dependent function contracts (Section 9, >>->). Chitil’s >>-> lets the post-condition read the actual argument, and notes that this breaks laziness. In Nix it would allow relational contracts such as “the output module’s networking.hostName equals the input host.name”. Such a contract forces the argument. Some bindings, such as a host’s entity context, are always forced by the host’s configuration, and for those a dependent contract adds no evaluation cost.
Pattern contracts (Sections 3-4). gen-bind has flat predicate contracts only. Pattern contracts with disjunction (|>) would give structural contracts on nested attrsets, such as “either { type = "host"; addr = ...; } or { type = "user"; shell = ...; }”, matching the top-level keys and attaching sub-contracts to fields. This is Chitil’s pCons and pNil with the attrset replacing the list constructors.
Witness tracing (Section 5.2). gen-bind’s blame messages carry provenance (source, scope) and no structural witness, the path through the data to the violation. Chitil accumulates String -> String context transformers along the path. In Nix this is attrpath accumulation, reporting host.users.tux.shell.
Contract algebra for simplification (Section 4, Figure 4). The laws true & c = c, c & true = c and true >-> true = true allow simplifying contract expressions ahead of time. gen-bind and gen-schema check every contract independently. A composition layer could fuse hasFields ["name"] & hasFields ["system"] into hasFields ["name" "system"] and drop true >-> true on pass-through bindings.
Contracts for abstract types (Section 7.2). Chitil defines io c = \io -> Just (io >>= return . assert c) for IO and notes that abstract types need combinators built from their map. The Nix analogues are derivations and paths, opaque until built. A derivation contract would check the output after the build, a different execution model built on the same type-directed principle.

Potential New Libraries or Features

A shared contract combinator vocabulary. gen-bind and gen-schema each define their own contract primitives. A shared vocabulary of mk (flat), hasFields, conjunction, disjunction (try the first, fall back), negation and function contracts (pre and post) would unify them and make the Figure 4 laws available for simplification.
Structural witness tracing for gen-bind. Thread an attrpath prefix through contract.apply on nested attrsets, so a violation reads at host.users.tux: value must have fields: name, system. wrap would pass path context through its recursive wrapping.
Dependent contracts for bindings that are always forced. For bindings every consumer destructures, allow contract.dependent { pre; post; } where post receives both the input binding and the module’s output. This is >>-> restricted to the safe case, and needs gen-bind’s signature to mark which bindings are always forced.

Research Directions

Completeness against meaning preservation. Degen, Thiemann and Wehr (2012, cited as [8]) prove no contract system is both meaning-preserving and complete. Chitil’s system preserves meaning and is incomplete: a violation in a part never demanded is never detected. For a fleet that is useful, since unbuilt hosts pass silently. Fleet-wide validation tooling would want a complete mode that forces every contract. Whether one library can offer both modes cleanly, or whether completeness needs full materialisation and eager checking, is open.
Contract inference from option types. gen-schema refinements are declared by hand. Chitil’s type-directed combinators suggest deriving contracts from NixOS option types: lib.types.int gives contract.isType "int", lib.types.enum vals gives a membership check, and lib.types.attrsOf t gives a recursive pattern contract.
Contract-preserving mixin composition. gen-schema’s mkMixin and composeMixins operate on records. If records carry refinements, composition should keep both the parent’s and the mixin’s, using Chitil’s conjunction law (c1 >-> c2) & (c3 >-> c4) = (c3 & c1) >-> (c2 & c4) (Lemma A.22). Mixin composition does not combine refinements today. A contract-aware combinator would give the composed record the conjunction of both sets, and the laws guarantee the result is still a projection.

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