Chapter 26: Bounded Quantification

---

Many of the interesting issues in programming languages arise from interactions between features that are relatively straightforward when considered individually. This chapter introduces bounded quantification, which arises when polymorphism and subtyping are combined, substantially increasing both the expressive power of the system and its metatheoretic complexity. The calculus we will be studying, called F_<: ("F sub"), has played a central role in programming language research since it was developed in the mid '80s, in particular in studies on the foundations of object-oriented programming.

26.1 Motivation

The simplest way of combining subtyping and polymorphism is to take them as completely orthogonal features—i.e., to consider a system that is essentially the union of the systems from Chapters 15 and 23. This system is the-oretically unproblematic, and is useful for all of the reasons that subtyping and polymorphism are individually. However, once we have both features in the same language, it is tempting to mix them in more interesting ways. To illustrate, let us consider a very simple example—we will see others in §26.3 and some larger and more pragmatic case studies in Chapters 27 and 32.

Suppose f is the identity function on records with a numeric field a:

   f = λx:{a:Nat}. x; ▸ f : {a:Nat} → {a:Nat} 

If ra is a record with an a field, ^[1]

Figure 26-1: Bounded Quantification (Kernel F_<:)

   ra = {a=0}; 

then we can apply f to ra—in any of the type systems that we have seen in previous chapters—yielding a record of the same type.

   f ra; ▸ {a=0} : {a:Nat} 

Similarly, if we define a larger record rab with two fields, a and b,

   rab = {a=0, b=true}; 

we can also apply f to rab by using the rule of subsumption (T-Sub, Figure 15-1) to promote the type of rab to {a:Nat} to match the type expected by f.

   f rab; ▸ {a=0, b=true} : {a:Nat} 

However, the result type of this application has only the field a, which means that a term like (f rab).b will be judged ill typed. In other words, by passing rab through the identity function, we have lost the ability to access its b field!

Using the polymorphism of System F, we can write f in a different way:

   fpoly = λX. λx:X. x; ▸ fpoly : "X. X → X 

The application of fpoly to rab (and an appropriate type argument) yields the desired result:

   fpoly [{a:Nat, b:Bool}] rab; ▸ {a=0, b=true} : {a:Nat, b:Bool} 

But in making the type of x into a variable, we have given up some information that we might have wanted to use. For example, suppose we want to write a different version of f that returns a pair of its original argument and the numeric successor of its a field.

   f2 = λx:{a:Nat}. {orig=x, asucc=succ(x.a)}; ▸ f2 : {a:Nat} → {orig:{a:Nat}, asucc:Nat} 

Again, using subtyping, we can apply f2 to both ra and rab, losing the b field in the second case.

   f2 ra; ▸ {orig={a=0}, asucc=1} : {orig:{a:Nat}, asucc:Nat}   f2 rab; ▸ {orig={a=0,b=true}, asucc=1} : {orig:{a:Nat}, asucc:Nat} 

But this time polymorphism offers us no solution. If we replace the type of x by a variable X as before, we lose the constraint that x must be a record with an a field, which is required to compute the asucc field of the result.

   f2poly = λX. λx:X. {orig=x, asucc=succ(x.a)}; ▸ Error: Expected record type 

The fact about the operational behavior of f2 that we want to express in its type is that it takes an argument of any record type R that includes a numeric a field and returns as its result a record containing a field of type R and a field of type Nat. We can use the subtype relation to express this concisely: f2 takes an argument of any subtype R of the type {a:Nat} and returns a record containing a field of type R and a field of type Nat. This intuition can be formalized by introducing a subtyping constraint on the bound variable X of f2poly.

   f2poly = λX<:{a:Nat}. λx:X. {orig=x, asucc=succ(x.a)}; ▸ f2poly : "X<:{a:Nat}. X → {orig:X, asucc:Nat} 

This so-called bounded quantification is the characteristic feature of System F_<:.

^[1]The system studied in most of this chapter is pure F_<: (Figure 26-1). The examples also use records (11-7) and numbers (8-2). The associated OCaml implementations are fullfsub and fullfomsub. (The fullfsub checker suffices for most of the examples; fullfomsub is needed for the ones involving type abbreviations with parameters, such as Pair.)

---