30.4 Fragments of F

---

30.4 Fragments of F_ω

Intuitively, it is clear that both λ→ and System F are contained in F_ω. We can make this intuition precise by defining a hierarchy of systems, F₁, F₂, F₃, etc., whose limit is F_ω.

30.4.1 Definition

In System F₁, the only kind is * and no quantification (") or abstraction (λ) over types is permitted. The remaining systems are defined with reference to a hierarchy of kinds at level i, defined as follows:

•  

  K1	=	⌉
  Ki+1	=	{*} È {J ⇛K | J Î Ki and K Î Ki+1}
  Kω	=	È1≤i Ki

In System F₂, we still have only kind * and no lambda-abstraction at the level of types, but we allow quantification over proper types (of kind *). In F₃, we allow quantification over type operators (i.e., we can write type expressions of the form "X::K.T, where K ÎK₃) and introduce abstraction over proper types (i.e., we consider type expressions of the form λX::*.T, giving them kinds like *⇛*). In general, F_i+1 permits quantification over types with kinds in K_i+1 and abstraction over types with kinds in K_i.

F₁ is just our simply typed lambda-calculus, λ_→. Its definition is superficially more complicated than Figure 9-1 because it includes kinding and type equivalence relations, but these are both trivial: every syntactically well formed type is also well kinded, with kind *, and the only type equivalent to a type T is T itself. F₂ is our System F; its position in this hierarchy is the reason why it is often called the second-order lambda-calculus. F₃ is the first system where the kinding and type equivalence relations become non-degenerate.

Interestingly, all the programs in this book live in F₃. (Strictly speaking, the type operators Object and Class in Chapter 32 are in F₄, since their argument is a type operator of kind (*⇛*)⇛*, but we could just as well treat these two as abbreviation mechanisms of the metalanguage rather than full-fledged expressions of the calculus, as we did with Pair before Chapter 29, since in the examples using Object and Class we do not need to quantify over types of this kind.) On the other hand, restricting our programming language to F₃ instead of using full F_ω does not actually simplify things very much, in terms of either implementation difficulty or metatheoretic intricacy, since the key mechanisms of type operator abstraction and type equivalence are already present at this level.

30.4.2 Exercise [⋆⋆⋆⋆ ↛]

Are there any useful programs that can be written in F₄ but not F₃?

---