15.4 The Top and Bottom Types

< Free Open Study >

The maximal type Top is not a necessary part of the simply typed lambda-calculus with subtyping; it can be removed without damaging the properties of the system. However, it is included in most presentations, for several reasons. First, it corresponds to the type Object found in most object-oriented languages. Second, Top is a convenient technical device in more sophisticated systems combining subtyping and parametric polymorphism. For example, in System F_<: (Chapters 26 and 28), the presence of Top allows us to recover ordinary unbounded quantification from bounded quantification, streamlining the system. Indeed, even records can be encoded in F_<:, further streamlining the presentation (at least for purposes of formal study); this encoding critically depends on Top. Finally, since Top's behavior is straightforward and it is often useful in examples, there is little reason not to keep it.

It is natural to ask whether we can also complete the subtype relation with a minimal element—a type Bot that is a subtype of every type. The answer is that we can: this extension is formalized in Figure 15-4.

Figure 15-4: Bottom Type

The first thing to notice is that Bot is empty—there are no closed values of type Bot. If there were one, say v, then the subsumption rule plus S-Bot would allow us to derive ⊢ v : Top→Top, from which the canonical forms lemma (15.3.6, which still holds under the extension) tells us that v must have the form λx:S₁ .t₂ for some S₁ and t₂. On the other hand, by subsumption, we also have ⊢ v : {}, from which the canonical forms lemma tells us that v must be a record. The syntax makes it clear that v cannot be both a function and a record, and so assuming that ⊢ v : Bot has led us to a contradiction.

The emptiness of Bot does not make it useless. On the contrary: Bot provides a very convenient way of expressing the fact that some operations (in particular, throwing an exception or invoking a continuation) are not intended to return. Giving such expressions the type Bot has two good effects: first, it signals to the programmer that no result is expected (since if the expression did return a result, it would be a value of type Bot); second, it signals to the typechecker that such an expression can safely be used in a context expecting any type of value. For example, if the exception-raising term error from Chapter 14 is given type Bot, then a term like

  λx:T.    if <check that x is reasonable> then      <compute result>    else      error

will be well typed because, no matter what the type of the normal result is, the term error can always be given the same type by subsumption, so the two branches of the if are compatible, as required by T-If.^[2]

Unfortunately, the presence of Bot significantly complicates the problem of building a typechecker for the system. A simple typechecking algorithm for a language with subtyping needs to rely on inferences like "if an application t₁ t₂ is well typed, then t₁ must have an arrow type." In the presence of Bot, we must refine this to "if t₁ t₂ is well typed, then t₁ must have either an arrow type or type Bot"; this point is expanded in §16.4. The complications are magnified further in systems with bounded quantification; see §28.8.

These complications show that adding Bot is a more serious step than adding Top. We shall omit it from the systems we consider in the remainder of the book.

^[2]In languages with polymorphism, such as ML, we can also use "X.X as a result type for error and similar constructs. This achieves the same effect as Bot by different means: instead of giving error a type that can be promoted to any type, we give it a type scheme that can be instantiated to any type. Though they rest on different foundations, the two solutions are quite similar: in particular, the type "X.X is also empty.

< Free Open Study >