16.4 Algorithmic Typing and the Bottom Type

---

16.4 Algorithmic Typing and the Bottom Type

If a minimal type Bot (§15.4) is added to the subtype relation, the subtyping and typing algorithms must be extended a little. We add one rule (the obvious one) to the algorithmic subtype relation

and two slightly trickier ones to the algorithmic typing relation:

The subtyping rule is clear. The intuition behind the typing rules is that, in the declarative system, we can apply something of type Bot to an argument of absolutely any type (by using subsumption to promote the Bot to whatever function type we like), and assume that the result has any other type, and similarly for projection.

16.4.1 Exercise [⋆]

Suppose we also have conditionals in the language. Do we need to add another algorithmic typing rule for if?

The additions needed to support Bot in this language are not overly complicated. We will see in §28.8, though, that more serious complications arise when Bot is combined with bounded quantification.

---