Exercise 2.1
Investigate for each of the following λ-terms whether they can be typed with a simple type. If so, give a type for the term and the corresponding types for $x$ and $y$. If not, explain why.
(a) $xxy$
(b) $xyy$
(c) $xyx$
(d) $x(xy)$
(e) $x(yx)$
(a) Let's clarify $xxy$ as $(xx)y$.
We know from Example 2.2.26(3) that $xx$ can't be typed. The reason is that if the type of the second $x$ is $A$, then the type of the first $x$ must be $A \to B$, and these two can't be unified.
So $xxy$ can't be simply typed.
(b) Let's clarify $xyy$ as $(xy)y$.
If the type of the second $y$ is $A$, then the type of $(xy)$ must be $A \to B$.
If the type of the first $y$ is $C$, then the type of $x$ must be $C \to D$.
Unifying, we have $A = C$ and $D = A \to B$.
So the types are:
$$\begin{align} y &: A \\ \\ x &: A \to (A \to B) \\ \\ xyy &: B \end{align}$$
(c) Let's clarify $xyx$ as $(xy)x$.
If the type of the second $x$ is $A$, then the type of $(xy)$ must be $A \to C$.
If the type of $y$ is $B$, then the type of the first $x$ must be $B \to D$.
Unifying, we have $A = B \to D$, and $D = A \to C$.
We can't resolve these to simple types because, for example, the type $A$ is infinitely self-referential. That is,
$$\begin{align} A &= B \to D \\ \\ & = B \to (A \to C) \\ \\ & = B \to ((B \to D) \to C) \\ \\ & = B \to ((B \to (A \to C)) \to C) \\ \\ & = \ldots \end{align}$$
So $xyx$ can't be simply typed.
(d) The term $x(xy)$ is already parenthesised.
If the type of $y$ is $B$, then the the type of the second $x$ must be $B \to C$.
That means the type of $(xy)$ is $C$.
Which means the type of the first $x$ must be $C \to D$.
Unifying, we have $B = C = D$.
So the types are:
$$\begin{align} y &: B \\ \\ x &: (B \to B) \\ \\ x(xy) &: B \end{align}$$
(e) The term $x(yx)$ is already parenthesised.
If the type of the second $x$ is $A$, then the type of $y$ is $A \to C$.
This means the type of $(yx)$ is $C$.
The type of the first $x$ must then be $C \to D$.
Unifying, we have $A =C \to D$.
So the types are:
$$\begin{align} x &: C \to D \\ \\ y &: (C \to D) \to C \\ \\ x(yx) &: D \end{align}$$
