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

Answer 1

Most importantly, Section 11.12 does not introduce polymorphic lists, but introduces monomorphic lists annotated by a type of its elements.

For example, Fig. 11-13 introduces a new term cons[T] t t. Here [T] is a type annotation, which indicates a type of elements of the list. Note that T is a metavariable ranged over types, not an object-level type variable or a type-level abstraction. In other words, it is different statements that "For every type T, the type List T has property P" and "the type of polymorphic lists ∀X. List X has property P". See Section 3.1 for details of metavariables.

I think most of your questions are answered in short by the above explanation. The followings are more detailed answers.

Q1

• Does Section 11.12 introduce lists and list operations by making use of some kind of polymorphism, or type inference?

Neither. It introduces monomorphic lists annotated by an element type (No need of type inference).

Q2

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

T is a metavariable. For instance, it implies a type List Bool describes finite-length lists whose elements are drawn from Bool.

Q3

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

T is a metavariable. It may give you an intuition to try typing some actual program which contains lists.

Q4

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

Yes/No. Both sections try to define the type List T as "a type of lists whose elements are drawn from T", but they define List T individually: List T of Section 11.12 is defined in Figure 11-13, and List T of Section 23.4 is defined informally in sentences.

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

As written in the book, the notation of List T is the same, but list-related primitives are defined differently.

Q5

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

Chapter 20 describes a type system to handle general recursive types, rather than a specific recursive type (e.g. List T). Actually the beginning of Chapter 20 takes List T as an example of recursive types.