11.12 Lists

---

11.12 Lists

The typing features we have seen can be classified into base types like Bool and Unit, and type constructors like → and × that build new types from old ones. Another useful type constructor is List. For every type T, the type List T describes finite-length lists whose elements are drawn from T.

Figure 11-13 summarizes the syntax, semantics, and typing rules for lists. Except for syntactic differences (List T instead of T list, etc.) and the explicit type annotations on all the syntactic forms in our presentation,^[10] these lists are essentially identical to those found in ML and other functional languages. The empty list (with elements of type T) is written nil[T]. The list formed by adding a new element t₁ (of type T) to the front of a list t₂ is written cons[T] t₁ t₂. The head and tail of a list t are written head[T] t and tail[T] t. The boolean predicate isnil[T] t yields true iff t is empty.^[11]

Figure 11-13: Lists

11.12.1 Exercise [⋆⋆⋆]

Verify that the progress and preservation theorems hold for the simply typed lambda-calculus with booleans and lists.

11.12.2 Exercise [⋆⋆]

The presentation of lists here includes many type annotations that are not really needed, in the sense that the typing rules can easily derive the annotations from context. Can all the type annotations be deleted?

^[10]Most of these explicit annotations could actually be omitted (Exercise [⋆, ↛]: which cannot); they are retained here to ease comparison with the encoding of lists in §23.4.

^[11]We adopt the "head/tail/isnil presentation" of lists here for simplicity. from the perspective of language design, it is arguably better to treat lists as a datatype and use case expressions for destructing them, since more programming errors can be caught as type errors this way.

---