Exercise 3.9
Find a closed λ2-version of $S ≡λxyz. xz(yz)$, and establish its type.
It is useful to remind ourselves of the derivation for the simply typed $S$ (ex 2.3).
There we found the type of $S$ is
$$ S : (B \to (A \to C)) \to (B \to A) \to B \to C $$
Here we want to parameterise the types of $x$, $y$ and $z$, and we can do this as follows.
$$ λα,β,γ:*. λx:β → (α→γ). λy:β→α . λz:β. xz(yz) : Παβγ:*.(β → (α→γ)) → (β→α) → β → γ$$
The type is analogous to the previously established type, but this time the components $α,β,γ$ are abstracted.
