Chapter 16: Metatheory of Subtyping

---

Overview

The definition in the previous chapter of the simply typed lambda-calculus with subtyping is not immediately suitable for implementation. Unlike the other calculi we have seen, the rules of this system are not syntax directed—they cannot just be "read from bottom to top" to yield a typechecking algorithm. The main culprits are the rules of subsumption (T-SUB) in the typing relation and transitivity (S-TRANS) in the subtype relation.

The reason T-SUB is problematic is that the term in its conclusion is specified as a bare metavariable t:

Every other typing rule specifies a term of some specific form—T-ABS applies only to lambda-abstractions, T-VAR only to variables, etc.—while T-SUB can be applied to any kind of term. This means that, if we are given a term t whose type we are trying to calculate, it will always be possible to apply either T-SUB or the other rule whose conclusion matches the shape of t.

S-TRANS is problematic for the same reason—its conclusion overlaps with the conclusions of all the other rules.

Since S and T are bare metavariables, we can potentially use S-TRANS as the final rule in a derivation of any subtyping statement. Thus, a naive "bottom to top" implementation of the subtyping rules would never know whether to try using this rule or whether to try another rule whose more specific conclusion also matches the two types whose membership in the subtype relation we are trying to check. ^[1]

There is one other problem with S-TRANS. Both of its premises mention the metavariable U, which does not appear in the conclusion. If we read the rule naively from bottom to top, it says that we should guess a type U and then attempt to show that S <: U and U <: T. Since there are an infinite number of Us that we could guess, this strategy has little hope of success.

The S-REFL rule also overlaps the conclusions of the other subtyping rules. This is less severe than the problems with T-SUB and S-TRANS: the reflexivity rule has no premises, so if it matches a subtyping statement we are trying to prove, we can succeed immediately. Still, it is another reason why the rules are not syntax directed.

The solution to all of these problems is to replace the ordinary (or declarative) subtyping and typing relations by two new relations, called the algorithmic subtyping and algorithmic typing relations, whose sets of inference rules are syntax directed. We then justify this switch by showing that the original subtyping and typing relations actually coincide with the algorithmic presentations: the statement S <: T is derivable from the algorithmic subtyping rules iff it is derivable from the declarative rules, and a term is typable by the algorithmic typing rules iff it is typable under the declarative rules.

We develop the algorithmic subtype relation in §16.1 and the algorithmic typing relation in §16.2. §16.3 addresses the special typechecking problems of multi-branch constructs like if...then...else, which require additional structure (the existence of least upper bounds, or joins, in the subtype relation). §16.4 considers the minimal type Bot.

^[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. §16.3 also deals with booleans and conditionals (8-1); the OCaml implementation for this section is joinsub. §16.4 extends the discussions to Bot; the corresponding implementation is bot.

---