Row Polymorphism for Extensible Records

A function that reads one field from a record and ignores the rest should be usable with any record that has that field. Subtyping can express this, but only by giving the function a supertype and requiring a coercion or a layout-compatible subtype at each call. A row type expresses it directly: the function’s type names the fields it needs and leaves a variable standing for everything else. The mechanism is small, but its interaction with unification has two sharp edges that explain most of the design decisions in languages that use it.

Rows are unordered maps with a tail

A row is a finite association of labels to types, plus a tail that is either the empty row or a row variable. Written as a grammar, a row is ⟨⟩, ⟨l : τ | Row⟩, or ρ.

The record type { ρ } wraps a row. A record with fields x : Int and y : String and nothing else is { ⟨x : Int, y : String | ⟨⟩⟩ }. The same record with an open tail is { ⟨x : Int, y : String | ρ⟩ }, meaning: these two fields, and possibly others described by ρ.

The critical property is that rows are unordered. ⟨x : Int, y : String | ρ⟩ and ⟨y : String, x : Int | ρ⟩ denote the same row. A checker that treats rows as ordered lists — the obvious implementation — will fail to unify types that should be equal, and the fix is either to canonicalize rows into a fixed order before comparison or to use a unification algorithm that is insensitive to order. Canonicalization is cheaper per comparison but requires a sort on every row built, which is linear in the number of fields.

A second property: labels within a row are distinct. A row ⟨x : Int, x : String | ρ⟩ is not a legal type, and the constraint that enforces this is called a lacks constraint (also written as a side condition l ∉ ρ). It is what makes extension well-defined — adding x to a row is only permitted when the row does not already have x.

Reading a field

The type of field selection is the whole mechanism in one rule: from e : { ⟨l : τ | ρ⟩ } and the side condition l ∉ ρ, selection yields e.l : τ.

The side condition l ∉ ρ says the tail does not contain the label being selected. Without it, the row could contain a second l with a different type, and the result type would be ambiguous. Equivalently, the checker can start from e’s inferred type, add the lacks constraint, and let unification absorb whatever fields the record actually has into ρ.

In practice, selection on a closed record needs no such check: the row is fully known, and the label is either present with one type or absent. Selection on an open record needs it because ρ is a variable that may later be bound to a row containing l. The checker therefore records a lacks constraint on ρ and solves it when ρ is resolved. If ρ later unifies with ⟨l : σ | ρ'⟩, the constraint fails and the program is rejected — correctly, since the record would then have two fields with the same label.

An implementation of selection:

def select(env, expr, label):
    t = infer(env, expr)                       # record type { row }
    field_ty, tail = fresh_var(), fresh_var()
    row = Row({label: field_ty}, tail)
    unify(t, Record(row))                      # record's row: label: field_ty | tail
    constrain_lacks(tail, label)               # side condition on the open tail
    return field_ty

The order matters: the row is built with the label first and a fresh tail, and unification with the record’s row determines the remaining fields. If the record has the label, the tail becomes the rest of its row; if the record’s row is closed and lacks the label, unification fails immediately. The lacks constraint on the tail is what prevents tail from later absorbing a duplicate label.

Extension, restriction, and the lack of scoped labels

Record extension adds a field: { ρ } becomes { ⟨l : τ | ρ⟩ } when l ∉ ρ. Record restriction removes one: { ⟨l : τ | ρ⟩ } becomes { ρ }.

Both are structural operations with constant cost in the type system: extension builds one row cell, restriction decomposes one. At run time, extension allocates a new record — a copy of the old one plus one field — so a loop that extends a record n times costs Θ(n²) work in total, the same shape as repeated string concatenation. Languages that expose extension as a primitive therefore usually also expose a bulk merge or a mutable build path, and the type system treats both as ordinary operations on rows.

The subtlety is label shadowing. Consider merging ⟨x : Int | ρ⟩ with ⟨x : String | σ⟩.

There are two coherent answers. The first says the merge is ill-typed unless the label is absent from one side, which is the strict rule and requires a lacks constraint on every merge. The second, introduced by Leijen as scoped labels, says the right-hand occurrence shadows the left and the resulting row keeps both, with the leftmost duplicate — the one belonging to the record being extended — accessible by selection and the rightmost shadowed. Scoped labels make merges total and make the type system’s rows behave like a stack of bindings. The cost is that rows are no longer sets of distinct labels, so the lacks constraint is replaced by a different side condition, and equality of rows becomes equality up to shadowing rather than up to permutation.

The strict rule is easier to implement and produces better error messages, because a duplicate label is reported at the merge site rather than resolved silently. Scoped labels admit more programs, particularly in code that layers defaults under overrides.

Why rows beat width subtyping for this purpose

The alternative to a row type is width subtyping with a record supertype, as described in structural subtyping and variance. The comparison comes down to three differences.

Direction of information. With subtyping, the function is declared to accept { x : Int } and the caller must supply a subtype. The function’s type does not say what it does with the other fields, because it cannot see them. With rows, the function’s type is { ⟨x : Int | ρ⟩ } → τ and ρ is quantified: the function is polymorphic in the rest of the record, and the caller’s record can have any shape that includes x. The second is a stronger statement and lets the checker accept the call without a coercion.

Composition. Two functions that each read a different field can be composed without knowing the union of their requirements in advance. The first has type { ⟨x : Int | ρ⟩ } → A and the second { ⟨y : String | σ⟩ } → B; a caller that supplies a record with both fields instantiates ρ and σ appropriately. Under width subtyping, the same composition requires the caller to construct a record that is a subtype of both supertypes, which is possible for records but not for every type.

Cost of inference. Row unification requires solving lacks constraints and canonicalizing unordered rows. Width subtyping requires solving inequalities rather than equalities, which as noted in the previous article means the solver produces least upper bounds rather than principal types. For records specifically, rows give principal types and subtyping does not, which is why languages that infer record types use rows. The principal-type guarantee itself comes from the unification algorithm, and rows preserve it because the constraint form is still equality.

The occurs check, again

A row variable can be bound to a row containing itself only through a recursive type, and the occurs check applies to rows exactly as it does to types. The check visits each node of the candidate type once, so its cost is linear in that type’s size, and it is paid on every unification that binds a variable. The interesting case is not a direct cycle but a cycle through a record: unifying ρ with ⟨x : { ρ } | ρ'⟩.

Substituting gives a record whose x field is a record with the same shape, which is a recursive type and has no finite representation. A checker must reject it unless the language has equirecursive types, in which case the cycle is legal and the unification algorithm must compare types up to bisimulation rather than up to syntactic equality. Equirecursive types make the occurs check into a coinductive check: instead of failing on a cycle, the algorithm assumes the cycle holds and continues, which terminates because there are finitely many pairs of subterms to compare.

Most languages with rows choose the inductive reading and keep the occurs check. The practical consequence is that a record type cannot directly contain itself; recursion must go through a named type or a function, which introduces the indirection needed to make the type finite.

What rows do not solve

Rows describe which fields are present. They say nothing about what the fields contain beyond their types, so a function polymorphic in ρ cannot require that every field of ρ satisfy a constraint. A type like “a record all of whose fields are Int” is not expressible with a row variable alone; it needs a constrained quantification over rows, which most row systems do not have.

Rows also do not give subtyping between record types. { ⟨x : Int | ρ⟩ } and { ⟨x : Int, y : Int | σ⟩ } are unrelated types unless one instantiates the other’s tail. A function expecting the first can be applied to a value of the second by instantiating ρ to ⟨y : Int | σ⟩, which is exactly the substitution the checker performs, but there is no general relation that admits the application without that instantiation. Languages that want both rows and subtyping must define how the two interact, and the interaction is where most of the complexity in such systems lives.

Finally, rows interact with type classes and traits in a way that is easy to get wrong. A constraint attached to a row-polymorphic function is a constraint on the field types the function names, not on the record as a whole: a function of type forall r. Show a => { x : a | r } -> String needs Show a and nothing more, and the fields hiding behind r are untouched. Requiring every field of the row to have an instance is a different constraint — it would need quantification over the row’s members, which row types alone do not provide.