Exercise 2.12
(a) Construct a term of type $((α →β) →α) →(α →α →β) →α$
(b) Construct a term of type $((α →β) →α) →(α →α →β) →β$
(a) The term takes two arguments, so let's set $x:((α →β) →α)$ and $y:(α →α →β)$.
We can't apply $x$ to $y$ or vice versa, so we'll construct $z:α$.
This gives us $yz : α→β$, and so $yzz:β$. This means $λz:α.yzz : α→β$. Finally, $x(λz:α.yzz): α$, as desired.
An abstraction with $y$ then $x$ gives us the required term.
$$ λx:((α →β) →α) . λy: (α →α →β) . x(λz:α. yzz) : ((α →β) →α) →(α →α →β) →α $$
(b) The term take the same two arguments, so again let's set $x:((α →β) →α)$ and $y:(α →α →β)$.
We'll use the previous result that $x(λz:α.yzz): α$.
Applying $y$ to two of these expressions gives us $y (x(λz:α.yzz)) (x(λz:α.yzz)) : β$, the desired type.
Again, abstracting with $y$ then $x$, gives us the required term.
$$ λx:((α →β) →α) . λy: (α →α →β) . y (x(λz:α.yzz)) (x(λz:α.yzz)) : ((α →β) →α) →(α →α →β) →β$$
