15.2 The Subtype Relation

---

15.2 The Subtype Relation

The subtype relation is formalized as a collection of inference rules for deriving statements of the form S <: T, pronounced "S is a subtype of T" (or "T is a supertype of S"). We consider each form of type (function types, record types, etc.) separately; for each one, we introduce one or more rules formalizing situations when it is safe to allow elements of one type of this form to be used where another is expected.

Before we get to the rules for particular type constructors, we make two general stipulations: first, that subtyping should be reflexive,

and second, that it should be transitive:

These rules follow directly from the intuition of safe substitution.

Now, for record types, we have already seen that we want to consider the type S = {k₁:S₁...k_m:S_m} to be a subtype of T = {l₁:T₁...l_n :T_n} if T has fewer fields than S. In particular, it is safe to "forget" some fields at the end of a record type. The so-called width subtyping rule captures this intuition:

It may seem surprising that the "smaller" type-the subtype-is the one with more fields. The easiest way to understand this is to adopt a more liberal view of record types than we did in §11.8, regarding a record type {x:Nat} as describing "the set of all records with at least a field x of type Nat." Values like {x=3} and {x=5} are elements of this type, and so are values like {x=3,y=100} and {x=3,a=true,b=true}. Similarly, the record type {x:Nat,y:Nat} describes records with at least the fields x and y, both of type Nat. Values like {x=3,y=100} and {x=3,y=100,z=true} are members of this type, but {x=3} is not, and neither is {x=3,a=true,b=true}. Thus, the set of values belonging to the second type is a proper subset of the set belonging to the first type. A longer record constitutes a more demanding-i.e., more informative-specification, and so describes a smaller set of values.

The width subtyping rule applies only to record types where the common fields are identical. It is also safe to allow the types of individual fields to vary, as long as the types of each corresponding field in the two records are in the subtype relation. The depth subtyping rule expresses this intuition:

The following subtyping derivation uses S-RCDWIDTH and S-RCDDEPTH together to show that the nested record type {x:{a:Nat,b:Nat},y:{m:Nat}} is a subtype of {x:{a:Nat},y:{}}:

If we want to use S-RCDDEPTH to refine the type of just a single record field (instead of refining every field, as we did in the example above), we can use S-REFL to obtain trivial subtyping derivations for the other fields.

We can also use the transitivity rule, S-TRANS, to combine width and depth subtyping. For example, we can obtain a supertype by promoting the type of one field while dropping another:

Our final record subtyping rule arises from the observation that the order of fields in a record does not make any difference to how we can safely use it, since the only thing that we can do with records once we've built them-i.e., projecting their fields-is insensitive to the order of fields.

For example, S-RCDPERM tells us that {c:Top,b:Bool,a:Nat} is a subtype of {a:Nat,b:Bool,c:Top}, and vice versa. (This implies that the subtype relation will not be anti-symmetric.)

S-RCDPERM can be used in combination with S-RCDWIDTH and S-TRANS to drop fields from anywhere in a record type, not just at the end.

15.2.1 Exercise [⋆]

Draw a derivation showing that {x:Nat,y:Nat,z:Nat} is a subtype of {y:Nat}.

S-RCDWIDTH, S-RCDDEPTH, and S-RCDPERM each embody a different sort of flexibility in the use of records. For purposes of discussion, it is useful to present them as three separate rules. In particular, there are languages that allow some of them but not others; for example, most variants of Abadi and Cardelli's object calculus (1996) omit width subtyping. However, for purposes of implementation it is more convenient to combine them into a single macro-rule that does all three things at once. This rule is discussed in the next chapter (cf. page 211).

Since we are working in a higher-order language, where not only numbers and records but also functions can be passed as arguments to other functions, we must also give a subtyping rule for function types-i.e., we must specify under what circumstances it is safe to use a function of one type in a context where a different function type is expected.

Notice that the sense of the subtype relation is reversed (contravariant) for the argument types in the left-hand premise, while it runs in the same direction (covariant) for the result types as for the function types themselves. The intuition is that, if we have a function f of type S₁ → S₂, then we know that f accepts elements of type S₁; clearly, f will also accept elements of any subtype T₁ of S₁. The type of f also tells us that it returns elements of type S₂; we can also view these results belonging to any supertype T₂ of S₂. That is, any function f of type S₁ → S₂ can also be viewed as having type T₁ → T₂.

An alternative view is that it is safe to allow a function of one type S₁ → S₂ to be used in a context where another type T₁ → T₂ is expected as long as none of the arguments that may be passed to the function in this context will surprise it (T₁ <: S₁) and none of the results that it returns will surprise the context (S₂ <: T₂).

Finally, it is convenient to have a type that is a supertype of every type. We introduce a new type constant Top, plus a rule that makes Top a maximum element of the subtype relation.

§15.4 discusses the Top type further.

Formally, the subtype relation is the least relation closed under the rules we have given. For easy reference, Figures 15-1, 15-2, and 15-3 recapitulate the full definition of the simply typed lambda-calculus with records and subtyping, highlighting the syntactic forms and rules we have added in this chapter. Note that the presence of the reflexivity and transitivity rules means that the subtype relation is clearly a preorder; however, because of the record permutation rule, it is not a partial order: there are many pairs of distinct types where each is a subtype of the other.

Figure 15-2: Records (Same as Figure 11-7)

Figure 15-3: Records and Subtyping

To finish the discussion of the subtype relation, let us verify that the example at the beginning of the chapter now typechecks. Using the following abbreviations to avoid running off the edge of the page,

and assuming the usual typing rules for numeric constants, we can construct a derivation for the typing statement ⊢ f xy : Nat as follows:

15.2.2 Exercise [⋆]

Is this the only derivation of the statement ⊢ f xy : Nat?

15.2.3 Exercise [⋆]

(1) How many different supertypes does {a:Top,b:Top} have? (2) Can you find an infinite descending chain in the subtype relation-that is, an infinite sequence of types S₀, S₁, etc. such that each S_i+1 is a subtype of S_i? (3) What about an infinite ascending chain?

15.2.4 Exercise [⋆]

Is there a type that is a subtype of every other type? Is there an arrow type that is a supertype of every other arrow type?

15.2.5 Exercise [⋆⋆]

Suppose we extend the calculus with the product type constructor T₁ × T₂ described in §11.6. It is natural to add a subtyping rule

corresponding to S-RCDDEPTH for records. Would it be a good idea to add a width subtyping rule for products

as well?

---