Task 26: Replace Type u by Type* wherever possible

Stream: mathlib4

[Martin Dvořák]

Claiming task 26.

[Jovan Gerbscheid]

I think the difference is that Type* introduces a fresh universe, while in Type _, the level can be inferred by unification (or be fresh if it isn't unified to be anything else).

But there might still be instances in Mathlib where this replacement is possible.

[Notification Bot]

A message was moved here from #mathlib4 > Call for help: technical/ organisational debt by Yaël Dillies.

[Matthew Ballard]

Re 26: I would be very very careful with this. We have been encountering significant still-unidentified slowdowns that depend on the choice of universe name.

Re 27: I would replace Type _

• first by Type* if possible
• second by Type whatever where whatever is the universe level it actually unifies to.

[Ruben Van de Velde]

I would not replace Type _ at all in cases where Type* doesn't work

[Edward van de Meent]

actually, i think that Type _ happens precisely because arguments have Type*, since you don't get to refer to the universe variable created?
for example:

def Foo {A : Type*} (s:Set A) : Type _ := s

[Matthew Ballard]

There has been at least one case where Type _ really meant Type 0 (oops). I don't like the obfuscation if it can reasonably be avoided but it is not high up my priority list.

[Martin Dvořák]

Matthew Ballard said:

Re 26: I would be very very careful with this. We have been encountering significant still-unidentified slowdowns that depend on the choice of universe name.

I believe readability is more important than compilation speed (having one more variable in the context increases the cognitive load for readers); however, we will benchmark the PR to check it isn't too bad.

[Matthew Ballard]

Please be aware of #12737 and request my review

[Jovan Gerbscheid]

My understanding is that #12737 tracks slowdowns caused by universe metavariables. But Type* (unlike Type _) introduces a fresh universe parameter, not a metavariable. So I think going from Type u to Type* isn't bad for performance

[Martin Dvořák]

WIP part 1 (Algebra without category theory): #24285

[Junyan Xu]

Is there any automation to replace (R : Type*) (S : Type*) (M : Type*) by (R S M : Type*) and {R : Type*} {A : Type*} by {R A : Type*}, etc.?

[Martin Dvořák]

I guess you could write a regex for the basic cases.

[Yaël Dillies]

Not that I know of, but I have many times wished there was!

[Martin Dvořák]

I suggest not to do it in this PR (because of the way diffs are visualized).

[Yury G. Kudryashov]

Also note that

• category theory relies on a specific order of universe variables, so that Category.{u} C means "category with morphisms in Type u";
• definitions and theorems about docs#ULift should use the same order of universe arguments as ULift does (this is not always the case at the moment), for similar reasons.

[Matthew Ballard]

Jovan Gerbscheid said:

My understanding is that #12737 tracks slowdowns caused by universe metavariables. But Type* (unlike Type _) introduces a fresh universe parameter, not a metavariable. So I think going from Type u to Type* isn't bad for performance

Yes that is a reasonable belief but see #PR reviews > #21099 use unification hints for generators normalization of levels includes sorting of names which, last I checked, behaves unexpectedly for names with more than one part or more generally outside of ASCII. If anyone has more time to track down the offending code in core and locate the proper changes, please do.

[Eric Wieser]

Generally if you're working in an area where the universes are an important part of the theory (like ULift and category theory), you should write

universe u v
variable {X : Type u} {Y : Type v}

rather than Type*

[Jovan Gerbscheid]

The changes that @Martin Dvořák is proposing also include removing explicit universe annotations (e.g. Category.{v} C -> Category C). This does introduce universe metavariables, so this may give a slowdown.

[Martin Dvořák]

Given the info I have just learnt, I will revert the changes related to categories.

[Jovan Gerbscheid]

I looked a bit further into the slowdowns from universe metavariables, and I think part of the problem is that isDefEq has two kinds of caches: transient and permanent (the permanent one is also temporary, but resets less often). Having (universe) metavariables means that the permanent cache cannot be used.

[Matthew Ballard]

I think I tried using docs#Lean.Expr.hasExprMVar instead at some point for the cache. It did help a bit

[Jovan Gerbscheid]

That seems reasonable but I'd also worry if that can introduce bugs in isDefEq.

[Matthew Ballard]

It was very much a hack which is why I didn’t pursue it at all

[Martin Dvořák]

PR #24285 is ready for review.

[Martin Dvořák]

Benchmark +25.08% in Mathlib.Algebra.Module.Presentation.Tensor ...
Is it too much? Should I revert the changes in this file?
PS: I have just noticed that the file is not imported by any other Mathlib file except the sink. Are the changes I made there valid, first of all?

[Jovan Gerbscheid]

Interesting. This should be caused by removing the explicit universe annotation in

variable (relations₁ : Relations.{w₁₀, w₁₁} A)

I wonder if we should introduce a notation

variable (relations₁ : Relations.{*, *} A)

In the same spirit as Type*

[Jovan Gerbscheid]

I think all your changes are valid. I think the only one where you actually changed the definition is Mathlib/Algebra/Quotient.lean, but I agree with that change.

[Martin Dvořák]

Ah yeah, this is the one I was worried about the most.

[Matthew Ballard]

@Adam Topaz had thought about a Category* version in the past.

I haven’t looked yet but this sounds like a smaller scale incident of what I described before.

[Matthew Ballard]

branch#mrb/merge_type_stars merges some Type*’s Please feel free to PR but not that there is currently a Python script to understand the chances. It should probably be removed in the end.

I will be unavailable for 24-48 hours.

[Junyan Xu]

Thanks! Another automation target is to remove declared universe variables that are no longer used.

[Martin Dvořák]

Absolutely! There are plenty.

[Kyle Miller]

Jovan Gerbscheid said:

So I think going from Type u to Type* isn't bad for performance

Matthew mentioned an issue (though I'm not sure about the ASCII part, since Type* only creates names of the form u_1, u_2, ...), but another is that Type* adds the new level parameter to the end of the level parameter list, which may result in a different order. Yury mentioned this in the context of API, but I'm mentioning this as something that could cause performance differences (though I don't know if this can cause significant problems).

(I like the idea of * as a fresh universe level parameter. If it makes it to core, I think it would need to be rethought — it's odd how Type* creates non-hygienic level variables — you can refer to u_1 for example.)

[Jovan Gerbscheid]

Yes, I think the implementation of introducing a fresh universe level on the fly should be redone. Although the issue of universe hygiene is more fundamental; that also exists when using Type _.

[Kyle Miller]

A couple options:

• * could create an inaccessible name, and these names can be cleaned in a pass before the declaration is added to the environment.
• * could create a level metavariable along with a record in the TermElab state that it is an error if this metavariable unifies with anything (there would be a pass at the end checking for this, flagging the place where the level was introduced along with what it unified to). This is nice since it works just like Type _ except for the fact it can throw an error when the uniqueness assumption isn't met.

[Kyle Miller]

Jovan Gerbscheid said:

that also exists when using Type _

What hygiene issue are you talking about?

[Jovan Gerbscheid]

example (a : Type _) : a = a := Eq.refl (a : Type u_1)

I think this is what you were referring to: the universe level u_1 is valid here.

[Kyle Miller]

Yeah, that's related, and it's using the same system as Type* too. (Type* works by creating a metavariable and immediately using levelMVarToParam on it, rather than waiting for it to be applied at a later elaboration checkpoint. For theorems, that's before elaborating the body.)

[Jovan Gerbscheid]

I think * should create a level parameter, not a metavariable, because we need the function Expr.hasMVar to return false for the better isDefEq cache to be used

[Kyle Miller]

With my second bulleted option (metavariables), this would also give a better error messages than this one without having to add checks everywhere in the language:

-- error is on the whole `theorem` line
theorem weird : True := by
  have := Type*
  trivial
/-
error: AddConstAsyncResult.commitConst: constant has level params [u_1] but expected []
-/

Compare to

theorem not_so_weird : True := by
  have := Type _
    --~~ error position
  trivial
/-
failed to infer universe levels in 'have' declaration type
  Type (?u.635 + 1)
-/

[Jovan Gerbscheid]

That doesn't seem right. If we make it a def, not_so_weird should compile correctly (in the hypothetical implementation of *), but using a metavariable will trigger this error.

[Jovan Gerbscheid]

I think it should have the same effect as the current Type*, appart from issues around naming and hygiene.

[Jovan Gerbscheid]

I noticed some interesting behaviour regarding when universe metavariables get abstracted and when not:

variable (a : Type _)

-- a : Type ?u.5
-- b : Type u_1
def test (b : Type _) : True := by sorry

-- a : Type u_2
-- b : Type u_1
def test' (b : Type _) : a = a := by sorry

-- b : Type u_1
theorem test'' (b : Type _) : True := by sorry

It seems that universe metavariables are not abstracted inside the body if they are introduced via variable and do not (at first) appear in the type, and if we are in a def.

The file that slowed down by 25% contains isPresentationCoreTensor, which satisfies all these conditions. You can see the offending metavariables with set_option pp.universes true

[Jovan Gerbscheid]

Also, the universe names are in a weird order when combining variable and normal arguments:

variable (a₁ a₂ : Type _)
-- a₁ : Type u_3
-- a₂ : Type ?u.11
-- b₁ : Type u_1
-- b₂ : Type u_2
def test (b₁ b₂ : Type _) : a₁ = a₁ := by sorry

[Kevin Buzzard]

Kyle Miller said:

Matthew mentioned an issue (though I'm not sure about the ASCII part, since Type* only creates names of the form u_1, u_2, ...), but another is that Type* adds the new level parameter to the end of the level parameter list, which may result in a different order. Yury mentioned this in the context of API, but I'm mentioning this as something that could cause performance differences (though I don't know if this can cause significant problems).

You know about the 29% speedup in the (unmerged!) #21129 caused by changing the alphabetical order of the universes, right?

We have not had the benefit of that speed-up literally thousands of times since then.

[Kyle Miller]

I didn't @Kevin Buzzard; and I guess that proves that changing universe variable orders could have caused a 29% slowdown (assuming we had a good order from the beginning).

[Kevin Buzzard]

Just to be clear, this wasn't "physical" universe order changing, this was literally renaming of the universes so that alphabetically they were in a different order. But if that can cause a 29% effect then I'm sure that reordering them can!

[Kyle Miller]

Jovan Gerbscheid said:

If we make it a def, not_so_weird should compile correctly

Declarations with universe levels that can't be inferred from the type are a very special case, and such definitions are harder to use (since you have to provide universe levels). I don't think I'd mind if you had to opt in with an explicit universe level.

Plus: Is there any case of a universe level that's used only in the body of a declaration that couldn't just be replaced by 0?

[Kyle Miller]

Jovan Gerbscheid said:

I noticed some interesting behaviour regarding when universe metavariables get abstracted and when not:

Additionally, for def it also depends on whether the type is a proposition or not. If it's not, everything appears to remain as level metavariables.

[Jovan Gerbscheid]

@Kyle Miller, using explicit universes also gives the error you said is weird:

universe u

-- error is on the whole `theorem` line
theorem weird : True := by
  have := Type u
  trivial

So I think the problem here is just that Lean's universe error messages have room for improvement. (Although this isn't a common scenario in practice anyways)

[Kyle Miller]

It looks like theorem is not removing the universe levels that don't appear in the header. I'd expect "unknown universe level 'u'", just like

variable (x : Nat)

theorem notWeird : True := by
  have := x -- unknown identifier 'x'
  trivial

(Ideally it would say a bit more about how these were variables unused in the header.)

[Aaron Liu]

Like this?

-- unused universe parameter 'u'
theorem goodError.{u} : True := by
  trivial

[Kyle Miller]

No, in the context of Jovan's example, one direct fix would cause it to say just "unknown universe level 'u'" but it could say something more informative like "universe level 'u' was not used in the theorem header, so it was not included" with more work.

[Jovan Gerbscheid]

What do we think of a set_option that makes lean throw an error if there are universe metavariables left after elaboration? It would be false by default, but turned on in Mathlib, similar to autoImplicit. This would force the replacement of Type _ by Type* when possible. It would be beneficial for performance, but also for readability, because it forces universes to be introduced explicitly (either with a named level, or with the new * syntax for simple cases).

[Kyle Miller]

Kevin Buzzard said:

The culprits are declarations such as docs#Algebra.Extension and docs#Algebra.Generators .

Oops, I hope I didn't cause a diversion in the discussion here. I meant to say "is there any case of a universe level parameter that's used only in the body of a definition or theorem that couldn't just be replaced by 0?" Structures definitely make use of this sometimes for a seemingly legitimate reason, as you point out. (And that certainly doesn't change the fact that structures doing this are harder to use!)

I was thinking about this at some point because one rule Lean could take with the "failed to infer universe levels" error is to set them to zero.

def f :=
  let xs : List PUnit := []
--         ~~~~~~~~~~
  true
/-
failed to infer universe levels in 'let' declaration type
  List.{?u.2513} PUnit.{?u.2513 + 1}
-/

Indeed, when this error happens, Lean sets the level metavariables to 0 so that it can make progress with the rest of the file.

set_option pp.universes true
#print f
/-
def f : Bool :=
let xs := List.nil.{0};
true
-/

I don't think this could solve any of the universe level slowness you bring up in any way, unfortunately.

[Notification Bot]

17 messages were moved from this topic to #mathlib4 > JacobiZariski is slow. by Kevin Buzzard.

[Kevin Buzzard]

Oops, I hope I didn't cause a diversion in the discussion here.

You did, but that's not a bad thing! Clogging up this discussion is though (and this is my fault not yours), so I moved the relevant posts to the "JacobiZariski is slow" thread.

[Martin Dvořák]

I would like to return to this refactor. Is there an agreement of what the result should look like? Last time I proposed it I had an impression that not everybody had the same idea.

[Jovan Gerbscheid]

Note that there is also some value in adding universe annotations to e.g. Category. This is the same performance issue we described above, but mathlib is not consistent with this. In #25453, all I did was explicitly annotate the universes, and it gives a big speedup:

  Benchmark                                                    Metric         Change
  ==================================================================================
+ ~Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit   instructions   -36.3%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.MappingCone       instructions   -18.9%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.Triangulated      instructions   -52.0%

To aid with this kind of performance improvement, we could add a set_option (false by default) which gives you a warning if a def has to abstract univese metavariables after elaboration. Then one can turn this option on on a branch, and then fix many of these kinds of slowdowns.

[Joël Riou]

In category theory and its applications, we also have definitions/lemmas for which we sometimes need to specify the universes explicitly: replacing Type u by Type* in the code would probably lead to uncontrolled permutations of the universe parameters. Then, please do not replace Type u by Type* wherever possible.

[Robin Carlier]

My experience matches Jovan’s. Before submitting #26366, it was stated using Type* to look cool. I just specified universes everywhere and got a ~27% speedup, this is rather impressive. I don’t think I’ll use Type* ever again, even if it means ending up with things like this (I wonder how bad the perf on this one would be if we were to Type* everything).

[Matthew Ballard]

Anecdote: I was told that at one point Coq (when it was called that) took 2/3's of its time dealing with universes. (Details beyond this I don't have but maybe someone has more.)

Begs the analogous question. Until that is answered, it is hard to lock in to one particular convention.

[Jovan Gerbscheid]

Banishing Type* in general is too harsh. The important thing is to write explicit universe parameters in constants that require them explicitly (Category is the poster child here). But when working with something simple like a Group, using Type* is completely fine.

[Jovan Gerbscheid]

What de people think about using this compromise that uses Type*, but still preserving the better performance:

universe v
variable {C : Type*} [Category.{v} C]

The universes from Type* always come after the ones from universe commands, which is exactly what we want here. So we end up with lemmas like foo.{v, u_1}.

[Adam Topaz]

This isn't great. What happens if you want to specify multiple categories?

[Adam Topaz]

universe v1 v2
variable {C D : Type*} [Category.{v1} C] [Category.{v2} C]

[Adam Topaz]

Oh maybe that's okay!

[Jovan Gerbscheid]

I presume you mean

variable {C D : Type*} [Category.{v1} C] [Category.{v2} D]

[Adam Topaz]

I think even in this case, when doing category theory you very often want to control universe parameters explicitly. For example some times you need to specify universe parameters explicitly in some constructions related to existence of (co)limits, and in those situations, if you use Type*, it's possible you would need to track down the universe's name to be able to write someConstruction.{u_7}.

[Jovan Gerbscheid]

I think in such a case, writing someConstruction.{_} (or just someConstruction) would suffice, because the universe .{_} would be filled in by unification immediately.

[Jovan Gerbscheid]

But of course if you think it is clearer with the explicit universe annotation, avoid Type* :)

[Kyle Miller]

My opinion here is that people should be free to use Type* or Type u as they see fit, maybe with these guidelines:

• If you are working in an area where universe levels need to be controlled (like category theory), prefer Type u
• If you are working in an area where it's important to avoid accidental universe monomorphism (e.g. avoiding accidentally using u for multiple types when they could have had their own levels), prefer Type*
• When reviewing, we shouldn't require using one style or the other, unless it's going to cause an issue (e.g. not using explicit levels in a category theory definition whose levels can't be inferred from any of the arguments). We can politely suggest changes like usual though.

[Kyle Miller]

Robin Carlier said:

Before submitting #26366, it was stated using Type* to look cool. I just specified universes everywhere and got a ~27% speedup, this is rather impressive.

Do we know why this is happening?

Is this fundamental to Type*, or is there some underlying issue that can be fixed?

[Jovan Gerbscheid]

The issue isn't Type* vs Type u. The issue is Category.{v} vs Category.

[Robin Carlier]

I'll rebenchmark with Type* + Category.{v}, but at this point if I need to specify, I don't see the advantage of Type* beyond gaining 1 character on a few lines...

[Robin Carlier]

(I also don't know how to get precise benchmarks, my way of benchmarking is to grab the compilation command via lake build -v and feed it to hyperfine)

[Jovan Gerbscheid]

You can leave a comment saying "!bench" on your PR. Once with this version, and once after you push the change.

[Kyle Miller]

Ok, good to know @Jovan Gerbscheid.

Side note: I wonder if the elaborator should have concepts of explicit universe parameters, implicit universe parameters, and universe outparams?

• In Category, the fact that the first parameter can only be inferred by usage of the category instance leads to all these unfortunate performance problems, where if the elaborator enforced writing Category.{v} (or at least Category.{_}) you'd either solve the issue or know that there's a metavariable involved.
• In HasDerivedCategory, I saw someone struggle a lot with the fact that one of the levels is actually sort of an 'outparam', and it's unclear from the interface that this is the case. The consequence is that if you use a sorryed-out HasDerivedCategory instance, your theorems get a mysterious extra universe level. Ideally the status of this mysterious extra universe level could be more explicit, that it's meant to be determined by the other parameters and the specific arguments to the constant.

[Robin Carlier]

Jovan Gerbscheid said:

You can leave a comment saying "!bench" on your PR. Once with this version, and once after you push the change.

I know, but I'd rather waste my electricity and compute than other's for my tests, and I'd really prefer if it there was a way to get similarly detailed info locally.

[Robin Carlier]

Re-tested with Type* + Category.{v} confirms @Jovan Gerbscheid’s prediction: perfs are identical compared to the ones with explicitly named universes. So [Category] is the bad child here.
Should we go on a hunt to see if we can speed up the lib?

[Kevin Buzzard]

Don't forget to also do the JacobiZariski file, where there are Algebra.Extensions which don't have specified universes (which may or may not make this file very slow).

[Jovan Gerbscheid]

I don't think this is the problem in JacobiZarisky, sadly.

[Kevin Buzzard]

My instinct is that that file has many problems and we're solving them one by one

[Jovan Gerbscheid]

Maybe, but I think that list excludes this one

[Kevin Buzzard]

Maybe. That weird speed-up we got when we rearranged universe alphabetical order is still something I'm baffled by.

[Matthew Ballard]

Because it is a total hack

[Matthew Ballard]

Most likely, the terms that get sent to the kernel are extremely sensitive to level perturbations or permutations.

[Mario Carneiro]

is it known if this is an issue in the kernel or the elaborator?

[Matthew Ballard]

I suspect there is some overlap but the larger problem is the kernel itself.

[Mario Carneiro]

if you (or anyone) can make a reproducible example I can play with it in lean4lean and maybe give some more concrete feedback

[Matthew Ballard]

Please, I tried to do this but had limited time and failed. I would start at RingTheory.Kaehler.JacobiZariski

[Matthew Ballard]

Maybe someone else has had success minimizing since the long ago

[Eric Wieser]

Kyle Miller said:

Side note: I wonder if the elaborator should have concepts of explicit universe parameters, implicit universe parameters, and universe outparams?

I've wanted this quite often for the pp_with_univ pretty-printer, in the simplified form of "just show the first n parameters"

[Jovan Gerbscheid]

For explicit/implicit universe parameters, do you mean that we could mark this by hand, or that a parameter is explicit whenever it cannot be inferred from the arguments (like in Category or PUnit)?

[Notification Bot]

16 messages were moved from this topic to #mathlib4 > JacobiZariski in lean4lean by Johan Commelin.

[Antoine Chambert-Loir]

Couldn't there just be a linter warning that could be disactivated either locally or globally if needed?

[Martin Dvořák]

I apologize for the long silence. I need to submit my Ph.D. thesis by the end of this year, then I will have time to open a new attempt at solving Task 26.

[Matthew Ballard]

I would strongly advise against doing this in the near-to-intermediate future.

[Martin Dvořák]

Have the community's preferences changed? Or are there too many open PRs that would get a collision?

[Johan Commelin]

https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Task.2026.3A.20Replace.20Type.20u.20by.20Type*.20wherever.20possible/near/513600720
The top of the thread already calls for caution.

[Matthew Ballard]

We also have related elaborators under consideration. #32374

Even if this is merged, we will need time to discuss adaptation.

[Martin Dvořák]

Anyways... I will ask again in a month.