Lesson 6.5 — Subtyping: structural and algorithmic, variance, nominal vs structural¶

Techniques: structural subtyping with top and bottom, records (width, depth, permutation) and functions (contravariant parameters), declarative rules with subsumption vs the algorithmic system with transitivity eliminated (Cardelli 1984/1988 [Car88]; [TAPL, Ch. 15–16]), and subtyping vs coercion [BTCGS91]; variance of generic types — declaration-site (Scala, Kotlin in/out, C#) vs use-site (Java wildcards [IV02, THEAG04]) — and why mutable containers must be invariant; nominal vs structural subtyping (Java, C#, Swift classes [IPW01] vs TypeScript, Go interfaces, OCaml objects) · Pebble implements: none — Pebble's types are nominal for structs and structural for arrays, with no subtyping (pebble-spec §5); the lab's ★ milestone L4 implements the algorithm and tests it against a brute-force search of the declarative rules · Drills: subtype-query · Prerequisites: Lessons 6.1, 6.2 and 6.4 · Time: 5 hours

Subtyping says that a value of one type can be used wherever a value of another type is expected: a record with more fields where fewer are needed, a function that accepts more where one that accepts less is required, a Dog where an Animal will do. The declarative rules are short and obviously sensible, but one of them — transitivity — makes them useless as an algorithm: to show \(S <: U\) it lets you guess any intermediate \(T\). This lesson derives the algorithm that TypeScript, Scala and every structural checker run, proves it equivalent to the rules, extends subtyping to generic types (where the direction of the relation depends on how a type parameter is used), and contrasts subtyping by shape with subtyping by declared name.

1. Problem and motivation¶

Structural subtyping and algorithmic subtyping¶

The problem. A function norm(p: {x: float, y: float}) should accept a point with an extra z field; a callback of type Animal -> int should be usable where Dog -> int is expected. The principle of safe substitution says \(S <: T\) ("\(S\) is a subtype of \(T\)") when every value of type \(S\) can be safely used in every context expecting a \(T\) [TAPL, §15.1]. Cardelli gave the structural rules for records and functions to model inheritance [Car88]; the subsumption rule (\(e : S\) and \(S <: T\) imply \(e : T\)) plugs them into typing. Both the subsumption rule and the transitivity rule of subtyping are not syntax-directed, so an implementation needs an algorithmic system in which they are admissible rather than primitive [TAPL, Ch. 16]. In a bidirectional checker (Lesson 6.4) subsumption is needed in exactly one place, the mode switch. Pebble has no subtyping, so its mode switch compares with equality; the lab's L4 implements the algorithm for a calculus with records and functions.

Variance of generic types¶

The problem. Given Dog <: Animal, is List<Dog> <: List<Animal>? For a read-only list yes (covariance), for a sink that only consumes animals the reverse (contravariance), and for a mutable list neither (invariance): Lesson 6.2 showed covariant mutable arrays are unsound without a run-time check. Languages either let the designer of a type declare each parameter's variance and check the declaration (declaration-site variance: Scala +T/-T, Kotlin and C# out/in) or let the user ask for a covariant or contravariant view at each use (use-site variance: Java's ? extends T and ? super T, from Igarashi and Viroli's variant parametric types [IV02, THEAG04]). Rust infers variance from the type's fields [RUSTC-Variance].

Nominal vs structural subtyping¶

The problem. Is {value: float} meant as meters the same type as {value: float} meant as seconds? Structural type systems say yes: types are compared by shape (TypeScript, OCaml objects, Go interfaces). Nominal systems say no: a type is a name, and \(S <: T\) only if \(S\) is declared to extend \(T\) (Java, C#, Swift classes and protocols; Featherweight Java [IPW01] is the formal model). Nominal typing gives abstraction and cheap checks; structural typing gives flexibility for independently written code. Pebble's structs are nominal (two structs with the same fields are different types) and its arrays structural ([int; 3] equals [int; 3]), with no subtyping between distinct types (pebble-spec §5).

2. Definitions and algorithms¶

Structural subtyping and algorithmic subtyping¶

Definition 6.5.1 (Types with top, bottom and records)

\(\tau ::= \mathsf{int} \mid \mathsf{bool} \mid \top \mid \bot \mid \tau_1 \to \tau_2 \mid \{l_1{:}\tau_1, \dots, l_n{:}\tau_n\}\) with distinct labels; a record type is identified with the same fields in any order. \(\top\) (top, TypeScript unknown, Java Object for references) is the type of every value; \(\bot\) (bot, TypeScript never, Rust !) has no values: an expression of type \(\bot\) never returns (it throws or loops).

Definition 6.5.2 (Declarative subtyping)

\(S <: T\) is the smallest relation closed under

\[ \begin{aligned} &\dfrac{}{S <: S}\ (\textsf{S-Refl}) \qquad \dfrac{S <: U \qquad U <: T}{S <: T}\ (\textsf{S-Trans}) \qquad \dfrac{}{S <: \top}\ (\textsf{S-Top}) \qquad \dfrac{}{\bot <: T}\ (\textsf{S-Bot}) \qquad \dfrac{T_1 <: S_1 \qquad S_2 <: T_2}{S_1 \to S_2 <: T_1 \to T_2}\ (\textsf{S-Arrow}) \\[1ex] &\dfrac{}{\{l_1{:}\tau_1, \dots, l_{n+k}{:}\tau_{n+k}\} <: \{l_1{:}\tau_1, \dots, l_n{:}\tau_n\}}\ (\textsf{S-RcdWidth}) \qquad \dfrac{S_i <: T_i \ \text{for each } i}{\{l_i{:}S_i\}_{i=1}^{n} <: \{l_i{:}T_i\}_{i=1}^{n}}\ (\textsf{S-RcdDepth}) \end{aligned} \]

(S-RcdPerm, reordering fields, is built into the identification of record types.) The typing rules get the subsumption rule \(\dfrac{\Gamma \vdash e : S \qquad S <: T}{\Gamma \vdash e : T}\) (T-Sub).

Definition 6.5.3 (Algorithmic subtyping)

\(\blacktriangleright S <: T\) is defined by the rules, in which exactly one applies to any pair (checked top to bottom):

\[ \begin{aligned} &\dfrac{}{\blacktriangleright S <: \top}\ (\textsf{SA-Top}) \qquad \dfrac{}{\blacktriangleright \bot <: T}\ (\textsf{SA-Bot}) \qquad \dfrac{B \in \{\mathsf{int}, \mathsf{bool}\}}{\blacktriangleright B <: B}\ (\textsf{SA-Base}) \qquad \dfrac{\blacktriangleright T_1 <: S_1 \qquad \blacktriangleright S_2 <: T_2}{\blacktriangleright S_1 \to S_2 <: T_1 \to T_2}\ (\textsf{SA-Arrow}) \\[1ex] &\dfrac{\{l_j\}_{j=1}^{n} \subseteq \{k_i\}_{i=1}^{m} \qquad \blacktriangleright S_i <: T_j \ \text{whenever}\ k_i = l_j}{\blacktriangleright \{k_i{:}S_i\}_{i=1}^{m} <: \{l_j{:}T_j\}_{j=1}^{n}}\ (\textsf{SA-Rcd}) \end{aligned} \]

No rule applies to any other pair (for example \(\mathsf{int}\) vs \(\mathsf{bool}\), a record vs an arrow, \(\top\) vs anything but \(\top\)).

Algorithm 6.5.4 (Subtype)

Input: types \(S\) and \(T\) (Definition 6.5.1).
Output: true iff \(\blacktriangleright S <: T\).
Precondition: record labels are distinct.
Postcondition: the result equals the declarative relation (Theorem 6.5.13).
Invariant: every recursive call is on a pair of strictly smaller types (a subterm of \(S\) and a subterm of \(T\)).

function Subtype(S, T):
    if T = ⊤ or S = ⊥: return true                           # SA-Top, SA-Bot
    if S, T are both int or both bool: return true            # SA-Base
    if S = S1 → S2 and T = T1 → T2:                           # SA-Arrow
        return Subtype(T1, S1) and Subtype(S2, T2)            # parameters swap sides
    if S = {k_i : S_i} and T = {l_j : T_j}:                   # SA-Rcd
        for each field l_j : T_j of T:
            if l_j is not a label of S: return false          # width: S may have more, not fewer
            if not Subtype(S.field(l_j), T_j): return false   # depth, found by label (permutation)
        return true
    return false

The lab's isSubtype (labs/ch06-bidir/include/bidir/Subtyping.h) and the drill subtype-query implement this algorithm; the drill adds the variance rules below.

Variance of generic types¶

Definition 6.5.5 (Variance; positions)

A type constructor \(C\) with parameter \(X\) is covariant in \(X\) if \(S <: T\) implies \(C[S] <: C[T]\), contravariant if it implies \(C[T] <: C[S]\), invariant if \(C[S] <: C[T]\) requires \(S <: T\) and \(T <: S\) (for these types: \(S = T\)), and bivariant if \(X\) does not matter. The polarity of an occurrence of \(X\) in a type is \(+\) at the top, flips under a function parameter, is kept under a function result, and is multiplied by the declared variance of any constructor it appears under (\(+ \cdot - = -\), and an occurrence under an invariant constructor is in both polarities).

Definition 6.5.6 (Declaration-site and use-site variance)

Declaration-site: the declaration class C[+X] (Scala; out X in Kotlin and C#) promises covariance; the checker verifies that \(X\) occurs only in \(+\) positions of the class's members (method results, read-only fields), and dually for -X / in X (\(-\) positions: method parameters). Use-site: every generic type is invariant, and a use may write C<? extends T> (Java) — the type of all C<S> with \(S <: T\), whose members may only be used covariantly — or C<? super T>, the contravariant view. Subtyping between wildcard types is decided by containment (JLS §4.5.1): ? extends U contains ? extends T if \(T <: U\), and contains T itself (so C<T> <: C<? extends U> for every \(T <: U\)); dually, ? super T contains ? super U if \(T <: U\).

Algorithm 6.5.7 (Checking a declaration-site variance annotation)

Input: a generic class C[vX] with declared variance \(v \in \{+, -, =\}\) and its members' types.
Output: the occurrences of \(X\) whose polarity contradicts \(v\).
Precondition: the variances of every other type constructor are known.
Postcondition: no reported occurrence ⇒ subtyping C[S] <: C[T] by the declared rule is safe (Theorem 6.5.15).
Invariant: Walk(τ, p) is called with \(p\) the polarity of \(\tau\)'s position.

function CheckVariance(C, v):
    bad ← []
    for each member m of C:
        if m is a method with parameters P1..Pk and result R:
            for each Pi: Walk(Pi, −)
            Walk(R, +)
        if m is a mutable field of type F: Walk(F, +); Walk(F, −)   # read and written
        if m is a read-only field of type F: Walk(F, +)
    return bad

function Walk(τ, p):
    case τ of
        X:              if v = + and p = −, or v = − and p = +: bad.append(this occurrence)
        A → B:          Walk(A, flip(p)); Walk(B, p)
        D[τ1] with declared variance w:
                        if w = +: Walk(τ1, p)
                        if w = −: Walk(τ1, flip(p))
                        if w = =: Walk(τ1, +); Walk(τ1, −)
        otherwise:      nothing

The drill's types use List[+T], Sink[-T] and Cell[T] (invariant), and Algorithm 6.5.4 gains one rule per constructor: List[S] <: List[T] if \(S <: T\); Sink[S] <: Sink[T] if \(T <: S\); Cell[S] <: Cell[T] if both.

Nominal vs structural subtyping¶

Definition 6.5.8 (Nominal subtyping)

A class table \(\mathit{CT}\) maps class names to declarations class C extends D { fields; methods }, with Object as the root. Nominal subtyping \(C <:_{N} D\) is the reflexive-transitive closure of the declared extends (and implements) edges [IPW01, §2]. Two classes with identical members but no declared relation are unrelated. Structural subtyping (Definition 6.5.2) compares members instead of names.

Algorithm 6.5.9 (Nominal subtype test by walking the supertype chain)

Input: a class table, class names \(C\) and \(D\).
Output: true iff \(C <:_{N} D\).
Precondition: the extends relation is acyclic (checked when classes are declared).
Postcondition: the result is the closure of Definition 6.5.8.
Invariant: c is always a supertype of \(C\).

function NominalSubtype(C, D):
    c ← C
    loop:
        if c = D: return true
        if c = Object: return false
        c ← superclass(c)             # interfaces: search all declared supertypes breadth-first

3. Worked examples¶

Structural subtyping and algorithmic subtyping¶

Algorithm 6.5.4 on \(S = \{a{:}\mathsf{int},\ f{:}\{x{:}\mathsf{int}\} \to \mathsf{int}\}\) and \(T = \{f{:}\{x{:}\mathsf{int}, y{:}\mathsf{bool}\} \to \top\}\) (the drill's format; indentation = depth):

call	pair	rule	result
1	`{a: int, f: {x: int} -> int} <: {f: {x: int, y: bool} -> top}`	SA-Rcd: T's only label `f` is in S	yes
2	· `{x: int} -> int <: {x: int, y: bool} -> top`	SA-Arrow	yes
3	· · `{x: int, y: bool} <: {x: int}` (parameters swapped)	SA-Rcd: width	yes
4	· · · `int <: int`	SA-Base	yes
5	· · `int <: top`	SA-Top	yes

Width appears twice, in opposite directions: at call 1 \(S\) may have the extra field a; at call 3 the expected parameter may have the extra field y, because the parameters were swapped. A function that needs only x can accept records that also have y.
The same judgment derived declaratively needs S-Trans: e.g. \(S <: \{f{:}\{x{:}\mathsf{int}\} \to \mathsf{int}\}\) by width, then that \(<: T\) by depth with S-Arrow. The algorithm fuses width, depth and permutation into SA-Rcd, so no intermediate type is ever guessed.

Try it

./course drill subtype-query --seed 5 --difficulty medium --solution prints one table like this per query.

Variance of generic types¶

Algorithm 6.5.7 on class Box[+X] { get(): X; set(v: X): unit; map(f: X -> int): Box[int] }:

member	occurrence	polarity computation	polarity	verdict for `+X`
`get(): X`	result	result: \(+\)	\(+\)	ok
`set(v: X)`	parameter	parameter: flip \(+\) → \(-\)	\(-\)	error: a covariant `X` cannot be consumed
`map(f: X -> int)`	inside a parameter of a parameter	parameter: \(-\); parameter of the function type: flip → \(+\)	\(+\)	ok

map shows why polarity is multiplicative: X is an argument to a callback that Box supplies, so Box produces values of X there. Removing set makes Box safely covariant — the read-only-container case.

Nominal vs structural subtyping¶

With class Meters { value: float } and class Seconds { value: float }, both extending Object: NominalSubtype(Seconds, Meters) walks Seconds → Object without meeting Meters and returns false (javac rejects speed(s, m) in the box of §7); structurally, {value: float} <: {value: float} by SA-Rcd (TypeScript accepts it). Adding a phantom field of a unique literal type ("branding") makes the shapes differ, which is how TypeScript programmers simulate nominal types.

4. Invariants and correctness¶

Structural subtyping and algorithmic subtyping¶

Lemma 6.5.10 (Reflexivity is admissible in the algorithmic system)

\(\blacktriangleright T <: T\) for every type \(T\).

Proof

By induction on \(T\). \(\top\): SA-Top. \(\bot\): SA-Bot. Base types: SA-Base. \(T_1 \to T_2\): by the hypothesis \(\blacktriangleright T_1 <: T_1\) and \(\blacktriangleright T_2 <: T_2\), so SA-Arrow. Records: the label sets are equal (so included) and each field is related to itself by the hypothesis, so SA-Rcd.

Lemma 6.5.11 (Transitivity is admissible in the algorithmic system)

If \(\blacktriangleright S <: U\) and \(\blacktriangleright U <: T\) then \(\blacktriangleright S <: T\).

Proof

By induction on the sum of the sizes of the two derivations \(D_1\) of \(\blacktriangleright S <: U\) and \(D_2\) of \(\blacktriangleright U <: T\), with a case on their last rules.

If \(D_2\) is SA-Top, then \(T = \top\) and SA-Top concludes. If \(D_1\) is SA-Bot, then \(S = \bot\) and SA-Bot concludes.
Otherwise \(T \neq \top\) and \(S \neq \bot\). Then \(U \neq \top\): the only rule concluding \(\blacktriangleright \top <: T\) is SA-Top, which needs \(T = \top\). And \(U \neq \bot\): the only rule concluding \(\blacktriangleright S <: \bot\) is SA-Bot, which needs \(S = \bot\). So \(U\) is a base type, an arrow or a record, and both derivations end with the structural rule for \(U\)'s shape; \(S\) and \(T\) have that shape too.
SA-Base twice: \(S = U = T\), and SA-Base concludes.
SA-Arrow twice: \(S = S_1 \to S_2\), \(U = U_1 \to U_2\), \(T = T_1 \to T_2\) with subderivations \(\blacktriangleright U_1 <: S_1\), \(\blacktriangleright S_2 <: U_2\), \(\blacktriangleright T_1 <: U_1\) and \(\blacktriangleright U_2 <: T_2\). The induction hypothesis on the pairs \((T_1 <: U_1, U_1 <: S_1)\) and \((S_2 <: U_2, U_2 <: T_2)\) gives \(\blacktriangleright T_1 <: S_1\) and \(\blacktriangleright S_2 <: T_2\), and SA-Arrow concludes.
SA-Rcd twice: \(T\)'s labels are among \(U\)'s, which are among \(S\)'s. For each label \(l\) of \(T\), \(\blacktriangleright S.l <: U.l\) and \(\blacktriangleright U.l <: T.l\) are subderivations, and the hypothesis gives \(\blacktriangleright S.l <: T.l\); SA-Rcd concludes.

Theorem 6.5.12 (The algorithm terminates)

Algorithm 6.5.4 terminates on every pair \((S, T)\) after at most \(\min(\lvert S \rvert, \lvert T \rvert)\) calls, where \(\lvert \cdot \rvert\) counts type nodes.

Proof

Each recursive call is on a pair \((S', T')\) of immediate subterms, one of \(S\) and one of \(T\), in either order (parameters swap), so \(\lvert S' \rvert + \lvert T' \rvert < \lvert S \rvert + \lvert T \rvert\): the recursion is well founded. The recursion descends both types in lockstep: an arrow's parameter is paired with the other arrow's parameter and its result with the other's result, and a field of \(T\) with the field of \(S\) that has the same label. So each call corresponds to one path from the root of \(T\), and different calls to different paths (labels are distinct); the same holds for \(S\). Hence the calls are at most the nodes of \(T\) and at most the nodes of \(S\).

Theorem 6.5.13 (Soundness and completeness of algorithmic subtyping)

\(\blacktriangleright S <: T\) iff \(S <: T\) (Definition 6.5.2).

Proof

Soundness (⇒), by induction on the algorithmic derivation: SA-Top, SA-Bot are S-Top, S-Bot; SA-Base is S-Refl; SA-Arrow is S-Arrow applied to the hypotheses; SA-Rcd is S-RcdDepth (on the fields of \(T\), using the hypotheses) composed by S-Trans with S-RcdWidth (dropping \(S\)'s extra fields), with permutation built in. Completeness (⇐), by induction on the declarative derivation: S-Refl by Lemma 6.5.10; S-Trans by the hypotheses and Lemma 6.5.11; S-Top, S-Bot by SA-Top, SA-Bot; S-Arrow by SA-Arrow on the hypotheses; S-RcdWidth by SA-Rcd with Lemma 6.5.10 on each kept field; S-RcdDepth by SA-Rcd on the hypotheses. [TAPL, §16.1] gives the same proof for its system.

The lab's L4_AgreesWithTheDeclarativeRulesOnAllSmallTypes test checks Theorem 6.5.13 by brute force: it computes the declarative relation as the least fixed point of Definition 6.5.2's rules over the 2 705 types of at most 5 nodes (labels a, b), and compares it with the learner's isSubtype on all 180 625 pairs of types of at most 4 nodes (10 061 of which are subtypes); the Python oracle of the drill passes the same test with generic types added.

What breaks the argument. With a subsumption rule in typing, Theorem 6.5.13 is not enough: the typing rules themselves must be made algorithmic (subsumption only at the mode switch, Lesson 6.4, or at applications, [TAPL, §16.2]). With recursive types, the induction in Theorem 6.5.12 fails (types are infinite), and the algorithm needs a cache of assumed pairs (Amadio–Cardelli).

Variance of generic types¶

Lemma 6.5.14 (Polarity composition)

If \(X\) occurs at polarity \(p\) in \(\tau[X]\) (Definition 6.5.5) and only there, then \(S <: T\) implies \(\tau[S] <: \tau[T]\) when \(p = +\) and \(\tau[T] <: \tau[S]\) when \(p = -\).

Proof

By induction on the position. At the top (\(p = +\)) the claim is \(S <: T\). Under a function result, S-Arrow is covariant in the result and preserves the polarity. Under a function parameter, S-Arrow is contravariant and flips it. Under a constructor declared \(+\) or \(-\), its subtyping rule preserves or flips the direction; under an invariant constructor there is no rule for \(S \ne T\), which is why the definition assigns both polarities (the claim is then only about \(S = T\)).

Theorem 6.5.15 (Checked declaration-site variance is safe)

If Algorithm 6.5.7 reports nothing for class C[+X], then for every \(S <: T\) and every value \(c : C[S]\), every member access on \(c\) typed at \(C[T]\) is also well typed at \(C[S]\) with a subtype of the result: using \(c\) as a \(C[T]\) is safe. Dually for -X.

Proof

A member access at \(C[T]\) either calls a method with arguments of types \(P_i[T]\) and result \(R[T]\), or reads a field of type \(F[T]\). Algorithm 6.5.7 guarantees that \(X\) occurs in \(P_i\) only at polarity \(-\) and in \(R\) and \(F\) only at \(+\) (counting nested occurrences with the multiplication of Definition 6.5.5). By Lemma 6.5.14 with \(S <: T\): \(P_i[T] <: P_i[S]\) (arguments acceptable at \(T\) are acceptable at \(S\)), and \(R[S] <: R[T]\), \(F[S] <: F[T]\) (results obtained at \(S\) can be used at \(T\)). So the access type-checks against \(c\)'s real type \(C[S]\) and, by subsumption, returns something usable at \(T\). A mutable field would put \(X\) at both polarities and be rejected, which is the covariant-array problem of Proposition 6.2.11 caught statically.

Nominal vs structural subtyping¶

Proposition 6.5.16 (Nominal subtyping is decided by Algorithm 6.5.9 and implies structural compatibility)

Algorithm 6.5.9 returns true iff \(C <:_{N} D\). In a class table where a subclass inherits every field and method of its superclass (with the same or, for method results, more specific types), \(C <:_{N} D\) implies that \(C\)'s member signature is a structural subtype of \(D\)'s; the converse fails.

Proof

Algorithm: by acyclicity the chain \(C, \mathrm{super}(C), \dots\) reaches Object in finitely many steps, and the loop visits exactly the classes \(c\) with \(C <:_{N} c\) along the single-inheritance chain (induction on the number of steps; interfaces add a breadth-first search over a finite DAG). Implication: by induction on the length of the extends chain: each step keeps every inherited member (width) with the same or covariantly refined types (depth), so the member record of \(C\) is a structural subtype of \(D\)'s by Theorem 6.5.13. Converse fails: Meters and Seconds of §3 have equal member signatures but no extends edge.

5. Complexity¶

Technique	Time (worst)	Time (typical)	Space	Variables
Algorithmic subtyping (Algorithm 6.5.4)	\(\min(\lvert S \rvert, \lvert T \rvert)\) calls; \(O(\lvert S \rvert \cdot \lvert T \rvert)\) time with list-searched labels, \(O(\lvert S \rvert + \lvert T \rvert)\) with hashed labels	small: types are shallow	\(O(\text{depth})\)	\(\lvert S \rvert, \lvert T \rvert\) type sizes (nodes)
Declarative search (with S-Trans)	not an algorithm: unboundedly many intermediates; bounded brute force \(\Theta(U^3)\) per fixed-point round	60 s in Python, 4 s in C++ for \(U = 2\,705\)	\(\Theta(U^2)\)	\(U\) types in the universe
Variance checking (Algorithm 6.5.7)	\(O(\lvert \text{declaration} \rvert)\)	linear	\(O(\text{depth})\)	—
Nominal test (Algorithm 6.5.9)	\(O(h)\) per query	\(O(1)\) with a display (HotSpot)	\(O(1)\)	\(h\) hierarchy depth

Justification. Theorem 6.5.12 bounds the calls of Algorithm 6.5.4; each SA-Rcd step looks up \(T\)'s labels in \(S\), \(O(\lvert S \rvert)\) per label by scanning (so \(O(\lvert S \rvert \cdot \lvert T \rvert)\) over the run) or \(O(1)\) by hashing. The declarative brute force (the lab and drill tests) iterates one-step rules and a Warshall closure, \(\Theta(U^3)\) per round, until no pair is added. Algorithm 6.5.7 walks each member type once. Algorithm 6.5.9 walks at most \(h\) superclasses; HotSpot answers most subtype checks in constant time by storing each class's primary superclasses at fixed depths (a display) and checking one slot [CR02].

Pathological families. Records of records: \(S_k = \{a{:}S_{k-1}, b{:}S_{k-1}\}\) has size \(\Theta(2^k)\), and checking \(S_k <: S_k\) visits all of it — linear in the (exponential) size; with hash-consing, a cache of already-proven pairs makes it \(O(k)\). For nominal subtyping with variance, the combination of variance, generics and "expansive" inheritance makes subtyping undecidable: Java's wildcards can encode Turing machines [Gri17].

Scale. TypeScript relates large structural types constantly (every object literal, every union); its checker caches relation results per pair of type ids in isTypeRelatedTo [TSC-Checker] for exactly the reason above.

Structural subtyping and algorithmic subtyping¶

Subtyping vs coercion [BTCGS91]: interpret \(S <: T\) as a coercion function (dropping fields = building a smaller record) instead of the identity. Coercive subtyping allows int <: float with a real conversion, at the price of a coherence proof (Lesson 6.3, Definition 6.3.5) and run-time copies; inclusive (identity) subtyping needs records whose layout supports width subtyping (offset tables, dictionaries).
Joins and meets [TAPL, §16.3]: the type of if c then e1 else e2 is the least upper bound of the branch types; records have joins (common fields, joined) and arrows have joins using meets of parameters, requiring a meet that may not exist without \(\bot\).
Recursive and equi-recursive types (Amadio–Cardelli 1993): subtyping by coinduction with an assumption set; the algorithm is quadratic with memoization.
Excess-property checks (TypeScript): a fresh object literal is checked without width subtyping, catching misspelled optional fields — a deliberate exception shown in the box.

Variance of generic types¶

Variance inference (Rust [RUSTC-Variance], TypeScript's variance measurement for type aliases): compute each parameter's variance from its uses by a fixed point over the declarations; no annotations, less control.
Use-site variance with capture (Java): List<? extends Number> is opened to List<CAP#1> with a fresh CAP#1 <: Number at each use; flexible for library users, notoriously hard error messages (the box's CAP#1).
Method parameter bivariance (TypeScript's method syntax, Eiffel's covariant parameters): unsound on purpose for ergonomics; strictFunctionTypes restores contravariance for function-typed properties only.

Nominal vs structural subtyping¶

Branding / newtypes (TypeScript intersections with a unique tag, Haskell and Rust newtypes): nominal distinctions inside a structural system, at zero run-time cost.
Structural interfaces over nominal classes (Go interfaces, Scala structural types, TypeScript's classes compared structurally): values are nominally typed, interfaces satisfied by shape; Go checks satisfaction statically and builds method tables (itabs) lazily at run time.
Nominal with declared variance and wildcards (Java, C#): decidability depends on restricting inheritance patterns [Gri17].

7. In real compilers¶

Structural subtyping and algorithmic subtyping¶

TypeScript's isTypeRelatedTo and structuredTypeRelatedTo in src/compiler/checker.ts [TSC-Checker] implement Algorithm 6.5.4 for object types, with the strictFunctionTypes switch deciding whether function-typed properties are compared contravariantly or bivariantly.

Width, depth, contravariance, top and bottom in tsc 5.9

Reproduce (tsc 5.9.3 via npx):

mkdir -p ts && cat > ts/structural.ts <<'EOF'
type Point = { x: number };
type Point3 = { x: number; y: number; z: number };
const p3: Point3 = { x: 1, y: 2, z: 3 };
const p: Point = p3;                                  // width: extra fields are fine
const q: Point = { x: 1, y: 2 };                      // excess-property check on a fresh literal
type Deep = { pos: { x: number } };
const d: Deep = { pos: p3 };                          // depth
let takesPoint = (a: Point) => a.x;
let takesPoint3 = (a: Point3) => a.z;
takesPoint3 = takesPoint;                             // parameter contravariance: accepted
takesPoint = takesPoint3;                             // rejected with strictFunctionTypes
interface Handler { handle(a: Point): number }       // method syntax: bivariant parameters
const h: Handler = { handle: (a: Point3) => a.z };    // accepted even under --strict
const anything: unknown = p3;                           // unknown is the top type
function fail(): never { throw new Error("no"); }     // never is the bottom type
const n: number = fail();
EOF
npx -y -p typescript@5.9 tsc --strict --noEmit ts/structural.ts

Output (complete):

ts/structural.ts(5,26): error TS2353: Object literal may only specify known properties, and 'y' does not exist in type 'Point'.
ts/structural.ts(11,1): error TS2322: Type '(a: Point3) => number' is not assignable to type '(a: Point) => number'.
  Types of parameters 'a' and 'a' are incompatible.
    Type 'Point' is missing the following properties from type 'Point3': y, z

What to notice: lines 4 and 7 are width and depth (SA-Rcd). Line 10 is SA-Arrow with the parameters swapped (Point3 <: Point), and line 11 fails on exactly that swapped premise ("Types of parameters 'a' and 'a' are incompatible"). Line 13 is accepted although it is the same shape as line 11: method parameters are bivariant, an intentional unsoundness (Lesson 6.2). Lines 14 and 16 use unknown as \(\top\) and never as \(\bot\) (S-Top, S-Bot). Line 5 is not a subtyping failure but TypeScript's excess-property check on a fresh literal (§6).

Variance of generic types¶

javac decides wildcard containment in Types.containsType [JAVAC-Types]; rustc infers variance in variances_of [RUSTC-Variance]; Kotlin checks declaration-site in/out annotations with the polarity rules of Algorithm 6.5.7, reporting a covariant type parameter in an in position [KOTLIN-Generics] (Kotlin's compiler is not runnable in this container).

Use-site variance in javac 21: invariance, ? extends and ? super

Reproduce (javac 21.0.10):

mkdir -p java && cat > java/Variance.java <<'EOF'
import java.util.ArrayList;
import java.util.List;

class Variance {
    static double sum(List<? extends Number> xs) {        // use-site covariance: read only
        double s = 0;
        for (Number x : xs) s += x.doubleValue();
        return s;
    }
    static void fill(List<? super Integer> out) {          // use-site contravariance: write only
        out.add(42);
    }
    static void run() {
        List<Integer> ints = new ArrayList<>();
        List<Number> nums = ints;                          // generics are invariant
        List<? extends Number> ro = ints;                  // fine
        ro.add(1);                                         // cannot add to ? extends
        fill(new ArrayList<Object>());                     // Object is a supertype of Integer
        double s = sum(ints);
    }
}
EOF
javac -d java java/Variance.java

Output (complete; the container's Picked up JAVA_TOOL_OPTIONS banner removed):

java/Variance.java:15: error: incompatible types: List<Integer> cannot be converted to List<Number>
        List<Number> nums = ints;                          // generics are invariant
                            ^
java/Variance.java:17: error: incompatible types: int cannot be converted to CAP#1
        ro.add(1);                                         // cannot add to ? extends
               ^
  where CAP#1 is a fresh type-variable:
    CAP#1 extends Number from capture of ? extends Number
Note: Some messages have been simplified; recompile with -Xdiags:verbose to get full output
2 errors

What to notice: List is invariant (line 15): List<Integer> <: List<Number> would allow the unsound store of Proposition 6.2.11, and erased generics cannot check it at run time (Lesson 6.9). ? extends Number is the covariant view: reading gives Number (line 7) but adding fails, because the element type is an unknown CAP#1 <: Number — the set(v: X) error of §3's variance check, found at the use instead of the declaration. ? super Integer is the contravariant view that accepts Integers (line 11) and an ArrayList<Object> (line 18).

Nominal vs structural subtyping¶

javac's Types.isSubtype walks declared supertypes (Algorithm 6.5.9 plus generics); the JVM repeats the test at run time for casts and array stores with HotSpot's fast display-based check [CR02]. TypeScript compares classes structurally, with private members as the one nominal exception.

Same shape, different names: javac 21 vs tsc 5.9, and branding

Reproduce (javac 21.0.10, tsc 5.9.3 via npx):

mkdir -p java ts && cat > java/Nominal.java <<'EOF'
class Nominal {
    record Meters(double value) {}
    record Seconds(double value) {}
    static double speed(Meters m, Seconds s) { return m.value() / s.value(); }
    static void run() {
        Meters m = new Meters(100);
        Seconds s = new Seconds(9.58);
        speed(s, m);                        // same shape, different names: rejected
    }
}
EOF
javac -d java java/Nominal.java
cat > ts/nominal.ts <<'EOF'
type Meters = { value: number };
type Seconds = { value: number };
function speed(m: Meters, s: Seconds): number { return m.value / s.value; }
const m: Meters = { value: 100 };
const s: Seconds = { value: 9.58 };
console.log(speed(s, m));                 // same shape: accepted, and wrong
type Brand<T, B extends string> = T & { readonly __brand: B };
type SafeMeters = Brand<number, "m">;
type SafeSeconds = Brand<number, "s">;
function safeSpeed(m: SafeMeters, s: SafeSeconds): number { return m / s; }
safeSpeed(9.58 as SafeSeconds, 100 as SafeMeters);   // branding simulates nominal types
EOF
npx -y -p typescript@5.9 tsc --strict --noEmit ts/nominal.ts

Output (complete; the container's Picked up JAVA_TOOL_OPTIONS banner removed):

java/Nominal.java:8: error: incompatible types: Seconds cannot be converted to Meters
        speed(s, m);                        // same shape, different names: rejected
              ^
Note: Some messages have been simplified; recompile with -Xdiags:verbose to get full output
1 error
ts/nominal.ts(11,11): error TS2345: Argument of type 'SafeSeconds' is not assignable to parameter of type 'SafeMeters'.
  Type 'SafeSeconds' is not assignable to type '{ readonly __brand: "m"; }'.
    Types of property '__brand' are incompatible.
      Type '"s"' is not assignable to type '"m"'.

What to notice: Java's records are nominal (Algorithm 6.5.9 finds no path from Seconds to Meters); TypeScript accepts the swapped call on line 6 because the shapes are equal (SA-Rcd), and rejects the branded version only because the phantom __brand fields now differ — a structural check that simulates a nominal one.

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Structural subtyping (algorithmic)	Width, depth, permutation, contravariant parameters, top and bottom; equals the declarative rules (Theorem 6.5.13)	\(O(\lvert S \rvert + \lvert T \rvert)\) with hashed labels · cached per type pair in practice	Explains the failing path ("types of parameters … are incompatible")	Low for the algorithm; joins/meets and recursion add effort	TypeScript, OCaml objects, Go interfaces, Scala structural types, the lab's L4
Variance of generics	Covariance for producers, contravariance for consumers, invariance for mutable containers (Theorem 6.5.15)	Linear declaration check; wildcard subtyping undecidable in general [Gri17]	Declaration-site: errors at the declaration; use-site: at each use, with capture variables	Medium (declaration-site), high (use-site with capture)	Scala, Kotlin, C# (declaration-site); Java (use-site); Rust (inferred)
Nominal subtyping	Only declared relations; abstraction boundaries enforced (Proposition 6.5.16)	\(O(h)\), \(O(1)\) with displays at run time	"X cannot be converted to Y" names both types	Low	Java, C#, Swift, C++, Kotlin, Rust traits (nominal impls)
Structural typing (whole types)	Any matching shape is accepted; unrelated code interoperates	As algorithmic subtyping	Accepts accidental matches (meters for seconds)	Low; branding for nominal needs	TypeScript, Go interfaces, OCaml, Elm records

Choose structural subtyping where independently written code must interoperate by shape (JavaScript objects, configuration records, interfaces); choose nominal where types carry meaning beyond their shape (units, invariants, abstraction). Choose declaration-site variance when library authors can annotate their types once (Kotlin, Scala, C#); use-site variance only when retrofitting generics onto an invariant language, as Java did.

9. Assessment¶

Technique	Quiz ids	Drill	Flashcard tag	Exercises
Structural subtyping (algorithmic)	`subtype-queries`, `transitivity-elimination`	`subtype-query` (easy, medium)	`subtyping`	Lab L4 ★
Variance of generics	`variance-positions`, `java-wildcards`	`subtype-query` (hard: `List`, `Sink`, `Cell`)	`variance`	—
Nominal vs structural	`nominal-structural`, `hotspot-display`	`subtype-query` (records are structural; the drill states it)	`nominal-structural`	— (Pebble's structs are nominal: E3 tests `P` vs `Q` with equal fields implicitly through E0401)

References¶

See the chapter references.

Lesson 6.5 — Subtyping: structural and algorithmic, variance, nominal vs structural¶

1. Problem and motivation¶

Structural subtyping and algorithmic subtyping¶

Variance of generic types¶

Nominal vs structural subtyping¶

2. Definitions and algorithms¶

Structural subtyping and algorithmic subtyping¶

Variance of generic types¶

Nominal vs structural subtyping¶

3. Worked examples¶

Structural subtyping and algorithmic subtyping¶

Variance of generic types¶

Nominal vs structural subtyping¶

4. Invariants and correctness¶

Structural subtyping and algorithmic subtyping¶

Variance of generic types¶

Nominal vs structural subtyping¶

5. Complexity¶

6. Variants and refinements¶

Structural subtyping and algorithmic subtyping¶

Variance of generic types¶

Nominal vs structural subtyping¶

7. In real compilers¶

Structural subtyping and algorithmic subtyping¶

Variance of generic types¶

Nominal vs structural subtyping¶

8. Comparison¶

9. Assessment¶

References¶