In Agda, why is universe polymorphism explicit?

Question

I've noticed that the process of coding a definition in Agda that is universe polymorphic usually requires little thought in how the Level parameters are specified. Most of the time in the input you can just use a different Level term for each place where it's applicable, and in the the output use the ⊔ and occasionally the lsuc of all previous Level terms if it's needed.

This often results in the universe polymorphic versions of definitions having boilerplate code tacked on, such as in the following example with the definition of dependent pair types.

open import Agda.Primitive public

-- Non-universe polymorphic example
data Σ (A : Set)(B : A → Set) : Set where
    pair : (x : A) → B x → Σ A B

-- Universe polymorphic example
data Σ' {i j : Level}(A : Set i)(B : A → Set j) : Set (i ⊔ j) where
    pair : (x : A) → B x → Σ' A B

Why is it not the case that whenever we write Set, Agda implicitly handles the universe polymorphism for us so we don't have to manually specify these Level terms? What benefits does this provide?

Answer 1

First of all, you may simplify your code with the ∀ keyword:

data Σ' ∀ {i} {j} (A : Set i) (B : A → Set j) : Set (i ⊔ j) where
    pair : (x : A) → B x → Σ' A B

You may also make use of the variable feature to omit the {i j} part, making it completely implicit: https://agda.readthedocs.io/en/v2.6.2.1/language/generalization-of-declared-variables.html#overview the first example contains an implicitized level.

Now, why is this necessary? It seems historical, but there are some good reasons (I'm not the person who made the decisions. I'm just explaining from my own POV). Consider the following signatures:

f : {A : Set i} {B : Set i} -> Bla
f : {A : Set i} {B : Set j} -> Bla

If levels are implicit, which one would f : {A : Set} {B : Set} desugar to? Both seem fine, but we have to make a choice. However, since both seem fine, users will have to guess.

The other benefit of explicit levels is that you may apply a level argument using the syntax of function application, where you can use some convenient sugars like f {i = lzero} or something.

Nowadays, people realized in most cases we don't even care about that. For instance, Lean and Arend have a default behavior for implicit universe polymorphism, with a special syntax for explicit cases. This syntax seems much better for traditional style universe polymorphism.

Answer 2

In Agda, universe levels are not only explicit but they are also first class. This means that you can store them in data structures and compute with them. This allows you to write generic programs in Agda's userland where you would have to resort to a meta-language in other proof assistants.

I present some of these constructions in Generic Level Polymorphic N-ary Functions.