28.8 Bounded Quantification and the Bottom Type

---

28.8 Bounded Quantification and the Bottom Type

The addition of a minimal Bot type (§15.4) somewhat complicates the metatheoretic properties of F_<:. The reason for this is that, in a type of the form "X<:Bot.T, the variable X is actually a synonym for Bot inside T, since X is a subtype of Bot by assumption and Bot is a subtype of X by the rule S-BOT. This, in turn, means that pairs of types such as "X<:Bot.X→X and "X<:Bot.Bot→Bot are equivalent in the subtype relation, even though they are not syntactically identical. Moreover, if the ambient context contains the assumptions X<:Bot and Y<:Bot, then the types X→Y and Y→X are equivalent even though neither of them mentions Bot explicitly. Despite these difficulties, the essential properties of kernel F_<: can still be established in the presence of Bot. Details can be found in Pierce (1997a).

---