How does this allow list operations to be applied to lists with elements of any type?

Question

In Types and Programming Languages by Pierce, Chapter 11 is simple extensions of the simply typed lambda calculus with any simple base types. Section 11.12 introduces Lists.

How does the section allow list operations to be applied to lists with elements of any type? Specifically, my confusions are:

• Does Section 11.12 introduce lists and list operations by making use of some kind of polymorphism, or type inference? (The book doesn't introduce type inference till Chapter 22 and parametric polymorphism till Chapter 23.)

  Does "When we first introduced lists in §11.12, we used “custom” inference rules to allow the operations to be applied to lists with elements of any type" in Section 23.4 mean that Section 11.12 makes use of type inference to achieve similar behavior of "polymorphism"?

• Does "For every type T, the type List T describes finite-length lists whose elements are drawn from T" in Section 11.12 mean

  • that List T is a single literal type name for all possible specific typess for T, or
  • that List T should be instantiated differently for different specific types for T, e.g. List Boolean, List Nat?

• Is [T] part of the the names of the list operators, e.g. nil[T], cons[T], isnil[T]?

  Should [T] in nil[T] be instantiated differently for different specific types for T, e.g. nil[Boolean], nil[Nat]?

• Does Section 23.4 use the same type List T as in Section 11.12? Where is List T defined?

• I think lists are not simple types but recursive types (not introduced till Chapter 20), so why does Section 11.12 cover lists?

Thanks.

11 Simple Extensions

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, 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 t1 (of type T) to the front of a list t2 is written cons[T] t1 t2 . 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.

and

23 Universal Types

23.4 Examples

Polymorphic Lists

As an example of straightforward polymorphic programming, suppose our programming language is equipped with a type constructor List and term constructors for the usual list manipulation primitives, with the following types.

ñ nil : ∀X. List X
cons : ∀X. X → List X → List X
isnil : ∀X. List X → Bool
head : ∀X. List X → X
tail : ∀X. List X → List X

When we first introduced lists in §11.12, we used “custom” inference rules to allow the operations to be applied to lists with elements of any type. Here, we can give the operations polymorphic types expressing exactly the same constraints