23 - Subtyping

Summary

A subtype relation is a preorder (reflexive and transitive relation) on types that validates the subsumption principle:

If τ′ is a subtype of τ, then a value of type τ′ may be provided whenever a value of type τ is required.

The subsumption principle relaxes the strictures of a type system to permit values of one type to be treated as values of another.

Experience shows that the subsumption principle, although useful as a general guide, can be tricky to apply correctly in practice. The key to getting it right is the principle of introduction and elimination. To determine whether a candidate subtyping relationship is sensible, it suffices to consider whether every introductory form of the subtype can be safely manipulated by every eliminatory form of the supertype. A subtyping principlemakes sense only if it passes this test; the proof of the type safety theorem for a given subtyping relation ensures that this is the case.

A good way to get a subtyping principle wrong is to think of a type merely as a set of values (generated by introductory forms) and to consider whether every value of the subtype can also be considered to be a value of the supertype. The intuition behind this approach is to think of subtyping as akin to the subset relation in ordinary mathematics. But, as we subsequently see, this can lead to serious errors, because it fails to take account of the eliminatory forms that are applicable to the supertype.