What are cumulative universes and `* : *`?

Question

In Agda, there is Set n. As I understand, Set n extends the Haskell-style value-type-kind hierarchy to infinite levels. That is, Set 0 is the universe of normal types, Set 1 is the universe of normal kinds, Set 2 is the universe of normal sorts, etc.

In contrast, Idris has the so called "cumulative hierarchy of universes". It seems that for a < b, Type a: Type b, and universe levels are inferred. But what does it mean in real world programs? Can't we define something that only operate on some higher but not lower universe?

By the way, I know it's logically inconsistent, but what is * : * compared to the above consistent solutions?

Answer 1

Having * : * in Agda would correspond to Set n : Set n, at which point you'd probably just drop the levels and have just Set : Set, you can achieve this with the --type-in-type flag.

However you shouldn't really draw the parallel between Set 0, Set 1, Set 2 ... and types, kinds, sorts; because kinds in haskell carry the intuition that they are only relevant during typechecking while you can have perfectly valid runtime data which has a type in Set 1.

Cumulativity refers to the fact that Set n is a subtype of Set (n+1), so that if you define a type in Set 0 you can also use it where you need a Set 1 or Set 2. In Agda's standard library there is a Lift type in the module Level to achieve something similar but it does not work as nicely. It would make sense to add cumulativity to Agda.

Idris in addition has "typical ambiguity" where the universe levels are not apparent to the user but somehow the typechecker is supposed to check that you are not using universes in an inconsistent way.

What is implemented at the moment in Idris is not actually enough to rule out paradoxes: https://github.com/idris-lang/Idris-dev/issues/287

Coq however also allows you to omit universe levels in some situations and I believe they do not have known inconsistencies related to that.