AFAIK, a hierarchy of type universe(Type^0: Type^1: Type^2: ...) was introduced to avoid inconsistency caused by Type: Type.

But some functional language(e.g. Idris) also allows subtyping of these type universes(x: Type^n then also x: Type^n+1). From my understanding, this is not mandatory to solve the inconsistency. So it leads me to guess there should be some advantages from this redundant subtyping rule.

When is cumulative type universes useful?

  • 1
    $\begingroup$ You are misusing the terminology. What you describe in the first paragraph is a hierarchy of universes which is not cummulative. The one in the second paragraph is cummulative. $\endgroup$ – Andrej Bauer Feb 9 '20 at 17:54

Without cummulative universes, if you have $A : \mathsf{Type}_3$ then you do not have $A : \mathsf{Type}_7$. Instead, we also have to introduce lifting functions $\iota_{i,j} : \mathsf{Type}_i \to \mathsf{Type}_j$ for all $i \leq j$ and write $\iota_{3,7}(A)$ to port $A$ from the third universe to the seventh one. But this is not all, we also want to know whether $\iota_{3,5}(\iota_{5,7}(A)) = \iota_{3,7}(A)$, i.e., can we lift in several steps? So we need to add a bunch of equations $\iota_{i,j}(\iota_{j,k}(A)) = \iota_{i,k}(A)$ for $i \leq j \leq k$. And this is not all, we also need things like $\iota_{i,i}(A) = A$ and $\iota_{i,j}(\Pi(x : A), B(x)) = \Pi (x : A) \iota_{i,j}(B(x))$, and on and on. It's all very annoying.

With cummulative universes we can just drop all the lifting functions $\iota_{i,j}$.

So why would anyone reject cummulative universes? There are several reasons. An important one is that with cummulative universe it is not true that every expression has at most one type, since a type is an element of many universes. This complicates various algorithms for inferring and checking types. Another reason is semantic: there are interesting models of type theory in which universes are not cummulative.

  • $\begingroup$ Thank you for the answers From my understanding, both of you are pointing out that the cumulative universe gives the simpler underlying theory by eliminating lifting rules. I think my question was misleading. I was asking about the advantage of programming. At first, I expected some functions that are polymorphic over universes which only can be defined with the cumulative universe. $\endgroup$ – heartpie2 Feb 18 '20 at 2:29
  • $\begingroup$ Then I saw id id example, and I learned that with or w/o universe subtyping I need to introduce shifting to solve the problem. It makes me suspicious of the existence of that sort of function and advantage in programming. Am I expecting something wrong? $\endgroup$ – heartpie2 Feb 18 '20 at 2:29

Suppose you have X : Type0. What universe can X -> Type0 go in?

It can't go in Type0, because Type0 : Type0 doesn't hold. Universes are presumably closed under function types, so we'd hope it can go in Type1 because Type0 : Type1. But without the subtyping rule, we don't know that X : Type1, we only know that it is in Type0.

Now, you could instead say that Type1 has function types for things in Type0 and Type1. But you also need to do this for all the other ways to build up types, so you'd have a lot of extra rules, unless you came up a similarly generic rule to the subtyping rule. You'll only need more the higher you go. And you still might just need a way to include a type from a lower universe to a higher one (this happens in Agda, for instance, and is defined using a data type called Lift).

Having cumulativity of universes is generally the simplest way to handle this issue.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.