Chapter 15: Subtyping

---

We have spent the last several chapters studying the typing behavior of a variety of language features within the framework of the simply typed lambda-calculus. This chapter addresses a more fundamental extension: subtyping (sometimes called subtype polymorphism). Unlike the features we have studied up to now, which could be formulated more or less orthogonally to each other, subtyping is a cross-cutting extension, interacting with most other language features in non-trivial ways.

Subtyping is characteristically found in object-oriented languages and is often considered an essential feature of the object-oriented style. We will explore this connection in detail in Chapter 18; for now, though, we present subtyping in a more economical setting with just functions and records, where most of the interesting issues already appear. §15.5 discusses the combination of subtyping with some of the other features we have seen in previous chapters. In the final section (15.6) we consider a more refined semantics for subtyping, in which the use of suptyping corresponds to the insertion of run-time coercions.

15.1 Subsumption

Without subtyping, the rules of the simply typed lambda-calculus can be annoyingly rigid. The type system's insistence that argument types exactly match the domain types of functions will lead the typechecker to reject many programs that, to the programmer, seem obviously well-behaved. For example, recall the typing rule for function application:

^[1]

Figure 15-1: Simply Typed Lambda-Calculus with Subtyping (λ_<:)

According to this rule, the well-behaved term

   (λr:{x:Nat}. r.x) {x=0,y=1} 

is not typable, since the type of the argument is {x:Nat,y:Nat}, whereas the function accepts {x:Nat}. But, clearly, the function just requires that its argument is a record with a field x; it doesn't care what other fields the argument may or may not have. Moreover, we can see this from the type of the function-we don't need to look at its body to verify that it doesn't use any fields besides x. It is always safe to pass an argument of type {x:Nat,y:Nat} to a function that expects type {x:Nat}.

The goal of subtyping is to refine the typing rules so that they can accept terms like the one above. We accomplish this by formalizing the intuition that some types are more informative than others: we say that S is a subtype of T, written S <: T, to mean that any term of type S can safely be used in a context where a term of type T is expected. This view of subtyping is often called the principle of safe substitution.

A simpler intuition is to read S <: T as "every value described by S is also described by T," that is, "the elements of S are a subset of the elements of T. We shall see in §15.6 that other, more refined, interpretations of subtyping are sometimes useful, but this subset semantics suffices for most purposes.

The bridge between the typing relation and this subtype relation is provided by adding a new typing rule-the so-called rule of subsumption:

This rule tells us that, if S <: T, then every element t of S is also an element of T. For example, if we define the subtype relation so that {x:Nat,y:Nat} <: {x:Nat}, then we can use rule T-SUB to derive ⊢ {x=0,y=1} : {x:Nat}, which is what we need to make our motivating example typecheck.

^[1]The calculus studied in this chapter is λ_<:, the simply typed lambda-calculus with subtyping (Figure 15-1) and records (15-3); the corresponding OCaml implementation is rcdsub. (Some of the examples also use numbers; fullsub is needed to check these.)

---