Are type abstraction values and universal types not for non functions, but only for functions? In Types and Programming Languages by Pierce, Chapter 23 Universal Types has a summary of System F in the following figure, in particular, "type abstraction values" and their types "universal types".

In all the examples I have seen so far in the chapter, in particular Section 23.4 Examples, (not sure if I miss any example):


all the type abstraction values are parametrically polymorphic functions, by allowing the types of their arguments to have any type, and
all the universal types, i.e. the types of type abstraction values, are types of parametrically polymorphic functions. 


Are type abstraction values and their universal types not for  non functions, but only for  functions? 

More specifically, in any type abstraction value, say $\lambda X.t$, must $t$ have a function type, not a non-function type?

In Section 23.4 Examples, values of base types and of recursive types  are type abstraction values, because their definitions in the section are   functions by Church encodings.

Thanks.
Short Answer: In λX₁. λX₂. ... λXₙ. t it doesn't matter if t is not a function, but if so, it may not be an interesting example for introduction.

Long Answer:

First of all, technically speaking, the type system defined in Figure 23-1 does NOT have any base types such as Bool or Nat. A type of t in λX. t is either a type variable X, a function type T → T, or a universal type ∀X. T.

Section 23.4, however, takes Nat as an example. So let's consider an extended type system by adding some base types and its values, terms, typing rules, etc. like Section 11.1 does.

Then we can consider, for example, a term λX. 42. This is a well-typed term. Proof:

\[
  \cfrac{}{
  \cfrac{\mathrm{X} ⊢ \mathrm{42} : \mathrm{Nat}}{
  ∅ ⊢ \mathrm{λ X. 42} : \mathrm{∀ X. Nat}
  }}
\]

This term, however, is not very interesting; polymorphism doesn't play any important role here.

Also, we can consider a type ∀X. X. But there is no term of type ∀X. X (i.e. there is no inhabitant of ∀X. X). This can be proved through the Curry-Howard correspondence. But this example may not be suitable for introduction of System F.

Section 23.7 writes a bit more interesting example. If we extend the type system by adding errors, we can consider a term λX. error. This term doesn't throw an error during an evaluation because of the type-abstraction. This observation gives an idea of a new type erasure method, described in Section 23.7.