23.9 Parametricity

---

23.9 Parametricity

Recall from §23.4 how we defined the type CBool of Church booleans

   CBool = "X.X→X→X; 

and the constants tru and fls:

   tru = λX. λt:X. λf:X. t; ▸ tru : CBool   fls = λX. λt:X. λf:X. f; ▸ fls : CBool 

Given the type CBool, we can actually write the definitions of tru and fls rather mechanically, simply by looking at the structure of the type. Since CBool begins with a ", any value of type CBool must be a type abstraction, so tru and fls must both begin with a λX. Then, since the body of CBool is an arrow type X→X→X, every value of this type must take two arguments of type X—i.e., the bodies of tru and fls must each begin λt:X.λf:X. Finally, since the result type of CBool is X, any value of type CBool must return an element of type X. But since X is a parameter, the only values of this type that we can possibly return are the bound variables t and f—we have no other way of obtaining or constructing values of this type ourselves. In other words, tru and fls are essentially the only inhabitants of the type CBool. Strictly speaking, CBool contains some other terms like (λb:CBool.b) tru, but it is intuitively clear that every one of them must behave like either tru or fls.

This observation is a simple consequence of a powerful principle known as parametricity, which formalizes the uniform behavior of polymorphic programs. Parametricity was introduced by Reynolds (1974, 1983) and has been further explored, along with related notions, by Reynolds (1984, Reynolds and Plotkin, 1993), Bainbridge et al. (1990), Ma (1992), Mitchell (1986), Mitchell and Meyer (1985), Hasegawa (1991), Pitts (1987, 1989, 2000), Abadi, Cardelli, Curien, and Plotkin (Abadi, Cardelli, and Curien, 1993; Plotkin and Abadi, 1993; Plotkin, Abadi, and Cardelli, 1994), Wadler (1989, 2001), and others. See Wadler (1989) for an expository introduction.

---