Universe Polymorphism

Stream: Type theory

[Marcus Rossel]

How is universe polymorphism handled in Lean? I have some vague recollection of reading that Lean figures out which levels are needed for each universe polymorphic type and creates a version of the type for each required universe level. I'm guessing this would imply that universe polymorphism doesn't need to be a part of Lean's metatheory.
Is this correct?

[Chris Bailey]

Marcus Rossel said:

I have some vague recollection of reading that Lean figures out which levels are needed for each universe polymorphic type and creates a version of the type for each required universe level.

It doesn't do this, each kernel declaration has a field containing the level parameters, and downstream uses refer to the polymorphic version.

[Marcus Rossel]

@Chris Bailey Hm, I don't understand this yet, but I'm not exactly sure what to ask.
Does this mean that Lean kind of computes whether a given level "fits into" a polymorphic level downstream (sorry if this question makes no sense)?

[Reid Barton]

Top-level constants (i.e. definitions, axioms, etc.), and only top-level constants, have (zero or more) universe variables. Each use of a top-level constant instantiates it at particular values of those universe variables (which may themselves be universe variables of the surrounding definition, or more complicated universe expressions built from them).

[Chris Bailey]

Marcus Rossel said:

Chris Bailey Hm, I don't understand this yet, but I'm not exactly sure what to ask.
Does this mean that Lean kind of computes whether a given level "fits into" a polymorphic level downstream (sorry if this question makes no sense)?

Maybe a way to put it is that if you have a declaration with a universe variable, the thing that's in the environment is name := MyThing, universeParams := [u]. There isn't a MyThing [1], MyThing[2], MyThing[3] for each concrete use.
When you retrieve the declaration/constant from the environment you substitute the universes that are actually being used (e.g. https://github.com/leanprover/lean4/blob/bda871da25c72248e6958b32a153c27e2b73f5cb/src/kernel/type_checker.cpp#L84)

[Marcus Rossel]

Thanks, that really helped!

[Marcus Rossel]

I just found the source of my vague recollection:

Mario Carneiro said:

... when you write

universe u
constant a : Type u

you are really defining a parametric family of constants, denoted a.{u}. It's not like a exists in some particular universe u, rather there is a different a at each universe: a.{0} : Type 0, a.{1} : Type 1 and so on. This is the same way that the variables command works: every definition is implicitly universally quantified over variable declarations in scope, and when you use the definition later you can supply different values for the variables.

Universe parameters are usually implicit, so when you write #check a what it really means is #check a.{_}. Lean has to pick some universe variable to fill the _, and it makes up u_1 as a universe variable name. So the output is saying a.{u_1} : Type u_1, although the .{u_1} part is hidden unless you set set_option pp.universes true.

I'm guessing I misinterpreted the meaning of this explanation. But now I don't understand how it matches the explanation given by @Chris Bailey above.

[Reid Barton]

The environment only contains a single definition a, which is universe-polymorphic.

[Mario Carneiro]

Marcus Rossel said:

I'm guessing this would imply that universe polymorphism doesn't need to be a part of Lean's metatheory.
Is this correct?

Lean's metatheory needs to contain some amount of universe polymorphism since in actual practice we have to typecheck universe polymorphic definitions, but lean is a conservative extension of lean with no universe polymorphism (where all universe levels are concrete numerals). Each lean definition is a simple scheme over such theorems, and if you can prove a contradiction in lean then you can instantiate all the variables to 0 to obtain a contradiction in this fixed-universe version of lean. I actually develop this mapping in detail in #leantt

[Chris Bailey]

To give a concrete example of what I meant, if you have:

def exampleList : list punit.{2} := list.nil

There 's one standalone list declaration in the environment which is the universe polymorphic one name := list, uparams := [u], type := Π (T : Sort S(u)), (Sort S(u)), but when checking the above definition App (Const (list.nil, [S(0)]), Const (punit, [S(S(0))])), the inference step gets the type of list.nil by referencing the universe polymorphic version with type Π {T : Sort S(u)}, (App (Const (list, [u]), v0)), then subbing in the universes currently being used to get Π {T : Sort S(S(0))}, (App (Const (list, [S(0)]), Var0)).