Chapter 30: Higher-Order Polymorphism

---

Having seen in Chapter 29 how to add type operators to λ_→, the natural next step is to mix them with the other typing features we have studied throughout the book. In this chapter, we combine type operators with the polymorphism of System F, yielding a well-known system called F_ω (Girard, 1972). Chapter 31 enriches this system with subtyping to form System , which is the setting for our final case study of purely functional objects in Chapter 32.

The definition of F_ω is a straightforward combination of features from λ_ω and System F. However, proving the basic properties of this system (in particular, preservation and progress) requires somewhat harder work than most of the systems we have seen, because we must deal with the fact that type-checking now requires evaluation at the level of types. These proofs will be the main job of this chapter.

30.1 Definitions

System F_ω is formed by combining System F from Chapter 23 and λ_ω from Chapter 29, adding kinding annotations (X::K) in places where type variables are bound (i.e., in type abstractions and quantifiers). The formal definition for the system with just universal quantifiers (not existentials) is given in Figure 30-1. We list the rules in full, even though the differences from earlier systems are minor, for easy reference in the proofs in §30.3.

 
Figure 30-1: Higher-Order Polymorphic Lambda-Calculus (F_ω)

We abbreviate "X::*.T as "X.T and {$X::*,T} as {$X,T}, so that terms of System F can be read directly as terms of F_ω.

Similarly, we obtain the higher-order variant of existential types by generalizing bindings from X to X::K in the original presentation of existentials in Chapter 24. Figure 30-2 summarizes this extension. ^[1].

Figure 30-2: Higher-Order Existential Types

^[1]The examples in this chapter are terms of F_ω (Figure 30-1) with records, booleans, and existentials (30-2). The associated OCaml implementation is fullomega. No implementation is provided for the dependent types mentioned in §30.5

---