Chapter 29: Type Operators and Kinding

---

Overview

In previous chapters, we have often made use of abbreviations like

   CBool = "X. X → X → X; 

and

   Pair Y Z = "X. (Y→Z→X) →X; 

to make examples easier to read, writing λx:Pair Nat Bool. x, for instance, instead of the more cumbersome λx:"X.(Nat→Bool→X)→X. x.

CBool is a simple abbreviation; when we see it in an example, we should just replace it by the right-hand side of its definition. Pair, on the other hand, is a parametric abbreviation; when we encounter Pair S T, we must substitute the actual types S and T for the parameters Y and Z in its definition. In other words, abbreviations like Pair give us an informal notation for defining functions at the level of type expressions.

We have also used type-level expressions like Array T and Ref T involving the type constructorstype operators Array and Ref. Although these type constructors are built into the language, rather than being defined by the programmer, they are also a form of functions at the level of types. We can view Ref, for example, as a function that, for each type T, yields the type of reference cells containing an element of T.

Our task in this and the next two chapters is to treat these type-level functions, collectively called type operators, more formally. In this chapter, we introduce basic mechanisms of abstraction and application at the level of types, along with a precise definition of when two type expressions should be regarded as equivalent and a well-formedness relation, called kinding, that prevents us from writing nonsensical type expressions. Chapter 30 goes a step further and treats type operators as first-class citizens—i.e., as entities that can be passed as arguments to functions; that chapter introduces the well-known System F_ω, generalizing the quantification over types in System F (Chapter 23) to higher-order quantification over type operators. Chapter 31 considers the combination of type operators, higher-order quantification, and subtyping. ^[1]

 
Figure 29-1: Type Operators and Kinding (λ_ω)

^[1]The system introduced in this chapter is the pure simply typed lambda-calculus with type operators, λ_ω(Figure 29-1). The examples also use numbers and booleans (8-2) and universal types (23-1). The associated OCaml implementation is fullomega.

---