Exercise 2.4
Add types to the bound variables in the following λ-terms such that they become pre-typed λ-terms which are legal, and give their types:
(a) $λxyz. x(yz)$
(b) $λxyz. y(xz)x$
(a) Let's first work out the types for $λxyz. x(yz)$.
We start with $x:A, y:B, z:C$. Since $y$ is applied to $z$ we have $B = C \to D$, and the type of $(yz)$ is D. Since $x$ is applied to $(yz)$ we must have $A = D \to E$.
Let's summarise this.
$$ (D \to E) \to (C \to D) \to C \to E $$
Renaming variables, and writing as a pre-typed λ-term we have
$$ λx: (β \to \gamma).λy: (α \to β).λz: α . x(yz) $$
The type is
$$(β \to \gamma) \to (α \to β) \to α \to \gamma$$
(b) Let's now work out the types for $λxyz. y(xz)x$.
We start with $x:A, y:B, z:C$. The sub-term $(xz)$ tells us $A=C \to D$. Since $y$ is applied to $(xz)$ we must have $B=D \to E$. Finally, $y(xz)$ is applied to $x$ so $E=A \to F$.
Let's summarise this.
$$(C \to D) \to (D \to (C \to D) \to F) \to C \to F$$
Renaming variables, and writing as a pre-typed λ-term we have
$$ λx: (α \to β).λy:(β \to (α \to β) \to \gamma).λz:α. y(xz)x $$
The type is
$$(α \to β) \to (β \to (α \to β) \to \gamma) \to α \to \gamma$$
