20.3 Subtyping

---

20.3 Subtyping

The final question that we need to address in this chapter concerns the combination of recursive types with the other major refinement of the simply typed lambda-calculus that we have seen so far-subtyping. For example, supposing that the type Even is a subtype of Nat, what should be the relation between the types μX.Nat→(Even × X) and μX.Even→(Nat × X)?

The simplest way to think through such questions is to view them "in the limit"-i.e., using an equi-recursive treatment of recursive types. In the present example, the elements inhabiting both types can be thought of as simple reactive processes (cf. page 271): given a number, they return another number plus a new process that is ready to receive a number, and so on. Processes belonging to the first type always yield even numbers and are capable of accepting arbitrary numbers. Those belonging to the second type yield arbitrary numbers, but expect always to be given even numbers. The constraints both on what arguments the function must accept and on what results it may return are more demanding for the first type, so intuitively we expect the first to be a subtype of the second. We can draw a picture summarizing these calculations as follows:

Can this intuitive argument be made precise? Indeed it can, as we shall see in Chapter 21.

---