The way I understand these types is by thinking of what functions I can build that satisfy the signature.
Booleans
For booleans, we have the type $\Pi\alpha . \alpha \rightarrow \alpha \rightarrow \alpha$. All members of this type will take in two abstract values (that is, values of type $\alpha$, where $\alpha$ can be anything) and return an abstract value (an $\alpha$).
In System F, there are exactly two functions that match this signature: $(\lambda x . \lambda y . x)$ and $(\lambda x . \lambda y . y)$. We can name them true and false and properly claim "all booleans are either true or false".
Integers
Integers have the type $\Pi\alpha . \alpha \rightarrow (\alpha \rightarrow \alpha) \rightarrow \alpha$. All members of this type need to be functions that take in two things: an abstract value and a function on abstract values, and return an abstract value.
(Again, we don't know anything about what type $\alpha$ actually is, nor do we know what the function of type $(\alpha \rightarrow \alpha)$ does. It could be the identity, it could be the successor function, it could accept a list and return the empty list.)
One function that matches this signature is $(\lambda x . \lambda f . x)$. Another is $(\lambda x . \lambda f . f x)$. Yet another is $(\lambda x . \lambda f . f (f x))$. There are countably many of these functions, so we can put them in one-to-one correspondence with the natural numbers and name them 0, 1, 2, ... . The only difference between these and Church numerals is that you can only apply them to values $x$ and $f$ with the right type.
Lists & Trees
After integers, lists and trees are easy. The type for lists, like you said, is $\Pi \alpha . \alpha \rightarrow (U \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$. Again, members of this type take in two arguments, an abstract value and a function that can manipulate abstract values, and returns an abstract value. The interesting part is the type $U$, which Girard uses to denote the type of elements in the list. A List Boolean has type $\Pi \alpha . \alpha \rightarrow (Boolean \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$.
We can easily define a function nil as $(\lambda x . \lambda f . x)$. That's one way to return a list given the arguments $x$ and $f$. The only other thing we can do to return a list is to apply the function $f$; given a value $u$ of type $U$, we could make the function $(\lambda x . \lambda f . f u x)$. If we parameterize over the value $u$, we get a more familiar cons function: $(\lambda u . \lambda x . \lambda f . f u x)$. Its type is $\Pi U . \Pi \alpha . \alpha \rightarrow (U \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$.
Trees have the type $\Pi \alpha . \alpha \rightarrow (U \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$. You just add another branch!
Example: Lists in other Programming Languages
A list is one of two things:
- Empty
- Non empty, so we can think of it as one element attached to a smaller list
Let's stick to lists of integers, which Girard would describe with the type $\Pi \alpha . \alpha \rightarrow (Integer \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$. His empty list is $\alpha$, the first argument, and his non-empty list is the second argument (which is a function expecting one element and another list).
In Java, we could represent these two alternatives by making an interface and a pair of classes.
interface IntList {}
class Empty implements IntList {}
class Cons implements IntList { int head; IntList tail; }
The Cons class has fields representing the two parts of any non-empty list.
In OCaml, things look a little more like System F.
type int_list = Empty | Cons of int * int_list
Again, there are two alternatives. A list can be Empty, or it can be a pair like Cons(2, Empty) made of an element and another list.
Girard's type is difficult to read because he expresses these ideas with one $\Pi$-type, but the idea's the same.
Below, I will write definitions on the form $\mathsf{foo}(x_1,\ldots,x_n)=e$ as syntactic sugar for $\mathsf{foo}=\lambda x_1.\cdots.\lambda x_n.e$ and expressions on the form $\mathsf{foo}(e_1,\ldots,e_n)$ as syntactic sugar for $\mathsf{foo}\ e_1\ \ldots\ e_n$.
List constructors:
- $\mathsf{nil} = \lambda c.\lambda n.n$
- $\mathsf{cons}(x,l) = \lambda c.\lambda n.c\ x\ (l\ c\ n)$
By these we have for example
$$\begin{align}
\mathsf{cons}(N_1, \mathsf{nil})
&= \lambda c.\lambda n.c\ N_1\ (\mathsf{nil}\ c\ n)
\to_\beta \lambda c.\lambda n.c\ N_1\ n
\\
\mathsf{cons}(N_1, \mathsf{cons}(N_2, \mathsf{nil}))
&= \lambda c.\lambda n.c\ N_1\ (\mathsf{cons}(N_2, \mathsf{nil})\ c\ n)
\\
&= \lambda c.\lambda n.c\ N_1\ ((\lambda c'.\lambda n'.c'\ N_2\ n')\ c\ n)
\\
&\to_\beta \lambda c.\lambda n.c\ N_1\ (c\ N_2\ n)
\end{align}$$
To get the head of a list, we need to find some function $c_{\mathsf{head}}$ and some value $n$ such that $\mathsf{cons}(x,l)\ c_{\mathsf{head}}\ n$ reduces to $x$. But
$$
\mathsf{cons}(x,l)\ c_{\mathsf{head}}\ n
= (\lambda c'.\lambda n'.c'\ x\ (l\ c'\ n'))\ c_{\mathsf{head}}\ n
\to_\beta c_{\mathsf{head}}\ x\ (l\ c'\ n)
$$
so we see that we can just take $c_{\mathsf{head}} = \lambda x.\lambda r.x$ and the value of $n$ doesn't matter.
Therefore, we can take
$$
\mathsf{head}(l) = l\ (\lambda x.\lambda r.x)\ \mathsf{id}
$$
where $\mathsf{id}(x)=x$.
To check if a list is empty, we need to find some function $c_{\mathsf{empty}}$ and some value $n$ such that $\mathsf{nil}\ c_{\mathsf{empty}}\ n$ reduces to $\mathsf{true}$, while $\mathsf{cons}(x,l)\ c_{\mathsf{empty}}\ n$ reduces to $\mathsf{false}$. But
$$
\mathsf{nil}\ c_{\mathsf{empty}}\ n
= (\lambda c'.\lambda n'.n')\ c_{\mathsf{empty}}\ n
\to_\beta n
$$
and
$$
\mathsf{cons}(x,l)\ c_{\mathsf{empty}}\ n
= (\lambda c'.\lambda n'.c'\ x\ (l\ c'\ n'))\ c_{\mathsf{empty}}\ n
\to_\beta c_{\mathsf{empty}}\ x\ (l\ c_{\mathsf{empty}}\ n)
.
$$
Note that the result for $\mathsf{nil}$ equals $n$ so we can take $n=\mathsf{true}$, and the result for $\mathsf{cons}(x,l)$ is an application of $c_{\mathsf{empty}}$ so we can just let $c_{\mathsf{empty}}\ x\ r$ return $\mathsf{false}.$ We therefore define
$$
\mathsf{empty}(l) = l\ (\lambda x.\lambda r.\mathsf{false})\ \mathsf{true}
$$
Showing that $\mathsf{head}\ (\mathsf{cons}\ a\ l) \to_\beta^* a$:
$$\begin{align}
\mathsf{head}\ (\mathsf{cons}\ a\ l)
&= (\lambda l'.l'\ (\lambda x.\lambda r.x)\ \mathsf{id})\ (\mathsf{cons}\ a\ l) \\
&\to_\beta (\mathsf{cons}\ a\ l)\ (\lambda x.\lambda r.x)\ \mathsf{id} \\
&= ((\lambda x'.\lambda l'.\lambda c.\lambda n.c\ x'\ (l'\ c\ n))\ a\ l)\ (\lambda x.\lambda r.x)\ \mathsf{id} \\
&= (\lambda x'.\lambda l'.\lambda c.\lambda n.c\ x'\ (l'\ c\ n))\ a\ l\ (\lambda x.\lambda r.x)\ \mathsf{id} \\
&\to_\beta (\lambda l'.\lambda c.\lambda n.c\ a\ (l'\ c\ n))\ l\ (\lambda x.\lambda r.x)\ \mathsf{id} \\
&\to_\beta (\lambda c.\lambda n.c\ a\ (l\ c\ n))\ (\lambda x.\lambda r.x)\ \mathsf{id} \\
&\to_\beta (\lambda n.(\lambda x.\lambda r.x)\ a\ (l\ (\lambda x.\lambda r.x)\ n))\ \mathsf{id} \\
&\to_\beta (\lambda x.\lambda r.x)\ a\ (l\ (\lambda x.\lambda r.x)\ \mathsf{id})) \\
&\to_\beta (\lambda r.a)\ (l\ (\lambda x.\lambda r.x)\ \mathsf{id})) \\
&\to_\beta a \\
\end{align}$$
Best Answer
Question 1. Just apply the definition of list and the fact that $\mathsf{times} \, \underline{n} \, \underline{m} \to_\beta^* \underline{n \times m}$, where $\underline{n}$ is the Church numeral of $n$, for every natural number $n$.
\begin{align} [\,\underline{3}, \underline{2}, \underline{1}\,] \, \mathsf{times} \, \underline{1} &= \big( \lambda c. \lambda n. c\,\underline{3} ( c \, \underline{2} (c \, \underline{1} \, n) ) \big) \mathsf{times} \, \underline{1} \\ &\to_\beta \big( \lambda n. \mathsf{times} \,\underline{3} ( \mathsf{times} \, \underline{2} (\mathsf{times} \, \underline{1} \, n) ) \big) \underline{1} \\ &\to_\beta \mathsf{times} \,\underline{3} ( \mathsf{times} \, \underline{2} (\mathsf{times} \, \underline{1} \, \underline{1}) ) \\ &\to_\beta^* \mathsf{times} \,\underline{3} ( \mathsf{times} \, \underline{2} (\underline{1 \times 1}) ) \\ &= \mathsf{times} \,\underline{3} ( \mathsf{times} \, \underline{2} \, \underline{1} ) \\ &\to_\beta^* \mathsf{times} \,\underline{3} ( \underline{2 \times 1} ) \\ &= \mathsf{times} \,\underline{3} \, \underline{2} \\ &\to_\beta^* \underline{3 \times 2} \\ &= \underline{6} \end{align}
Question 2. Just apply the definitions of $\mathsf{cons}$ and of list. \begin{align} \mathsf{cons} \, 3 \, [2, 1] &= (\lambda x. \lambda l. \lambda c. \lambda n. cx (lcn)) \, 3 \, [2,1] \\ &\to_\beta (\lambda l. \lambda c. \lambda n. c\,3 (lcn)) [2,1] \\ &\to_\beta \lambda c. \lambda n. c\,3 ([2,1] cn) \\ &= \lambda c. \lambda n. c\,3 \big((\lambda c'. \lambda n'. c' 2 (c' 1 \, n')) c\,n \big) \\ &\to_\beta \lambda c. \lambda n. c\,3 \big((\lambda n'. c \, 2 (c \, 1 \, n')) n \big) \\ &\to_\beta \lambda c. \lambda n. c\,3 ( c \, 2 (c \, 1 \, n) ) \\ &= [3,2,1] \end{align}
Note that in Question 2, the fact that $1, 2, 3$ are Church numerals do not play any role. Actually, $1, 2, 3$ here could be replaced by any $\lambda$-terms.