23.3 System F

---

23.3 System F

The system we will be studying in this chapter, commonly called System F, was first discovered by Jean-Yves Girard (1972), in the context of proof theory in logic. A little later, a type system with essentially the same power was developed, independently, by a computer scientist, John Reynolds (1974), who called it the polymorphic lambda-calculus. This system has been used extensively as a research vehicle for foundational work on polymorphism and as the basis for numerous programming language designs. It is also sometimes called the second-order lambda-calculus, because it corresponds, via the Curry-Howard correspondence, to second-order intuitionistic logic, which allows quantification not only over individuals [terms], but also over predicates [types].

The definition of System F is a straightforward extension of λ_→, the simply typed lambda-calculus. In λ_→, lambda-abstraction is used to abstract terms out of terms, and application is used to supply values for the abstracted parts. Since we want here a mechanism for abstracting types out of terms and filling them in later, we introduce a new form of abstraction, written λX.t, whose parameter is a type, and a new form of application, t [T], in which the argument is a type expression. We call our new abstractions type abstractions and the new application construct type application or instantiation.

When, during evaluation, a type abstraction meets a type application, the pair forms a redex, just as in lgr;_→. We add a reduction rule

analogous to the ordinary reduction rule for abstractions and applications.

For example, when the polymorphic identity function

   id = λX. λx:X. x; 

is applied to Nat by writing id [Nat], the result is [X ↦ Nat](λx:X.x), i.e., λx:Nat.x, the identity function on natural numbers.

Finally, we need to specify the type of a polymorphic abstraction. We use types like Nat→Nat for classifying ordinary functions like λx:Nat.x; we now need a different form of "arrow type" whose domain is a type, for classifying polymorphic functions like id. Notice that, for each argument T to which it is applied, id yields a function of type T→T; that is, the type of the result of id depends on the actual type that we pass it as argument. To capture this dependency, we write the type of id as "X.X→X. The typing rules for polymorphic abstraction and application are analogous to the rules for term-level abstraction and application.

Note that we include the type variable X in the context used by the subderivation for t. We continue the convention (5.3.4) that the names of (term or type) variables should be chosen so as to be different from all the names already bound by Г and that lambda-bound type variables may be renamed at will in order to satisfy this condition. (In some presentations of System F, this freshness condition is given as an explicit side condition on the T-TABS rule, instead of being built into the rules about how contexts are constructed, as we are doing here.) For the moment, the only role of type variables in contexts is to keep track of scopes and make sure that the same type variable is not added twice to a context. In later chapters, we will annotate type variables with information of various kinds, such as bounds (Chapter 26) and kinds (Chapter 29).

Figure 23-1 shows the complete definition of the polymorphic lambda-calculus, with differences from λ_→ highlighted. As usual, this summary defines just the pure calculus, omitting other type constructors such as records, base types such as Nat and Bool, and term-language extensions such as let and fix. These extra constructs can be added straightforwardly to the pure system, and we will use them freely in the examples that follow.

---