Chapter 20: Recursive Types

---

Overview

We saw in §11.12 how to extend a simple type system to include a type constructor List(T) whose elements are lists with elements of type T. Lists are just one example of a large class of common structures-also including queues, binary trees, labeled trees, abstract syntax trees, etc.-that may grow to arbitrary size, but that have a simple, regular structure. An element of List(Nat), for example, is always either nil or else a pair (a "cons cell") of a number and another List(Nat). Clearly, it does not make sense to provide every one of these structures as a separate, primitive language feature. Instead, we need a general mechanism with which they can be defined from simpler elements, as needed. This mechanism is called recursive types.

Consider again the type of lists of numbers.^[1] We can represent the fact that a list is either nil or a pair using the variant and tuple types defined in §11.10 and §11.7:

   NatList = <nil:Unit, cons:{...,...}>; 

The data value carried by nil is trivial, since the nil tag itself already tells us everything that we need to know about an empty list. The value carried by the cons tag, on the other hand, is a pair consisting of a number and another list. The first component of this pair has type Nat,

   NatList = <nil:Unit, cons: {Nat, ...}>; 

while the second component is a list of numbers-i.e., an element of the very type NatList that we are defining:

   NatList = <nil:Unit, cons:{Nat,NatList}>; 

^[2]

This equation is not just a simple definition-that is, we are not giving a new name to a phrase whose meaning we already understand-since the right-hand side mentions the very name that we are in the process of defining. Instead, we can think of it as a specification of an infinite tree:

The recursive equation specifying this infinite tree type is similar to the equation specifying the recursive factorial function on page 52. Here, as there, it is convenient to make this equation into a proper definition by moving the "loop" over to the right-hand side of the =.^[3] We do this by introducing an explicit recursion operator μ for types:

   NatList = μX. <nil:Unit, cons:{Nat,X}>; 

Intuitively, this definition is read, "Let NatList be the infinite type satisfying the equation X = <nil:Unit, cons:{Nat,X}>.

We will see in §20.2 that there are actually two somewhat different ways of formalizing recursive types-the so-called equi-recursive and iso-recursive presentations-differing in the amount of help that the programmer is expected to give to the typechecker in the form of type annotations. In the programming examples in the following section, we use the lighter equi-recursive presentation.

^[1]We ignore, in the rest of this chapter, the question of how to give a single, generic definition of lists with elements of an arbitrary type T. To deal with this, we also need the mechanism of type operators, which will be introduced in Chapter 29.

^[2]The system studied in this chapter is the simply typed calculus with recursive types. The examples use a variety of features from earlier chapters; the associated checker for these is fullequirec. For §20.2, the associated checker is fullisorec.

^[3]The reason this move is convenient is that it allows us to talk about recursive types without giving them names. However, there are also some advantages to working with explicitly named recursive types-see the discussion of nominal vs. structural type systems in §19.3.

---