Chapter 23: Universal Types

---

In the previous chapter, we studied the simple form of let-polymorphism found in ML. In this chapter, we consider a more general form of polymorphism in the setting of a powerful calculus known as System F.

23.1 Motivation

As we remarked in §22.7, we can write an infinite number of "doubling" functions in the simply typed lambda-calculus…

   doubleNat = λf:Nat→Nat. λx:Nat. f (f x);   doubleRcd = λf:{l:Bool}→{l:Bool}. λx:{l:Bool}. f (f x);   doubleFun = λf:(Nat→Nat)→(Nat→Nat). λx:Nat→Nat. f (f x); 

Each of these functions is applicable to a different type of argument, but all share precisely the same behavior (indeed, they share precisely the same program text, aside from the typing annotations). If we want apply the doubling operation to different types of arguments within the same program, we will need to write out separate definitions of doubleT for each T. This kind of cut-and-paste programming violates a basic dictum of software engineering:

ABSTRACTION PRINCIPLE: Each significant piece of functionality in a program should be implemented in just one place in the source code. Where similar functions are carried out by distinct pieces of code, it is generally beneficial to combine them into one by abstracting out the varying parts.

^[1]

Figure 23-1: Polymorphic Lambda-Calculus (System F)

Here, the varying parts are the types! What we need, then, are facilities for abstracting out a type from a term and later instantiating this abstract term with concrete type annotations.

^[1]The system studied in most of this chapter is pure System F (Figure 23-1); the examples in §23.4 use various extensions with previously studied features. The associated OCaml implementation is fullpoly. (The examples involving pairs and lists require the fullomega checker.)

---