[TYPES] Transfinite universe levels

[Gabriel Scherer]

There are several reasons to be interested in universe hierarchies, among
which (1) the question of the ordinal strength of the resulting type
theory, (2) the ability to reflect a fragment of the type theory of
interest into itself to study it internally, and (3) usability questions
arising from the inconvenience, in practice, of predicative universes.
Erik's answer gives a lot of information on (1) and (2), but I have a
comment on (3).

If I understand correctly, Agda today has a finite hierarchy of universes
that are types, and a Set-omega sort (that is not a type) to classify
universe-polymorphic declarations. It is natural to think of extending this
hierarchy with sorts (omega+n) (making Set-omega a type), and then one
would extend quantification on universe levels to something of the form
(forall (i < l)) for an ordinal level l.
However, my intuition would be that this does not deliver much usability
benefits in practice. We use universe-polymorphic definitions to get
genericity (from a programming point of view, we think of it as
SystemF-style impredicative quantification), and then sometimes we find
that we cannot compose two generic things as it would require going above
Set-omega. But in practice with a transfinite hierarchy you would likely
run into the same trouble: if two independent generic definitions quantify
in the strongest possible way, they clash, and otherwise one can be used
under the other but not conversely. When you develop in the large, you
would still need to synchronize universe constraints among the various
libraries to compose them in the way you intend; in fact, it is likely that
in practice you could (given a coherent policy for universe numbering among
the libraries of your development) lift that back to finite universes
equipped with finite bounded quantification.

For this reason, I have generally considered that extending the ordinal
hierarchy you have access to isn't actually so important. If you don't ask
for ordinals that are very strong (say, if you are happy with the
m*omega+k, or below epsilon0), my understanding is that the metatheory
would not be harder than it is today with finite universes and universe
quantification, but the usability of the resulting system also wouldn't be
very different.

On Tue, Jul 10, 2018 at 11:00 PM Stefan Monnier <monnier at iro.umontreal.ca>
wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
>
> Most type theory-based tools nowadays are based on a calculus with an
> infinite hierarchy of predicative universes.  Some of them, such as
> Agda, also allow abstraction over those levels, so we end up with a PTS
> along the lines of:
>
>     ℓ ::= z | s ℓ | ℓ₁ ∪ ℓ₂ | l      (where `l` is a level variable)
>
>     S = { Type ℓ, Type ω, SortLevel }
>     A = { Type ℓ : Type (ℓ + 1), TypeLevel : SortLevel }
>     R = { (Type ℓ₁, Type ℓ₂, Type (ℓ₁ ∪ ℓ₂)),
>           (SortLevel, Type ℓ, Type ω),
>           (SortLevel, Type ω, Type ω) }
>
> I was wondering if there's been work to push this to larger ordinals, to
> allow maybe rules like
>
>           (Type ω, Type ω, Type (ω·ω))
>
> I.e. "deep universe polymorphism"
>
>
>         Stefan
>