Chapter 28: Metatheory of Bounded Quantification

---

In this chapter we develop subtyping and typechecking algorithms for F_<:. We study both the kernel and the full variants of the system, which behave somewhat differently. Some properties are enjoyed by both but harder to prove for the full variant, while others are lost outright in full F_<:—the price we pay for the extra expressiveness of this system.

We first present a typechecking algorithm that works for both systems in §28.1 and §28.2. Then we consider subtype checking, taking first the kernel system in §28.3 and then the full system in §28.4. §28.5 continues the discussion of subtyping in full F_<:, focusing on the surprising fact that the subtype relation is undecidable. §28.6 shows that the kernel system has joins and meets, while the full system does not. §28.7 touches on some issues raised by bounded existentials, and §28.8 considers the effects of adding a minimal Bot type.

28.1 Exposure

In the typechecking algorithm in §16.2 for the simply typed lambda-calculus with subtyping, the key idea was to calculate a minimal type for each term from the minimal types of its subterms. We can use the same basic idea for F_<:, but we need to take into account one small complication arising from the presence of type variables in the system. Consider the term

   f = λX<:Nat→Nat. λy:X. y 5; ▸ f : "X<:Nat→Nat. X → Nat 

This term is clearly well typed, since the type of the variable y in the application y 5 can be promoted to Nat→Nat by T-SUB. But the minimal type of y is ^[1]X, which is not an arrow type. In order to find the minimal type of the whole application, we need to find the smallest arrow type that y possesses—i.e., the minimal arrow type that is a supertype of the type variable X. Not too surprisingly, we can find this type by promoting the minimal type of y until it becomes something other than a type variable.

Formally, we write Г ⊢ S ⇑ T (pronounced "S exposes to T under Г") to mean "T is the least nonvariable supertype of S." Exposure is defined by repeated promotion of variables, as shown in Figure 28-1.

Figure 28-1: Exposure Algorithm for F_<:

It is easy to see that these rules define a total function. Moreover, the result of exposing a type is always the least supertype that has some shape other than a variable. For example, if Г = X<:Top, Y<:Nat→Nat, Z<:Y, W<:Z, then:

      Г ⊢ Top ⇑ Top        Г ⊢ Y ⇑ Nat→Nat       Г ⊢ W ⇑ Nat→Nat      Г ⊢ X ⇑ Top          Г ⊢ Z ⇑ Nat→Nat 

The essential properties of exposure can be summarized as follows.

28.1.1 Lemma [Exposure]:

Suppose Г ⊢ S ⇑ T. Then:

1. Г ⊢ S <: T.

2. If Г ⊢ S <: U and U is not a variable, then Г ⊢ T <: U.

Proof: Part (1) goes by induction on a derivation of Г ⊢ S ⇑ T, part (2) by induction on a derivation of Г ⊢ S <: U.

^[1]The system studied in this chapter is pure F_<: (Figure 26-1). The corresponding implementation is purefsub; the fullfsub implementation also includes existentials (24-1) and several extensions from Chapter 11.

---