values, types, kinds,... as an infinite sequence?

Question

I'm only beginning to become familiar with the concept of kinds, so bear with me if I am not formulating my questions well...

Values have Types:

3 :: Int
[1,2,3] :: [Int]
('c',True) :: (Char,Bool)

Types have Kinds:

the type 'Int' has kind *
the type '[Int]' also has kind *
   but the type constructor [] has kind * -> *
similarly, the type (Char,Bool) has kind  *
   but the type constructor (,) has kind * -> * -> *

What do Kinds have?

Do they kinds have ilk, or genres, or breeds, or varieties?

How far does this sequence of abstraction go? Do we stop because we run out of words, or do we stop because going farther has no value? Or, perhaps, because we quickly reach the limits of human cognition and just can't wrap our heads around higher-genred kinds?

A related question: languages give us value-constructors (like a cons operator) to make values. Languages also give us type-constructors like (,) or [] to make types. Are there any languages that expose kind-constructors to make kinds?

Another edge case that I'm curious about: We apparently have a type that has no value, denoted as ⊥, called "the bottom type". Is there a kind that has no type: a bottom kind?

Answer 1

The terminology type and kind does not scale well. Type theorists since Bertrand Russell have used a hierarchy of "types." One version of this has that Integer : Type 0, Type 0 : Type 1, Type 1 : Type 2, ..., Type n : Type (n+1), .... In dependently typed languages like Coq and Agda, one frequently needs these "higher sorts."

Levels like this are helpful for avoiding Russell's paradox. Using Type : Type tends to cause contradiction (see Quine for alternative designs).

This use of numbers is the standard notation when we need it. Some type theories have a notion of "cumulative kinds", "cumulative levels" or "cumulative sorts" which says "if t : Type n then also t : Type (n+1)".

Cumulative levels + "level polymorphism" give a theory almost as flexible as Type : Type, but avoids paradoxes. Coq makes the levels implicit mostly, although the sorts Set and Prop are both typed Type, Type {1} : Type {2}. That is, you don't usually see the numbers, and most of the time it just works.

Agda has a language pragma which provides level polymorphism, and makes things very flexible, but can be slightly bureaucratic (Agda is however usually less "bureaucratic" than Coq in other areas).

Another good word is "universe."

Answer 2

You should probably read Tim Sheard's paper about Omega, a dialect of Haskell with an infinite tower of types/kinds/sorts, but without full-blown dependent types. It explains why you'd want this, and mentions that the levels above "sort" are in practice (at least so far) not directly used very much.