Can we abstract over kinds in $\lambda\underline{\omega}$?

Question

I am reading "Lambda Calculi with Types" by Henk Barendregt.

According to the definitions, $\lambda\underline{\omega}$ (types depending on types) allows us to assign types to type constructors such as $(\lambda \alpha : *. \alpha \to \alpha) : * \to *$ or $(\lambda \alpha : *. \lambda x : * \to *. x\alpha) : * \to (* \to *) \to * $. But the definitions are unclear whether something like this would be also be a valid term:

$(\lambda k: \square. k \to k) : \square \to \square$, where $\square$ is the sort of all kinds (a "kind constructor")

What about even higher order abstractions? The book doesn't even define "the sort of all sorts", but if I would define $\square_2$ such that $\square \to \square : \square_2$, $(\square \to \square) \to \square : \square_2$, etc, I could type even higher order abstractions such as:

$(\lambda k_2: \square_2. k_2 \to k_2) : \square_2 \to \square_2$

Is this valid in $\lambda\underline{\omega}$? (The $\omega$ in the name is what makes me believe it is) If not, is there an extension of $\lambda\underline{\omega}$ in which this is?

Answer 1

No, it isn't. The only terms of sort $\square$ in $\lambda\underline{\omega}$ are $*$ and $t_1 \to t_2$ where $t_1$ and $t_2$ are terms of sort $\square$. $\lambda k:\square.k$ is not a term of sort $\square$. In fact, you can easily formulate $\lambda\underline{\omega}$ without even talking about a sort $\square$.

It's trivial to add such terms if you want. Probably the easiest system to consider such thing is a Pure Type System aka generalized type systems introduced also by Barendregt in this paper I believe. You could allow $(\lambda k:\square. k \to k)$ by having sorts $\{*,\square,\square_2\}$, axioms $\{(*:\square),(\square:\square_2)\}$, and rules $\{(*,*),(\square,\square),(\square_2,\square_2)\}$. You can continue on in the obvious manner for higher and higher towers. You can go off in other directions too, not just a vertical tower. The generalized type systems paper referenced above gives examples of systems with a variety of other arrangements of sorts. You could also consider the "settings" described in Bart Jacobs' PhD thesis "Categorical Type Theory" which provides a bit more flexibility than Pure Type Systems.