Exercise 3.10
Let $M ≡ λx : (Πα : ∗. α →α) . x(σ →σ)(xσ)$.
(a) Prove that $M$ is legal in λ2.
(b) Find a term $N$ such that $M N$ is legal in λ2 and may be considered to be a proper way of adding type information to $(λx. xx)(λy. y)$.
(a) To show $M$ is legal in λ2 we need to find a context such that $M$ has a type. The following derivation does this.
In the context $Γ \equiv σ:*$, the term $M$ has a type $(\Pi \alpha: * . (\alpha \to \alpha)) \to \sigma \to \sigma$, so $M$ is legal.
(b) Looking at the definition of $M$, we can see it takes an argument with type $(Πα : ∗. α →α)$. We can try a simple form for $N$, that is
$$N \equiv λα:*.λy:α.y$$
In fact section 3.8 of the textbook tells us this is the only closed term of that type. Furthermore, it corresponds to the sub-term $(λy. y)$ of the term we want to type.
Let's check that applying $M$ to $N$ does result in type $σ →σ$ as expected from the type of $M$.
$$\begin{align} M N & \equiv ( λx : (Πα : ∗. α →α) . x(σ →σ)(xσ) ) \; (λα:*.λy:α.y) \; : \; σ →σ \\ \\ &\to_β (λα:*.λy:α.y) (σ →σ) \; ((λα:*.λy:α.y)σ) \; : \; σ →σ \\ \\ &\to_β (λy:σ →σ.y)(λy:σ.y) \; : \; σ →σ \\ \\ &\to_β λy:σ.y \; : \; σ →σ \end{align}$$
$MN$ is legal because it has a type $σ →σ$ in the context $Γ \equiv σ:*$.
This $MN$ is a proper way of adding type information to $(λx. xx)(λy. y)$, as the following shows.
$$ σ:* \; ⊢\; (λx: (Πα : ∗. α →α) . x(σ →σ)(xσ))(λy:σ. y) \; : \; σ →σ$$
