Subtyping: What `Dog <: Animal` Licenses

The entire content of subtyping in a type system is the subsumption rule. It says: if you can show an expression has type S, and S is a subtype of T, then you may also treat that expression as a T.

Read the rule and then notice the thing that makes it expensive. It has no expression form in its conclusion. Γ ⊢ e : T matches *any* e. Every other rule in [[typing-rules]] is keyed to a syntactic shape — an addition, an application, a conditional — and can therefore be selected by looking at the node. This one cannot. A checker implementing the rules literally would have to consider applying subsumption at every node, in every possible way, which is search rather than checking.

That is why adding subtyping is not an incremental change to a checker. It forces a redesign into an *algorithmic* rule set where subsumption is permitted only at specific positions — argument passing, assignment, return, and the branches of a conditional — with a theorem that the restricted system accepts the same programs. It is also the single reason [[hindley-milner]] cannot absorb subtyping: unification solves equalities, and subsumption turns every equality into an inequality.

Liskov’s substitution principle is usually quoted as a design maxim and is more useful read as two separate claims: one syntactic, which a compiler enforces, and one behavioural, which it does not.

The syntactic obligation is exactly T-Sub, plus the requirements on members: an override must accept at least what the overridden method accepted and return no more than it promised. Every statically checked object-oriented language enforces this. Java rejects an override that narrows a parameter type or widens a checked-exception set; C# and Kotlin do the same; @Override exists to catch the case where you meant to override and did not.

The behavioural obligation is the one Liskov actually wrote about, and it has three parts: a subtype may not strengthen a precondition, may not weaken a postcondition, and must preserve the supertype’s invariants. None of these is expressible in a mainstream type system, so none is checked.

The canonical demonstration is Square extends Rectangle. Rectangle offers setWidth and setHeight, and its implicit postcondition is that setting one does not change the other. Square must keep its sides equal, so setWidth also changes the height. Every signature matches. The compiler is entirely satisfied. And a function written against Rectangle that sets width to 5 and height to 4 and expects an area of 20 gets 16 when handed a Square. Nothing in any mainstream type system can catch this, which is worth stating plainly because it is the practical limit of the whole feature: subtyping is checked on shapes and used for behaviour.

Where does Dog <: Animal come from? Two families of answer, and the choice shapes an entire ecosystem.

Nominal subtyping requires a declaration: class Dog extends Animal, impl Display for Dog, struct Dog : Animal. The relation holds because someone said so. Accidental conformance is impossible, name-based invariants are enforceable — a UserId and an OrderId that are both integers underneath are genuinely different types — and adding a supertype to an existing type requires editing that type.

Structural subtyping requires only shape: if a type has the right members with the right types, it qualifies. TypeScript, Go’s interfaces and OCaml’s object types work this way. Third-party conformance is automatic, adapting a type from another library needs no wrapper, and accidental conformance is a real hazard — a type with a Close() error method satisfies io.Closer whether or not closing is what it does.

The full treatment is [[structural-vs-nominal]]; what matters here is that the *rule* — T-Sub — is identical in both, and only the definition of <: differs. That is a useful thing to notice, because it means the algorithmic difficulties of subtyping are shared: both need reflexivity and transitivity, both interact with [[variance]] the same way, and both destroy principal types.

Class inheritance is the most visible source of the relation and far from the only one. Recognising the others is what turns subtyping from an object-oriented topic into a type-system one.

Record width and depth. { name: string, age: int } <: { name: string } — a record with more fields is usable where fewer were demanded. That is width subtyping, and it is the whole basis of structural typing. Depth subtyping goes further: { pet: Dog } <: { pet: Animal }, which is only sound if the field is immutable — the subject of [[variance]].

Top and bottom types. Any, Object, unknown sit above everything; Nothing, never, ! sit below everything. A bottom type is genuinely useful: it is the type of an expression that does not return, which is what lets throw appear in a branch of a conditional without disturbing the other branch’s type.

Union and intersection types. T <: T | U always, and T & U <: T always. These are subtyping relations by construction, and they are why [[union-types]] and [[intersection-types]] compose with the rest of the system rather than sitting beside it.

Lifetimes. In Rust, a longer lifetime is a subtype of a shorter one: &'static str <: &'a str. This is real subtyping in a language people describe as not having any, and it is where most confusing Rust lifetime errors actually come from — see [[lifetime-analysis]].

What is *not* subtyping, despite looking like it: numeric widening. int to float changes the representation, so it is a conversion the compiler inserts, not a claim that an int value is a float value. The distinction matters because conversions cost an instruction and can lose precision, while subsumption is free and lossless by definition.