How high up do kinds go in type theory?

Question

I understand this is a bit naive, but I just learned how types can have types that we call 'kinds,' in system F$\omega$ as a sort of extended higher order lambda calculus. The wiki article on it suggests it's a lambda calculus 'one level up.' but didn't mention anything about extending kinds to higher order kinds.

I got to wondering if kinds can have 'superkinds' of their own. Is there an ascending ladder in type theory of higher order kinds? Can we have 'dependent kinds?' where kinds are dependent on types? Or kind quantification? Can we keep on extending this ladder higher for ever higher order types? Can we have subkinds, inductive kinds, and coinductive kinds the way we have subtypes, inductive types, and coinductive types, and so on up the ladder of higher and higher order types? Is there a good reference for this sort of transfinite induction (if that's the right term) in type theory?

Answer 1

You might want to look at the notion of a pure type system (PTS). A PTS is built from the following datum:

1. A set ${\mathscr S}$ of sorts, which intuitively correspond to the different layers of types, kinds, higher order kinds, ...
2. A set ${\mathscr A}\subset{\mathscr S}^2$ of axioms: $(s_0,s_1)\in{\mathscr A}$ signifies that $s_0$ itself is a type of sort $s_1$.
3. A ternary relation ${\mathscr R}\subseteq{\mathscr S}^3$ of rules, specifying the way dependent product types can be built: $(s_0,s_1,s_2)\in{\mathscr R}$ signifies that the type system should allow the formation of dependent product types for those dependent types for which the parameter type has sort $s_0$ and the argument type has sort $s_1$, and that the resulting dependent product type itself should have sort $s_2$.

For example, if you take ${\mathscr S} := \{\ast\}$, ${\mathscr A} := \emptyset$ and ${\mathscr R} := \{(\ast,\ast,\ast)\}$, you have a single sort of types, and you may form dependent product types for types depending on terms. In particular, function types like $A\to \ast$ do not exist (since $\ast$ is not a type, i.e. has no sort), so that a posteriori the only dependent product types one may form are those corresponding to constant dependent types, i.e. ordinary function types $A\to B$ for types $A,B$. In other words, you get the ordinary typed $\lambda$-calculus.

However, you might include a sort $\square$ and force $\ast:\square$ by putting $(\ast,\square)\in{\mathscr A}$. Then, the rule $(\ast,\square,\square)$ would allow for the formation of dependent product types $A \to \ast:\square$ for $A$ a type of sort $\ast$, and for such a dependent type $V:A\to\ast$, you might indeed form its dependent product type $\prod_{x:A} V x: \ast$ from the rule $(\ast,\ast,\ast)$. The resulting system is $\lambda\text{P}$.

To implement 'terms depending on types' like the Church naturals $\prod_{X:\ast} X\to (X\to X)\to X:\ast$ you would need the rule $(\square,\ast,\ast)$ (giving System $F$), and to form 'types depending on types' you'd need to include the rule $(\square,\square,\square)$ (giving $\lambda_\omega$).

The 8 possible combinations of the above rules gives the so called $\lambda$-cube of pure type sytems, at the top of which you have the calculus of constructions. However, you can also have an infinite ladder of sorts, as in the calculus of inductive constructions. Finally, note that the 'paradise' configuration with ${\mathscr S} := \{\ast\}$, ${\mathscr A}:=\{(\ast,\ast)\}$ and ${\mathscr R} := \{(\ast,\ast,\ast)\}$ yields an inconsistent system. See e.g. nlab or these slides