How does this allow list operations to be applied to lists with elements of any type? 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 ﬁrst 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 ﬁnite-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 classiﬁed 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 ﬁnite-length lists whose elements are
  drawn from T.
  
  Figure 11-13 summarizes the syntax, semantics, and typing rules for
  lists. Except for syntactic diﬀerences (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 iﬀ
  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 ﬁrst 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
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 ﬁnite-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.