Subtyping
In the simply typed lambda calculus a function of type
\mathsf{Number} \to \mathsf{Number} demands an argument of
exactly type \mathsf{Number} — no more, no less. But that is
needlessly strict. If some value is a \mathsf{Nat} (a natural number), and
every \mathsf{Nat} is a \mathsf{Number},
then surely it is safe to hand it to a function expecting a
\mathsf{Number}. Subtyping is the type-system feature that
makes that intuition precise and formal: a relation S <: T, read
"S is a subtype of T", meaning
every value of type S may safely be used wherever a value of type
T is expected.
This is the principle of safe substitution (the type-theoretic heart of what
object-oriented programmers call the Liskov Substitution Principle). Subtyping is not about how values
are represented in memory, nor about inheritance hierarchies drawn in a UML tool — it is a
purely behavioural promise about interchangeability, and the type checker's job is to enforce it. Get
the promise wrong and a program that type-checks will still crash; get the variance of functions,
records and arrays right and you have one of the most useful — and most subtly dangerous — features in
all of language design.
One rule connects subtyping to typing: subsumption
The whole point of the relation S <: T is captured by a single new typing
rule bolted onto the calculus. It says: if a term has type S, and
S is a subtype of T, then that same term also has
type T.
\dfrac{\Gamma \vdash t : S \qquad S <: T}{\Gamma \vdash t : T}\;\;(\textsc{T-Sub})
This rule — subsumption — is what lets a \mathsf{Nat} flow
into a \mathsf{Number} slot. It also means typing is no longer syntax-directed
(a term now has many types, all the supertypes of its most precise one), which is exactly the
complication algorithmic subtyping has to undo. Subtyping is otherwise defined by its own set of
inference rules, and two of them make it a preorder:
\dfrac{}{\;S <: S\;}\;(\textsc{S-Refl}) \qquad\qquad
\dfrac{S <: U \qquad U <: T}{S <: T}\;(\textsc{S-Trans})
Reflexivity — every type is a subtype of itself (substituting like for like is always
safe). Transitivity — subtyping chains, so if
\mathsf{Nat} <: \mathsf{Int} and
\mathsf{Int} <: \mathsf{Number} then
\mathsf{Nat} <: \mathsf{Number}. Together they turn the set of types into a
partial order (up to the mutual-subtype equivalence S <: T
and T <: S) — a structure we can draw.
The subtype order is a poset — draw it as a Hasse diagram
Because subtyping is reflexive and transitive, the types form a partially ordered set.
We can picture it as a Hasse diagram: draw a type below another when it is a subtype,
and connect only the covering edges (transitivity fills in the rest). An arrow read upward is
"<:". Reveal the lattice level by level.
At the very top sits \mathsf{Top} (written
\top) — the supertype of everything, the type that promises
nothing, analogous to Object or any's safe cousin unknown. At
the very bottom sits \mathsf{Bot} (\bot) — the
subtype of everything, inhabited by no value at all, the type of an expression that never
returns (a thrown exception, an infinite loop). They are the top and bottom of the order:
\dfrac{}{\;S <: \mathsf{Top}\;}\;(\textsc{S-Top}) \qquad\qquad
\dfrac{}{\;\mathsf{Bot} <: S\;}\;(\textsc{S-Bot})
\mathsf{Bot} is genuinely useful: a function
fail(): Bot that only ever throws can be dropped into any context, because
\mathsf{Bot} <: T for every T. TypeScript spells
it never; Scala spells it Nothing.
Function subtyping: contravariant in, covariant out
The deepest — and most error-prone — rule is the one for function types. When is
S_1 \to S_2 <: T_1 \to T_2? That is: when can a function of the first type be
used safely wherever a function of the second is expected? Ask what "used safely" requires. A caller
who thinks they hold a T_1 \to T_2 will feed in a
T_1 and expect a T_2 back.
\dfrac{T_1 <: S_1 \qquad S_2 <: T_2}{\;S_1 \to S_2 \;<:\; T_1 \to T_2\;}\;(\textsc{S-Arrow})
-
Result: covariant (S_2 <: T_2, same direction). The
function actually returns an S_2; the caller expects a
T_2. That is safe precisely when
S_2 <: T_2 — returning something more specific than promised is
always fine.
-
Argument: contravariant (T_1 <: S_1,
reversed). The caller passes a T_1; the function is prepared to
handle any S_1. That is safe precisely when
T_1 <: S_1 — accepting a more general argument than demanded is
always fine. A function that accepts any \mathsf{Number} can stand in for
one that was only asked to accept \mathsf{Nat}s.
The slogan: be liberal in what you accept, conservative in what you return. Flip
either direction and the type system becomes unsound. This is the classic exam question, and the source
of Java's and Eiffel's famous array holes.
A subtype checker you can run
Subtyping is decidable and the algorithm is short. We model types as a discriminated union — primitives
(with a small built-in hierarchy \mathsf{Nat} <: \mathsf{Int} <: \mathsf{Number}),
function types, plus \mathsf{Top} and
\mathsf{Bot} — and translate the inference rules directly into a recursive
subtype(s, t). Watch the argument flip in the function case.
type Ty =
| { kind: "top" }
| { kind: "bot" }
| { kind: "prim"; name: string } // Nat | Int | Number | Bool
| { kind: "fun"; arg: Ty; res: Ty };
// A tiny primitive hierarchy: each maps to the list of its supertypes (self included).
const supers: Record<string, string[]> = {
Nat: ["Nat", "Int", "Number"],
Int: ["Int", "Number"],
Number: ["Number"],
Bool: ["Bool"],
};
const primSub = (s: string, t: string): boolean => (supers[s] ?? [s]).includes(t);
// The subtype relation S <: T, straight from the inference rules.
function subtype(s: Ty, t: Ty): boolean {
if (t.kind === "top") return true; // S-Top : everything <: Top
if (s.kind === "bot") return true; // S-Bot : Bot <: everything
if (s.kind === "prim" && t.kind === "prim") return primSub(s.name, t.name);
if (s.kind === "fun" && t.kind === "fun") {
// S-Arrow: contravariant argument, covariant result.
return subtype(t.arg, s.arg) && subtype(s.res, t.res);
}
return t.kind === "bot" ? s.kind === "bot" : s.kind === t.kind; // Top<:Top, Bot<:Bot
}
// Pretty-printer and convenience constructors.
const prim = (name: string): Ty => ({ kind: "prim", name });
const fn = (arg: Ty, res: Ty): Ty => ({ kind: "fun", arg, res });
const TOP: Ty = { kind: "top" }, BOT: Ty = { kind: "bot" };
const show = (t: Ty): string =>
t.kind === "top" ? "Top" : t.kind === "bot" ? "Bot"
: t.kind === "prim" ? t.name : `(${show(t.arg)} -> ${show(t.res)})`;
const check = (s: Ty, t: Ty) =>
console.log(`${show(s).padEnd(24)} <: ${show(t).padEnd(24)} = ${subtype(s, t)}`);
check(prim("Nat"), prim("Number")); // true (Nat <: Int <: Number)
check(prim("Number"), prim("Nat")); // false (wrong direction)
check(fn(prim("Number"), prim("Nat")), fn(prim("Nat"), prim("Number")));
// ^ accepts more (Number>=Nat), returns less (Nat<=Number): a valid subtype = true
check(fn(prim("Nat"), prim("Number")), fn(prim("Number"), prim("Nat")));
// ^ argument variance is backwards = false
check(BOT, fn(prim("Int"), prim("Bool"))); // true (Bot <: anything)
check(prim("Bool"), TOP); // true (anything <: Top)
The third and fourth calls are the payoff: swapping the two function types flips the answer, because the
argument position is contravariant. A function that takes a \mathsf{Number}
and returns a \mathsf{Nat} is a perfectly good stand-in for one that takes a
\mathsf{Nat} and returns a \mathsf{Number} — but
never the reverse.
\mathsf{Bot} (TypeScript's never) is the identity element of
union types and the unit that makes exhaustiveness checking work. Because
\mathsf{Bot} <: T for every T, a value of type
never is assignable everywhere — so if, after narrowing a switch over a union,
the compiler proves the remaining type is never, it knows you have handled every case. Add
a new variant and the "impossible" branch suddenly has a non-never type, and the assignment
const _exhaustive: never = x fails to compile. You get a compile-time reminder to handle
the new case — the bottom type doing real engineering work.
Java and C# let you write Number[] a = new Integer[3]; — they treat arrays as
covariant: \mathsf{Integer}[] <: \mathsf{Number}[] because
\mathsf{Integer} <: \mathsf{Number}. It reads reasonably, and for reading
it is sound. But an array is not read-only. The very next line, a[0] = 3.14;, type-checks —
the compiler thinks a is a Number[] and 3.14 is a
\mathsf{Number} — yet it tries to store a floating-point value into an
Integer[]. Java plugs the leak with a run-time ArrayStoreException;
the static type system alone is unsound here. The lesson from
\textsc{S-Arrow}: a mutable cell is like a function you can both call
(read, covariant) and be called by (write, contravariant), so it is safe only when
invariant — subtyping in neither direction. Read-only structures may be covariant;
write-only ones contravariant; read-write ones must be invariant.