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. ...

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.

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.