Help/pointers wanted for `Foo.{*, *}` syntax

Stream: mathlib4

[Robin Carlier]

Following #mathlib4 > `grind ext` and universe-level metavariable and part of the discussion in #mathlib4 > Task 26: Replace Type u by Type* wherever possible, a pattern that we used to use a lot in category theory ((C : Type*) [Category C]) turns out to have terrible performances and weird behavior w.r.t automation because of the universe-level metavariable introduced by [Category C]. Instead, one should always specify the universe level explicitly for Category and write something like (C : Type u) [Category.{v} C], or even (C : Type*) [Category.{v} C].

For files that are "very universe polymorphic" (usually, stuff dealing with many categories and many functors between them), this means we have to introduce a lot of universes, and not mess up any index when specifying them so as to not inadvertently "monomorphize". This makes writing (and reviewing!) that kind of code a bit of a pain.

It’s been suggested by @Eric Wieser that we should have a Category.{*} syntax, doing the same kind of things that Type* does: as far as I understand, it introduce a hidden "new" universe level variable that is not a meta-variable, and use that variable here and only here (so that repeated applications will never "monomorphize"). Having this would be nice and fix the problems mentionned above, and potentially speeds up a bit the library if we replace existing (C : Type*) [Category C] with this.

Of course, this is not only for Category: there are other classes/structures that takes extra universe level parameters (e.g Bicategory takes two extra universe parameters, so writing (B : Type*) [Bicategory.{*, *} B] is also desirable), so if we have this kind of syntax, it should in fact be available for basically any identifier that can take an universe level parameter.

It seems after that suggestion that no one decided to actually work on this, which is too bad given the massive improvement it would be.

I’m willing to give it a try, but I’m very much of a beginner with parsers/notations/meta code, so I’m asking here if some meta wizards can at least give me some pointers to help me understand what should be the best way to set this up, etc.

Of course, I guess a good place to start is the file defining Type*, but here the situation is quite different because it introduces Type* as a "full term" rather than as something that modifies existing syntaxes, takes valid identifiers as parameters like we’d want for Foo.{*, *}.

[Kenny Lau]

so Category.{*} should elab to Category.{v} every time?

[Kenny Lau]

(because Type* currently makes a different mvar every time it's called)

[Robin Carlier]

No, it should elab to a new different level variable every time (just like Type*).

variable (C D : Type*) [Category.{*} C] [Category.{*} D] would essentially replace

universe v₁ v₂ u₁ u₂
variable (C : Type u₁) (D : Type u₂) [Category.{v₁} C] [Category.{v₂} D]

[Kenny Lau]

but how would Lean know to place the new universe variable (v1 v2) before the existing variables (u1 u2)?

[Robin Carlier]

Right, this is something I did not think about. This does makes things more complicated.

I guess this would place them in random order. In most situations, that would be fine I guess?
AFAICT the reason why we put the morphisms levels before objects levels is so that expressions with extra level parameters can put the extra parameters first, i.e if we were to switch the order of u and v in the definition of a category, we’d have to write [Category.{u,v} C] and not just [Category.{v} C]. So for definitions that does not add "new" universe levels that can’t be inferred by the instances /types already, it’s probably fine? Arguably, when you do add new universe levels you shouldn’t use Type* or .{*} anyways and be precise.

[Robin Carlier]

(Note that I am asking for pointers specifically because I do not have the answers to all the questions about the thing already!)

[Kenny Lau]

This is a bit complicated, I remember something about universe order (and even alphabetical order) mattering in the JacobiZariski saga

[Robin Carlier]

When we write variable (C : Type*) (D: Type*) [Category C] [Category D] already in the infoview the displayed "names" of the unverse levels is in the "wrong order":

C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D

so that if we were "fine" with [Category C], a "not too smart" [Category.{*} C]would be fine? I don’t know how much I can trust the infoview with mvars though.

[Kenny Lau]

but wasn't it the case that we noticed [Category C] caused some slowdowns and therefore we switched to [Category.{v} C]?

[Robin Carlier]

My understanding is that the slowdowns here (maybe not in JacobiZariski) are cause by the fact that they're mvars, rather than the order.

[Kenny Lau]

I'm afraid I don't really know a lot about this, I'll wait for someone else to chime in.

[Aaron Liu]

I think we still want to put the morphism universes first

[Aaron Liu]

not necessarily because they're faster

[Aaron Liu]

but maybe we should also find out if it's faster

[Robin Carlier]

Bump. Is there a meta expert who can comment on the feasibility of this? e.g @Kyle Miller who wrote the original Type*?

A very, very dirty solution would be to not have a general Foo.{*} or Foo.{*,…,*} syntax but only for a few explicitly registered identifiers (Category, Cat, Bicategory, etc.) and then a straight copy-pasting of the code for Type* (for each identifier) may work. This is obviously a lot of duplication and not robust at all.

A perhaps less dirty solution would be to have an attribute on certain identifiers that "registers them" for this kind of syntax (and then we’d tag the declaration for Cat, Category, Bicategory etc.), the attribute would generate the syntax and make it available when registered. I don’t know enough meta to know if this is possible.

The "best" solution would be to be able to declare * as valid syntax in whatever syntax category universes live, and have it being parsed with code similar to Type*. The most naive

/-- error: Unknown attribute `[level_parser]` -/
#guard_msgs in
syntax "*" : level

fails

The last suggestion is probably ridiculous/might make no sense as is but hopefully I’ll learn something from whoever explains me why it’s ridiculous.

[Adam Topaz]

Category* has been requested many times at this point. Here's a PR: #30797

[Robin Carlier]

Having this is clearly an improvement over having nothing, but I’m slightly worried about the fact that you’re going with the first proposition in my post above, i.e that we basically have to duplicate the code if we want Bicategory* (bicategories have the same issue as categories w.r.t universe mvars), or any other identifier of that kind that might introduce extra universe levels. There doesn’t seem to be that much such identifiers in practice, so perhaps duplication is fine? (I withdraw my wish that Catshould be such an identifier, because we often want (a b : Cat) to mean (a b : Cat.{v_1, u_1}) and not (a : Cat.{v_1, u_1})) (b : Cat.{v_2, u_2}), which is what a Cat* would do if it were to mimic Type*.)

[Adam Topaz]

I agree about the duplication issue, but this particular elaborator reorders the universe parameters in some controlled and non-naive way. So I do think it’s worth having this special case (and maybe also the bicategory case)

[Robin Carlier]

I think there’s also Groupoid (which extends Category), but admitedly we use them way less than Category so we can just declare the universe explicitly for Groupoid if this is too much duplication.

[Eric Wieser]

Robin Carlier said:

The last suggestion is probably ridiculous/might make no sense as is but hopefully I’ll learn something from whoever explains me why it’s ridiculous.

initialize Lean.Parser.registerBuiltinDynamicParserAttribute `level_parser `level

should fix it

[Eric Wieser]

But it has to be in a different file to the one where you define the syntax

[Adam Topaz]

I've described what Category* does in the PR description of #30797 . Since there is still the question of whether we even want this special case which orders universes in a particular way, as opposed to a more generic Foo.{*,_,*}, it would be helpful if anyone who has been fed up with universe declarations in category theory could take a look at the description. The test file has some more detailed examples illustrating the behavior.

[Adam Topaz]

Quick note: I did just change the behavior so that (C : Type _) [Category* C] and [Category* (Type _)] now both do work. There was no reason to exclude level mvars in C or its type.

[Kenny Lau]

why is Type part of the syntax?

[Adam Topaz]

What do you mean?

[Kenny Lau]

Type seems redundant in the syntax [Category* (Type _)] (what else could it be)

[Adam Topaz]

[Category _] would make an expr metavariable for the term, but [Category (Type _)] makes a level metavariable.

[Adam Topaz]

I'll add these as tests:

section

variable [inst : Category* _]

/--
info: inst : Category.{v_1, ?u.985} ?_mvar.987
-/
#guard_msgs (info) in
#check inst

variable [inst2 : Category* (Type _)]

/--
info: inst2 : Category.{v_2, ?u.1005} (Type ?u.1007)
-/
#guard_msgs (info) in
#check inst2

end

[Kenny Lau]

Adam Topaz said:

[Category _] would make an expr metavariable for the term, but [Category (Type _)] makes a level metavariable.

i'm suggesting to change the syntax/elab so that [Category* _] make a level mvar

[Kenny Lau]

(did you mean to type with *?)

[Kenny Lau]

wait i'm bit confused

[Kenny Lau]

why would you want to assume an arbitrary category instance on the type Type ?u

[Kenny Lau]

we already have one and the homs are functions

[Adam Topaz]

Type _ is just a convenient way to introduce something with a universe mvar. This is just for testing Category*.

[Adam Topaz]

I don't know what you're suggesting with Category* _.

[Kenny Lau]

/--
info: inst2 : Category.{v_2, ?u.1005} (Type ?u.1007)
-/

I'm referring to this output, which says to me "assume an arbitrary category instance on the type Type ?u"

[Kenny Lau]

ok, I guess you're suggesting that I should overlook that for now

[Kenny Lau]

Adam Topaz said:

/--
info: inst : Category.{v_1, ?u.985} ?_mvar.987
-/

should this instead look like Category.{v_1, u_1} ?mvar?

[Adam Topaz]

yeah, I should investigate why it looks like ?_m.

[Adam Topaz]

Adam Topaz said:

yeah, I should investigate why it looks like ?_m.

fixed