3
$\begingroup$

I've followed the tutorial on Checking Dependent Types with Normalization by Evaluation: A Tutorial by David Christiansen, where we implement a small dependently typed kernel with the axiom Univ : Univ. The "Projects" section of the tutorial provides a project on replacing this with a universe hieararchy:

7.Replace U with an infinite number of universes and a cumulativity relation. To do this, type equality checks should be replaced by a subsumption check, where each type constructor has variance rules similar to other systems with subtyping.

I've looked around a little, and it seems like both Agda and Lean implement a universe hierarchy using levels, which have the following operations:

lzero : Level
lsuc  : (n : Level) → Level
_⊔_   : (n m : Level) → Level
  1. Who came up with this encoding of universes based on levels originally? Why not simply reuse the natural numbers for universe levels? There must be some reason to introduce a new Level type, instead of reusing the already present Nat?
  2. How does one type-check and perform normalization-by-evaluation on universe levels?
  3. What are the subtleties one should be aware of when implementing universes?
  4. How should I test that my universe hierarchy implementation is correct? Are there short, well-known theorems that depend on a universe hierarchy, which I should try to encode?

I am hesitant to try my hand at naively implementing universes based on my intuition, because all the references I have read (ATAPL, MiniTT, and the above tutorial) all stop short of explaining universe levels. I get the feeling that there is non-triviality which I am unable to see, and thus would like to know how to (a) implement, and (b) test universes, on top of the kernel I now have

$\endgroup$
3
  • 1
    $\begingroup$ Coq reference $\endgroup$ – ice1000 May 19 at 7:16
  • $\begingroup$ @ice1000 Thanks for the link! The abstract says "However, the structure and hierarchy of universes is more complex than bare polymorphic type variables.". In what sense is it more complex? This is in some sense the source of my confusion; I don't see why universes are subtle. $\endgroup$ – Siddharth Bhat May 19 at 7:24
  • 1
    $\begingroup$ I wrote an answer (: $\endgroup$ – ice1000 May 19 at 7:35
1
$\begingroup$

IMHO universe hierarchy is particularly complicated to implement while the benefit is very small. It complicates programming in the language and the implementation of the language. The only benefit is to ensure the logical consistency. I guess that's why everybody is not writing about it.

Here are some answers to your questions. I don't know much type theory -- I can't answer everything, sorry.

Why not simply reuse the natural numbers for universe levels?

Nat has an eliminator. You shouldn't be able to pattern match on a level. In fact, introducing Level as a type (not to mention an inductive type) already causes problem. Imagine the following function:

Ty : (ell : Level) -> Set (lsuc ell)
Ty l = Set l

What is the universe level of the type of Ty? Also, what's the universe level of the type of Level? If we don't have a type for levels (but instead built it into the syntax, to eliminate these cases) we could avoid these problems (but then you become less flexible ofc).

How does one type-check and perform normalization-by-evaluation on universe levels?

I guess just like Nat. The relevant operations are strict subset of Nat.

What are the subtleties one should be aware of when implementing universes?

  1. Level is actually not a type. I personally don't like Agda's approach (but prefer Lean's, Arend's approach, where Level is not a type).
  2. You need to compare levels for equality and less than relation. So, your compiler should know max(x, y) >= x, max(x, y, z) >= max(x, y), etc.
  3. There are many styles of universe hierarchy. You can peek cumulativity, impredicativity (be careful, it may lead to inconsistency), typical ambiguity, etc.
  4. You may want to implement a solver for level equations (if you have implicit inference mechanism), but that's very complicated.

How should I test that my universe hierarchy implementation is correct?

Try to refute the construction of the Girard paradox. It's everywhere on the internet. Also, there is another example which I believe that it won't work with universe levels.

I'm also implementing universe polymorphism on a little programming language, but the code is kinda messy.

$\endgroup$
3
  • 1
    $\begingroup$ One benefit of a consistent universe hierarchy I want to mention is that you can erase proofs. $\endgroup$ – Labbekak May 19 at 20:13
  • 1
    $\begingroup$ I think you can do that even without universe hierarchy, no? Idris2 now has type-in-type but it has a lot of erasure $\endgroup$ – ice1000 May 20 at 1:11
  • 1
    $\begingroup$ No if you erase proofs with type-in-type your language is no longer type-safe, because you can inhabit any proof A = B with an infinite loop and cast any (unrelated) A to a B. You have to evaluate the proof in order to be type-safe, because then the program would run forever, but at least not cast A to B. Please see stackoverflow.com/questions/61930740/… $\endgroup$ – Labbekak May 20 at 6:49

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.