Structural Subtyping and the Variance Lattice

A type system that only knows equality forces every value to have exactly the type its context demands. Real programs pass records with extra fields to functions that read a subset, and pass functions that accept fewer cases where more are expected. Subtyping is the relation that licenses those substitutions, and the rules governing it are constrained by a small number of soundness arguments that dictate, field by field, which directions are safe.

Width: more fields is a subtype

A record type lists field names and their types. The width rule says that a record with additional fields is a subtype of a record with fewer: { x: Int, y: Int, z: Int } <: { x: Int, y: Int }.

The justification is a substitution argument. Any expression expecting the right-hand type will only project x and y. A value of the left-hand type has both fields, at the same offsets relative to the record’s start, so every projection the context performs succeeds and returns the expected type. The extra field is never read, so its presence cannot be observed.

That argument depends on the record’s layout being prefix-compatible: the fields named in the supertype must sit at the same offsets in both. Implementations that sort fields by name or hash them into a fixed table satisfy this trivially, because field access goes through a lookup rather than a fixed displacement. Implementations that lay fields out in declaration order satisfy it only when the supertype’s field order matches a prefix of the subtype’s. A language that permits reordering must therefore either sort deterministically or insert a coercion that copies the common fields into a fresh record. Copying costs one allocation and a linear pass over the common fields; it is what happens whenever a structural subtype is passed to code compiled against the supertype’s layout.

The alternative to width subtyping for this purpose — a type that names only the fields a function reads and leaves the rest abstract — is the row variable described in row polymorphism for extensible records.

Depth, and why it is not free

The depth rule says that a type constructor applied to subtypes yields a subtype: List { x: Int, y: Int } <: List { x: Int }.

Read naively, this is the same argument one level down: any element the context reads from the list is a record with at least x, so any projection succeeds. The rule is sound for constructors that only produce values to the context — lists that are read, immutable tuples, promises.

It is unsound for constructors that consume values, and the counterexample is short. Suppose mutable cells are covariant:

c : Ref { x: Int, y: Int }        -- assume Ref is covariant
d : Ref { x: Int } = c            -- accepted by the depth rule
d := { x: 0 }                     -- writes a value with no y
y = c.value.y                     -- reads a field that is not there

The assignment through d is type-correct under the supertype’s rules, but the storage is shared with c, which believes its contents always have y. The read then accesses a field that the stored value does not have. This is not a theoretical failure: Java’s arrays are covariant, so a String[] may be assigned to a variable of type Object[], and the store of an Object that is not a String into that reference is accepted statically. Java answers with a runtime check on the array’s component type, which throws ArrayStoreException for the offending store. The language specification mandates that check precisely because the static rule cannot be made sound without giving up array covariance.

The repair is to make the constructor invariant: Ref τ is a subtype of Ref σ only when τ and σ are equivalent. Then the widening in the example is rejected, and no runtime check is needed. The cost is expressiveness: a function that reads a cell of records cannot be passed a cell of records with extra fields, even though it only reads.

Contravariance in function arguments

Function types have variance in both positions, and the two directions differ. For the result, the rule is S → T <: S → U when T <: U. A function returning T can be used where a function returning U is expected, because whatever it returns is acceptable to the context. The result position is covariant.

For the argument the relation reverses: S → U <: T → U when T <: S. The function that accepts the wider argument type is the subtype, because it can be used wherever a function accepting the narrower type is expected: the context will only supply values of the narrower type, and the function accepts all of those. This is contravariance, and it is the rule that catches programmers by surprise.

The two combine into the standard rule for the function arrow: (S₁ → T₁) <: (S₂ → T₂) iff S₂ <: S₁ and T₁ <: T₂. Written as a variance annotation, the arrow has signature (−, +).

The variance lattice

Every type constructor gets one of four variances, which form a lattice under the question “does a subtype argument produce a subtype result”:

Variance	Condition on C τ <: C σ	Typical constructor
Covariant +	τ <: σ	immutable list, reader, producer
Contravariant −	σ <: τ	consumer, sink, comparator
Invariant	τ ≡ σ and nothing more	mutable cell, array, set
Bivariant	always	phantom parameter, unconstrained

Variance composes. For a constructor applied to a parameter that itself contains a parameter, the effective variance is the product of the two. In the type (α → Int) → Int — a continuation — the outer arrow is contravariant in its argument, and that argument is an arrow contravariant in α, so α appears covariantly overall. Writing ⊥ for invariance, the composition rules are sign arithmetic: +·+ = +, +·− = −, −·+ = −, −·− = +, and an occurrence reached through a nested constructor whose parameter is invariant is invariant regardless of the sign above it. A bivariant parameter, being phantom, has no occurrence in the body to compose with, so it never contributes to another parameter’s variance.

Read as sets of permitted argument pairs, the four classes are nested: invariance permits only equal types, covariance additionally permits proper subtypes, contravariance additionally permits proper supertypes, and bivariance permits everything. Covariance and contravariance overlap exactly at invariance — that is, at the equal-type pairs — and are otherwise incomparable, so the middle of the lattice is a diamond rather than a chain. Adding the empty relation, which permits nothing and corresponds to a constructor no subtype argument can satisfy, gives the full lattice: bottom is the empty relation, invariance sits above it, covariance and contravariance sit above invariance, and bivariance is the top. A constructor with no variance annotation in a language that requires one is treated as invariant, which is the conservative choice: among the three non-degenerate variances, invariance is the one whose permitted pairs are implied by each of the others, so a checker that assumes no relationship at all is never wrong.

A checker computes these annotations once per type definition and caches them. The computation is a fixed point over the definition’s structure: start every parameter at the most permissive variance, walk the body propagating each occurrence’s composed variance upward to the parameter, and meet the results at each parameter until nothing changes. Because a definition may refer to itself, the iteration repeats until the annotation stops moving; for a definition of size n the number of iterations is bounded by n, so the worst case is quadratic in the size of a single definition — which is why some languages require the programmer to write the annotation instead of inferring it.

Subtyping as a preorder, and what it costs

The subtype relation must be reflexive and transitive to be usable in a type checker. Reflexivity is free. Transitivity is not: the declarative rule that τ₁ <: τ₂ and τ₂ <: τ₃ yield τ₁ <: τ₃ is the natural specification, but an implementation that searches for intermediate types has no bound on the search. Practical algorithms avoid the search by making the rules syntax-directed: each pair of type shapes has exactly one applicable rule, and the derivation is deterministic. For records and functions that works because the rules decompose structurally. Adding a rule that requires guessing a middle type — as a subtyping rule for bounded quantification does — reintroduces the search unless the language restricts the form of bounds.

Transitivity also interacts badly with inference. A constraint α <: β where both are variables has no unique solution: any pair of types with that relation satisfies it. A solver must either pick a canonical solution, which usually means collapsing the variables to a single one, or defer the constraint until one side becomes concrete. Deferral is what most checkers do, and the practical consequence is that an inferred type can only be described by its constraints rather than named outright: it is the minimal solution in the ordering the constraints induce, and it is principal only when that minimal solution is unique.

Coercions versus erasure

Where a subtype value is used at a supertype, an implementation has two choices: represent the conversion as a no-op and rely on layout compatibility, or emit an explicit coercion.

Erasure is cheap and is what happens in a language whose records are laid out with the supertype’s fields as a prefix and whose functions share a calling convention. The runtime cost of subtyping is then zero, and the only artifact is the static proof.

Explicit coercions appear when the representations differ: a structural record passed to a nominal interface, an integer widened to a float, a function adapted to a different argument order. Each coercion is a real operation with a real cost, and a chain of them can be collapsed by the compiler only if the intermediate representations are compatible. The same distinction — representation-free conversion against an explicit runtime check — governs how generic type arguments are handled, as described in erasure and reification of generic types.

The distinction matters for diagnostics too. A language that erases subtyping has no runtime information about the static type of a value, so a failure caused by an unsound cast cannot be attributed. A language that keeps coercions can report where the conversion happened. Java’s ArrayStoreException is the documented compromise: it is thrown on a store into an array whose runtime component type does not accept the stored value, even though the static element type of the array reference does, and the cost is one comparison per store on that path.

Where structural and nominal subtyping diverge

A structural system derives subtyping from the shape of the type. A nominal system derives it from declared relationships: a class names its superclass, an interface lists its parents, a type declaration says it implements another.

Structural subtyping admits more programs. Two independently written record types with identical fields are interchangeable, which makes it natural for data interchange and for functions that accept “anything with a name field.” It also makes every field name part of a global namespace: adding a field to one type silently makes it a subtype of another, and removing a field silently breaks callers in other modules.

Nominal subtyping admits fewer programs and localizes change. Adding a field to a class does not create a relationship with another class. But it requires the declaration to be edited when a new relationship is wanted, which is impossible when the two types come from different libraries and neither can be changed. Languages that need both usually provide a structural escape hatch — an interface satisfied by shape — alongside nominal declarations, and the two relations must then be kept consistent by the checker.

Variance is independent of the declaration mechanism, because it follows from the soundness argument rather than from how the subtype relation was established. A nominal mutable collection is invariant for the same reason a structural one is: what matters is which positions the constructor reads and which it writes, not whether the relation came from a declaration or from a field list.