Nats instead of Levels

Stream: lean4

[Adam Topaz]

@Matthew Ballard noticed something curious

universe u
variable (n m : Nat)
example : PUnit.{n} := .unit -- okay
example : PUnit.{m+n} := .unit -- fails
example : PUnit.{u+n} := .unit -- fails

Can someone explain what's going on? Note that all three would fail in lean3.

[Adam Topaz]

Specifically, I'm wondering what mechanism makes the first example work?

[Adam Topaz]

Even stranger

universe u
variable (α : Type u) (n : α)
set_option pp.universes true
example : PUnit.{n} := .unit

[Leonardo de Moura]

universe u
variable (n m : Nat)
def f1 : PUnit.{n} := .unit -- okay
#print f1 -- f is universe polymorphic (n is a universe level here).
-- The definition above is equivalent too
def f1'.{n} : PUnit.{n} := .unit -- okay

[Henrik Böving]

so n becomes autoImplicit-ed but as a universe parameter?

[Adam Topaz]

Aha, I see.

[Henrik Böving]

(obviously not real autoImplicit but conceptually)

[Adam Topaz]

I should have checked that this fails :)

set_option autoImplicit false

variable (n : Nat)
def foo : PUnit.{n} := .unit

Thanks!

[Arthur Adjedj]

The {m+n} examples fail because + expects a nat literal on the right-hand side, not a universe variable

[Adam Topaz]

Yeah, with the autoImplicit option off, everything is now clear.

[Henrik Böving]

I think it would be reasonable for autoImplicit to check this though right? This seems like something that is easily fixable but could trip people up

[Matthew Ballard]

What would need to be done to make this syntax work as “expected”?

[Adam Topaz]

Arthur Adjedj said:

The {m+n} examples fail because + expects a nat literal on the right-hand side, not a universe variable

To be precise, I think the + fails for the same reason as the following fails:

universe u v
example : PUnit.{u+v} := .unit

I.e. the operations allowed on universe levels are (i)max, and + numeral. I guess this is what you said, sorry for the noise.

[Henrik Böving]

Do not autoImplicit a universe parameter when there is already a variable bound with the same name I would say @Matthew Ballard

[Henrik Böving]

(and vice versa, dont autoImplicit an expression name when there is a universe level bound at the same name, but this should be rare since universe levels are rare)

[Matthew Ballard]

Sorry. I should be more clear. I was thinking Type.{u+ Nat.succ n} gives Type.{u + n +1}

[Matthew Ballard]

This goes back to discussions in #mathlib4 > !4#3463 universe constraint issues where in categorical contexts it is natural to require universe level inequalities as hypotheses.

[Henrik Böving]

Oh no not at all, universe levels in Lean are fully distinct from expressions. They are their own thing: docs4#Lean.Expr vs docs4#Lean.Level (well noot 100% as you can see, sorts contain levels, the point is that an expressioon cannnot appear as a level). What is happening in the above example is that Lean decided to introduce a universe parameter n distinct from the n : Nat so it seems like the Nat is acting as a universe parameter when this is in fact not the case. And my proposal to fix this UX issue would be: don't autoImplicit a universe parameter when there is an expr parameter of the same name already bound at the point

[Adam Topaz]

Henrik Böving said:

And my proposal to fix this UX issue would be: don't autoImplicit a universe parameter when there is an expr parameter of the same name already bound at the point

I think this is very reasonable.

[Matthew Ballard]

Yes I agree with that too

[Matthew Ballard]

What I was asking (poorly) was more a wish. If I wanted to try to parse Nat’s as universe levels, what would I need to do?

[Henrik Böving]

You can't, expressions are distinct from levels. if you have a (n : Nat) in scope you cannot make Lean understand that you want the same n to be a universe parameter. This is also reasonable I'd say. universe parameters (unlike n : Nat) do never get filled in at runtime, they always have to be resolved at compile time to a concrete universe.

[Matthew Ballard]

Is this only a code generation concern or does it extend beyond that?

[Henrik Böving]

In the code generator we don't really care about universe levels at all. universe levels only make sennse if you have a value x : Type u and since types are not code generation relevant they get erased ASAP in the code generation pipeline.

That being said I do not know why Lean enforces universe polymorphic code to always be resolved at compile time, someone else will have to shine a light at that.

[Henrik Böving]

Henrik Böving said:

You can't, expressions are distinct from levels. if you have a (n : Nat) in scope you cannot make Lean understand that you want the same n to be a universe parameter. This is also reasonable I'd say. universe parameters (unlike n : Nat) do never get filled in at runtime, they always have to be resolved at compile time to a concrete universe.

Maybe this paragraph makes more sense if I rephrase to "at type checking time"^^

[Gabriel Ebner]

While you can't go from Nat to level, you can to some degree go from level to Nat (see also the ToLevel type class in mathlib):

class LevelOf.{u} : Type u where levelOf : Nat
export LevelOf (levelOf)
instance : LevelOf.{0} where levelOf := 0
instance [LevelOf.{n}] : LevelOf.{n+1} where levelOf := levelOf.{n} + 1

#eval levelOf.{13} -- 13

[Gabriel Ebner]

(If you want to be surprised, try #eval levelOf)

[Henrik Böving]

Why is it that value?

[Gabriel Ebner]

Because of synthInstance.maxSize.

[Gabriel Ebner]

(I think it should rather fail than succeed when exceeding the limit though.)

[Henrik Böving]

Can you tell us why Lean does the "I want to resolve universe polymorphism" thing?^^

[Gabriel Ebner]

I'm not sure if I understand the question completely. Are you asking why levels are not first-class values. That's because it would be unsound, what universe would (i : Level) → Type i live in (it must be larger any of the levels you can pass into that function)?

[Adam Topaz]

Are universes first class values in agda, or am I misremembering something?

[Eric Rodriguez]

iirc the answer is it's complicated: you can make expressions like the one above, and they live in Type ω : Type ω_1 : Type ω_2..., but you can't parametrize over types in Type ω.

[Adam Topaz]

Aha, I see.

[Arthur Adjedj]

To be more clear, levels are represented as a type Level in Agda, which means that one may create a function toLevel : Nat -> Level. However, the Level type doesn’t have any elimination principle, so one cannot make a non-trivial function toNat : Level -> Nat for example. In practice, Levels are still handled in a special way during type-checking, to account for things like the commutativity of the max operator when checking equality between levels, but their lack of elimination principle means that they can easily be erased at runtime

[Mario Carneiro]

Gabriel Ebner said:

While you can't go from Nat to level, you can to some degree go from level to Nat (see also the ToLevel type class in mathlib):

class LevelOf.{u} : Type u where levelOf : Nat
export LevelOf (levelOf)
instance : LevelOf.{0} where levelOf := 0
instance [LevelOf.{n}] : LevelOf.{n+1} where levelOf := levelOf.{n} + 1

#eval levelOf.{13} -- 13

Actually you can also go the other way using a similar trick:

class ToLevel.{u} (n : Nat) : Type u
instance : ToLevel.{0} 0 := {}
instance [ToLevel.{n} n] : ToLevel.{n+1} (n + 1) := {}

def ToLevel.Out (n : Nat) [ToLevel.{u} n] : Sort u := PUnit
#check ToLevel.Out 13 -- ToLevel.Out 13 : Type 12

(It's hard to write a function which returns a universe level so this one returns a value whose type is Sort u where u is the output)

[Henrik Böving]

Adam Topaz said:

Henrik Böving said:

And my proposal to fix this UX issue would be: don't autoImplicit a universe parameter when there is an expr parameter of the same name already bound at the point

I think this is very reasonable.

I spent a few minutes digging and I believe this would be the correct location to insert: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Level.lean#L76 but LevelElabM does not have the currently bound term variables in its context yet so one would have to slightly refactor that to include such a thing as well. Then it should be possible to efficiently do this.

[Sebastian Ullrich]

This looks like a pretty rare edge case to guard against in core; variables of different kinds inhabiting different namespaces is also not unusual in programming languages. If someone was sufficiently motivated, this could be flagged by a custom linter.

[Eric Wieser]

Are there any other programming languages with autoImplicit behavior?

[Alex Keizer]

I think Haskell does, for types at least. I don't know of any lang that has autoImplicit behaviours across different namespaces.