Exercise 2.11
Find inhabitants of the following types in the empty context, by giving appropriate derivations.
(a) $(α →α →γ) →α →β →γ$
(b) $((α →γ) →α) →(α →γ) →β →γ$
(a) The term takes 3 arguments so let's start with $x:α →α →γ, y:α, z:β$.
We can immediately see that $x$ takes arguments of type $α$ twice we can construct $xyy:γ$. The third argument $z:β$ is taken but ignored. So we have the following.
$$ λx:α →α →γ . λy:α . λz:β . xyy : (α →α →γ) →α →β →γ $$
The following flag notation derivation confirms the inhabitant has the given type.
(b) Again the term takes 3 arguments so let's start with $x:((α →γ) →α) , y:(α→β), z:β$.
We can see that $x$ takes an argument of type $(α→γ)$, and $y$ is for this type. We can construct $xy:α$. Since $y$ takes an argument of type $α$ and returns a type $γ$, means we can further construct $y(xy):γ$. The third argument $z:β$ is taken but ignored. So we have the following.
$$ λx:(α →γ) →α . λy:α→γ . λz:β . y(xy) : ((α →γ) →α ) →(α→β) →β →γ $$
The following flag notation derivation confirms the inhabitant has the given type.
