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

Solution 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."

Solution 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.