Leijen (2005) -- Extensible Records with Scoped Labels

The paper

D. Leijen, “Extensible records with scoped labels.,” 2005.

A summary of the paper and how gen uses it.

Leijen, Daan. “Extensible Records with Scoped Labels.” Draft, Revision 76, July 23, 2005. Institute of Information and Computing Sciences, Utrecht University. https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/scopedlabels.pdf

Paper Summary

Records — labeled products — are fundamental building blocks for data structures, yet most programming languages severely restrict their use: labels cannot be reused at different types, records must be explicitly declared, and extensibility is absent. Prior work by Wand (1987), Remy (1993), and Gaster & Jones (1996) introduced row variables and extensible record types, but each system imposed complexity costs: Wand’s system lacked principal types due to ambiguous free extension semantics; Remy’s presence/absence flags produced types unintuitive to users (absent labels appearing in types with abs flags); Gaster & Jones required lacks predicates from qualified types theory, adding both conceptual weight and implementation burden.

Leijen proposes a simpler alternative grounded in a single novel idea: allow duplicate labels in records and retain them, introducing scoped label semantics. Where all prior systems treated free extension (extending a record with a label that may already be present) as an implicit update — overwriting the previous field — Leijen’s system preserves the previous field in both the runtime value and the static type. Selection and restriction operate on the first matching label, so extending a record with a duplicate label effectively shadows the previous binding. Restriction removes the first occurrence, exposing the previous value underneath. This makes records behave as stacks indexed by label, and the type system reflects this precisely: {x :: Int, x :: Bool} is a well-formed type distinct from {x :: Bool, x :: Int}.

The type-theoretic contribution is minimal in surface area but deep in consequence. The entire record system requires only a new equality relation on monotypes (Figure 1, six rules) and an extended unification algorithm (Figures 2-3). Rows are sequences of labeled types, either empty (||) or extended (|l :: t | r|). The critical rule is (eq-swap): two adjacent fields in a row may be permuted if and only if their labels are distinct. This ensures that records are equivalent up to permutation of distinct labels (so {x :: Int, y :: Bool} equals {y :: Bool, x :: Int}) but that duplicate labels maintain their relative order (so {x :: Int, x :: Bool} is NOT equal to {x :: Bool, x :: Int}). Combined with transitivity (eq-trans) and structural equality (eq-head), this gives a complete notion of row equivalence that keeps selection and restriction well-defined even in the presence of duplicates.

The unification algorithm (Section 7, Figure 2) extends Robinson unification with a row rewriting operation (Figure 3). When unifying a row (|l :: t | r|) with some row s, the algorithm rewrites s into the form (|l :: t' | s'|) using label swapping (row-swap), then unifies the field types and tails recursively. A critical side condition in rule (uni-row) — tail(r) not in dom(theta_1) — prevents non-termination when two rows share a common tail variable but differ in prefix (the pathological case \r -> if True then {x = 2 | r} else {y = 2 | r}). Leijen proves:

• Theorem 1 (Soundness) — if two types unify, they are equal under the resulting substitution.
• Theorem 2 (Completeness) — if two types are equal under some unifier, unification succeeds and finds a most general unifier.

These results carry over directly to Hindley-Milner, qualified types, and MLF, since the record extension is purely at the level of monotype equality and unification — no new type rules are introduced. Section 4 demonstrates this composability by using records with MLF to encode first-class modules with impredicative higher-ranked polymorphism, where fields can have universally quantified types (e.g., {id :: forall a. a -> a}).

Section 5 extends the design to variants (labeled sums), which share the same row type infrastructure. Variants use injection, embedding, and decomposition operations. Scoped labels in variants arise through the embedding operation, which can introduce duplicate tags. Decomposition matches on the first occurrence of a label (nesting level zero); the embedding operation increments the nesting level for duplicate labels, enabling principled disambiguation.

Section 8 surveys four implementation strategies with increasing efficiency: association lists (O(n) select), labeled vectors with binary search (O(log n)), labeled vectors with constant folding (amortized O(1) for closed types via partial evaluation), and plain vectors with extension predicates (guaranteed O(1) via evidence translation). The labeled-vectors-plus-constant-folding approach is recommended as the best practical compromise: it uses worker-wrapper transformations to float lookup operations to call sites where record types are known, achieving constant-time selection without the parameter explosion of the predicate approach.

Key Concepts

• Free extension with retention (S2) — extending a record with an existing label pushes a new value rather than overwriting. The previous value is preserved in both the runtime representation and the static type. This cleanly separates the concepts of extension and update, unlike all prior systems (Wand, Remy, Gaster-Jones) which conflated them.
• Scoped labels (S2.1, S3.2) — duplicate labels form a scope stack. Selection returns the topmost (most recently extended) value; restriction pops the top, exposing the previous value. The motivating use case is environment modeling: warning env f = f {color = red | env} temporarily shadows the color field, and f (env - color) restores the parent context’s color.
• Row equality with restricted permutation (S3, Figure 1) — the (eq-swap) rule permits reordering adjacent fields only when their labels differ. This is the sole mechanism preventing permutation of duplicate labels, maintaining stack ordering invariants without additional type-level constructs.
• Orthogonal type system extension (S6) — the record system requires only a new equality on monotypes and extended unification. No new type rules, no predicates, no flags. This makes it embeddable in HM, qualified types, and MLF with minimal effort.
• Row unification with termination guard (S7, Figures 2-3) — the (uni-row) side condition tail(r) not in dom(theta_1) prevents the infinite rewriting loop that afflicts Wand’s system and TREX. Soundness (Theorem 1) and completeness (Theorem 2) are proven in a companion technical report.
• Variants with scoped tags (S5) — the embedding operation <l | v> on variants parallels record extension. Duplicate variant tags require nesting-level tracking at runtime: injection creates level-0 variants, embedding increments the level for duplicates, and decomposition only matches level-0 tags.
• Worker-wrapper compilation for O(1) selection (S8) — for polymorphic records with open row tails, splitting functions into a wrapper (that performs label lookup at the call site where types are known) and a worker (that uses integer indices) achieves constant-time access. This is a variant of GHC’s worker-wrapper transformation.

How gen uses this

gen-algebra

The record algebra in lib/rec.nix implements Leijen’s three primitive operations and the scoped label mechanism. It is exported as record. Every operation takes its label operands first and the record last, so extend l v and select l are partial applications that compose over records.

• Representation — records use { __entries = { label = [value-stack]; }; __order = [labels]; }, an attrset-with-shadow-stack encoding. Each label maps to a list representing the scope stack. Extension pushes onto the head of the stack, restriction removes the head, selection reads the head.
• record.extend label value r — Leijen S2 extension {l = e | r}. Pushes value onto the label’s stack. If the label already exists, the previous value stays underneath (free extension with retention).
• record.select label r — Leijen S2 selection r.l. Returns the head of the label’s stack (first matching label). Throws if the label is absent.
• record.restrict label r — Leijen S2 restriction r - l. Pops the head of the label’s stack. If the stack had depth > 1, the previous value becomes visible to select, the scoped label exposure of S2.1 (the warning env f pattern). Restricting an absent label returns the record unchanged.
• record.has label r / record.depth label r — label presence and stack height. depth is the number of duplicate extensions.
• record.update label value r — Leijen S2 derived operation {l := x | r} = {l = x | r - l}. Replaces the head of the stack and throws if the label is absent. record.upsert is the non-strict form, extend after restrict.
• record.emit r — collapses the shadow stack to a plain attrset of heads. record.emitAll labels r keeps the full stacks for the listed labels.
• record.combine { left; right; } — left-biased combination. For each label, the left record’s stack sits above the right record’s stack.
• record.satisfies required r / record.assertSatisfies — label presence checks (S3.1). They validate that a record contains all required labels, the runtime counterpart of the paper’s guarantee that selection and restriction apply only to present fields.
• record.mixin delta parent / record.compose m1 m2 — mixin composition (Bracha & Cook 1990) over Leijen’s records. mixin computes delta parent combined over parent, so the delta’s values sit on top of each label’s stack.

Selection is a Nix attrset lookup, which matches the constant-time cost of Leijen’s labeled-vector approach (S8). Restriction adds a list tail per label.

gen-bind

gen-bind injects named values into module functions. When a bound name collides with an argument the module system already provides (both supply lib, say), the merge strategy in lib/merge-strategy.nix decides:

• bind-wins (the default) — the binding shadows the module-system argument, like Leijen’s first-match selection returning the most recent extension.
• error — a collision throws. This mirrors strict extension (S2.1, the Gaster-Jones style), where extending with a present label is a type error.
• system-wins — the module-system argument wins and the binding is dropped.

gen-bind merges with plain attrsets rather than shadow stacks, so the correspondence is at the level of the strategy vocabulary.

gen-schema

gen-schema builds on gen-algebra’s records in two places:

• Mixin application (lib/mixin.nix) — applyMixin checks the mixin’s requires labels against the kind’s record with record.assertSatisfies, then applies it with record.mixin (the mixin wins) or record.combine (the kind wins, for Beta-style mixins).
• Module emission (lib/bridge.nix) — emitModule turns a record into a NixOS module. It uses record.emitAll to keep the full stacks of collection labels, so every value accumulated across extensions reaches the module, and collapses the other labels to their heads.

Further directions

Unexploited Ideas

• Variant types with scoped tags (S5) — gen-algebra implements record algebra but not variant algebra. Leijen’s variants use the same row infrastructure, adding injection, embedding, and decomposition operations. The embedding operation’s nesting-level increment for duplicate tags is unimplemented. Variants would model tagged union types (e.g., rule action kinds, entity types as labeled choices) with the same scoped label guarantees.

• Evidence translation for guaranteed O(1) selection (S8, extension predicates) — gen-algebra achieves O(1) select via Nix’s native attrset lookup, but the evidence-translation approach (extension predicates turned into runtime offset parameters) is unexploited. In a compiled setting, this would guarantee constant-time access even for polymorphic records with open row tails. Not directly applicable in Nix (interpreted, lazy) but relevant if the ecosystem ever targets a compiled backend.

• Worker-wrapper transformation for open records (S8) — Leijen’s technique of splitting functions into a wrapper (performs lookup at monomorphic call site) and a worker (uses integer indices) is applicable to gen-scope attribute access patterns. Currently, attribute access goes through string-keyed attrset lookup; a pre-computed index mapping could amortize lookup costs for frequently accessed attributes across large fleets.

• Row unification as a first-class operation (S7) — the unification algorithm could power a structural compatibility checker that goes beyond gen-algebra’s record.satisfies (which checks label presence only). Full row unification would check type compatibility of corresponding fields, enable inference of the most general record type for a set of constraints, and detect incompatible record extensions statically. This would strengthen gen-schema’s mixin compatibility validation.

• First-class modules via records + MLF (S4) — Leijen shows that records with impredicative higher-ranked polymorphism encode first-class modules where fields can have universally quantified types. NixOS modules are already first-class values in Nix, but they lack the static type guarantees. A future type-checking layer for Nix could use Leijen’s encoding to give NixOS modules typed interfaces with polymorphic fields.

Research Directions

• Scoped labels and monotonic scope graphs — Leijen’s (eq-swap) rule (only distinct labels may permute) interacts interestingly with Neron (2015) scope graph resolution order (D < I < P). When scope graph nodes carry records with scoped labels, the combination of resolution specificity and label scope depth creates a two-dimensional override lattice. The formal properties of this combination (confluence, monotonicity under graph extension) are unexplored.

• Lazy record restriction as demand-driven scope narrowing — in Nix’s lazy evaluation model, record.restrict is only evaluated when a consumer demands the restricted record. This means scope narrowing (exposing a parent’s value by restricting a child’s override) is demand-driven, aligning with gen-scope’s demand-driven attribute evaluation. Whether this can be formalized as a lazy record calculus with demand-driven scoping — combining Leijen’s records with Chitil’s (2012) lazy contracts — is an open question.

• Mixin composition under scoped labels — Bracha & Cook (1990) assume records without duplicates. gen-algebra composes Bracha’s mixin formula over Leijen’s shadow-stack records, but the formal interaction properties (associativity, commutativity of independent mixins, idempotence) under scoped labels have not been verified. In particular, whether compose m1 m2 over shadow-stack records satisfies the same algebraic laws as over flat records when both mixins touch the same label at different depths.