Exercise 2.5
For each of the following terms, try to find a pre-typed variant which is typable. If this is not possible, show why.
(a) $λxy. x(λz. y)y$
(b) $λxy. x(λz. x)y$
(a) Let's try to work out the types for $λxy. x(λz. y)y$.
We start with the bound variables $x:A, y:B, z:C$.
The type of $(λz. y)$ is $C \to B$, and since $x$ is applied to it, we must have $A = (C \to B) \to D$. Finally, since $x(λz. y)$ is applied to $y$, we have $D = B \to E$.
Summarising we have
$$ λxy. x(λz. y)y : ((C \to B) \to B \to E) \to B \to E$$
Renaming variables, and writing as a pre-typed λ-term, we have
$$ λx:((\gamma \to β) \to β \to ρ).λy:β. x(λz:\gamma. y)y$$
(b) Let's try to work out the types for $λxy. x(λz. x)y$.
We start with the bound variables $x:A, y:B, z:C$.
The type of $(λz. x)$ is $C \to A$, and since $x$ is applied to it, this leads to $A = (C \to A)$, which is impossible.
So $λxy. x(λz. x)y$ is not typable.
