Exercise 5.4
Prove that * is the only legal kind in λP.
The set of kinds $\mathbb{K}$ is defined as
$$\mathbb{K} = * \; | \; \mathbb{K} \to \mathbb{K}$$
The textbook gives examples of kinds
$$∗, \; ∗→∗, \; ∗→∗→∗, \; (∗→∗) →∗, \; (∗→∗) →∗→∗, \; ∗→(∗→∗) →∗$$
For a kind $k$ to be legal, there must exist a context $Γ$ and type $t$ such that $Γ⊢k:t$.
All judgements are a result of the derivation rules for λP, given in Figure 5.1, so we can examine them to see how a judgement of the form $Γ⊢k:t$ can be derived.
The axiomatic (sort) rule $\emptyset \vdash *:\Box$ immediately tells us that * is a legal kind.
Using the definition of kinds, aside from *, all other kinds are arrow types of the form $\mathbb{K} \to \mathbb{K}$. All of them are derived from the simplest $* \to *$. If we can show that $* \to *$ is not derivable, then we have shown all the other kinds (except *) are not derivable.
The type $* \to *$ is only derived by the (form) rule. Note that $* \to *$ is an abbreviation of $\Pi x:*.*$.
$$(form) \quad \frac{Γ ⊢ A:* \qquad Γ, x:A ⊢ B:s}{Γ ⊢ \Pi x:A.B:s} \quad x \notin Γ$$
To form $\Pi x:*.*$, we must have $A=*$ and $B=*$. The first premise would then require $*:*$.
There is no derivation rule that results in $Γ ⊢*:*$, and so kinds aside from * are not derivable in λP.
