What are cumulative universes and `* : *`?

10
votes

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?

1
functional-programmingtype-systemsagdadependent-typeidris
Universes are not inferred in Idris: Idris constructs a graph and checks whether it is acyclic. With * : * you never need to write out levels (I'm quite tired writing stuff like ∀ {α₁ α₂ α₃ β₁ β₂ β₃ γ₁ γ₂ γ₃} {C₁ : Category α₁ β₁ γ₁} {C₂ : Category α₂ β₂ γ₂} {C₃ : Category α₃ β₃ γ₃} instead of ∀ {C₁ C₂ C₃}), in Agda records can't contain properly universe polymorphic functions, which is very annoying, HList must be rewritten as a function instead of a data, you can't compose some functions because of the Setω error and so on. I.e. * : * is very convenient. – user3237465
Of what does Idris construct a graph? I've seen this kind of information before but I can't understand because I'm too bad at data structures and algorithms. – 盛安安
Nodes are levels, edges are (<). I.e. you can't have l1 < l2 and l2 < l1, because this would result in l1 < l1, which means Type l1 : Type l1. – user3237465

1 Answers

7
votes

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.