◄ WORLD V · SONNY 5DART 249 · a helldive at the net

THE SUBTYPING if A can stand in for B everywhere, A is a subtype of B

Subtyping is the “is-a” relation made precise: A <: B means a value of type A may be used anywhere a B is expected. For records it is width subtyping — {x, y, z} is a subtype of {x, y} because it has (at least) the fields B demands. The Liskov Substitution Principle raises this from structure to behavior: a subtype must honor the supertype's contract, not merely its shape. Subtyping is what lets one piece of code serve many concrete types — and where variance, the trickiest corner of type systems, lives.

THE TECHNIQUE A <: B iff A supplies everything B requires (width subtyping)

Two record types by their field sets. The demo checks width subtyping: does the wider record supply every field the narrower one requires? live demo







  
HISTORY & CREDIT Cardelli 1984 · Liskov-Wing 1994

  
“Subtyping is inheritance.” — inheritance is one way to get it; subtyping is the substitutability itself, and it can be purely structural (having the right fields) with no class hierarchy at all. The relation is about use, not lineage. cited

  
1984 · Luca Cardelli — “A Semantics of Multiple Inheritance”: record subtyping, width and depth.
1994 · Barbara Liskov & Jeannette Wing — behavioral subtyping (the LSP made formal): a subtype must satisfy the supertype's spec.
now · structural subtyping in TypeScript/Go interfaces; nominal in Java/C#.

  
Substitutability is a contract, not a shape: a subtype may have more, but it must never demand more or promise less. Break the contract and the “is-a” is a lie the type checker cannot catch. Liskov-Wing 1994






  
RECOMMEND FOR I-13 width subtyping both directions, computed

  
On the canonical compiler, with fields as a bitmask, {x,y,z}=7 <: {x,y}=3 holds (1) but the reverse fails (0) — the narrower record lacks z:

  
$ i13 run t_subtyping.i13   # (wide & narrow)==narrow ?
xyz_sub_xy = 1          -- {x,y,z} supplies x,y -> subtype of {x,y}
xy_sub_xyz = 0          -- {x,y} lacks z -> NOT a subtype of {x,y,z}

  
Recommend: subtyping is N/A for I-13 — with a single type there is no “is-a” lattice, no variance, none of the subtlety that makes subtyping the hardest part of a type system. The demo computes width subtyping with a bitmask & (7<:3 holds), which i13 can evaluate, but i13 never needs to: there is one type, so everything trivially substitutes for everything. The cost of that simplicity is the safety subtyping buys — i13 will not stop you passing the wrong shape, because to it there are no shapes.