Why an infinite type hierarchy?

Question

Coq, Agda, and Idris have an infinite type hierarchy (Type 1 : Type 2 : Type 3 : ...). But why not do it instead like λC, the system in the lambda cube that's closest to the calculus of constructions, which has only two sorts, $*$ and $◽$, and these rules?

$$\frac {} {∅ ⊢ * : ◽}$$

$$\frac {Γ ⊢ T _ 1 : s _ 1 \qquad Γ, \: x : T _ 1 ⊢ t : T _ 2} {Γ ⊢ (λ \: x : T _ 1, \: t) : (Π \: x : T _ 1, \: T _ 2)}$$

$$\frac {Γ ⊢ T _ 1 : s _ 1 \qquad Γ, \: x : T _ 1 ⊢ T _ 2 : s _ 2} {Γ ⊢ (Π \: x : T _ 1, \: T _ 2) : s _ 2}$$

This seems simpler. Does this system have important limitations?

Answer 1

Actually, the approach of the CoC is more expressive -- it permits arbitrary impredicative quantification. For example, the type $\forall a.\; a \to a$ can be instantiated with itself to get $(\forall a.\; a \to a) \to (\forall a.\; a \to a)$, which is not possible with a universe hierarchy.

The reason it is not widely used is because impredicative quantification is incompatible with classical logic. If you have it, you cannot give a model of type theory where types are interpreted as sets in the naive way --- see John Reynolds's famous paper Polymorphism is Not Set-theoretic.

Since many people want to use type theory as a way to machine-check ordinary mathematical proofs, they are generally unenthusiastic about type-theoretic features which are incompatible with the usual foundations. In fact, Coq originally supported impredicativity, but they have steadily abandoned it.

Answer 2

I'll compliment Neel's (excellent, as usual) answer with a bit more exposition on why levels are used in practice.

The first important limitation of CoC is that it is trivial! A surprising observation is that there is no type for which you can prove that it has more than one element, much less an infinite number of them. Adding just 2 universes gives you the natural numbers with provably infinitely many elements, and all "simple" datatypes.

The second limitation is the computation rules: CoC only supports iteration, i.e. the recusive functions do not have access to the sub-terms of their arguments. For this reason, it is more convenient to add inductive types as a primitive construction, giving rise to the CIC. But now another problem arises: the most natural induction rule (called elimination in this context) is inconsistent with the Excluded Middle! These problems don't appear if you restrict the induction rule to predicative types with universes.

In conclusion, it appears that CoC has neither the expressiveness nor the robustness wrt consistency that you would like in a foundational system. Adding universes solves many of these problems.