Overloaded notations have bad performance

Stream: mathlib4

[Robin Carlier]

I was reading the discussion at #22698 which seemed to imply that overloading notations was having quite a performance hit.
So in #25922 conducted a little experiment with an other famous overloaded notation: docs#CategoryTheory.MonoidalCategoryStruct.tensorHom, which has the same notation as docs#CategoryTheory.MonoidalCategoryStruct.tensorObj and docs#CategoryTheory.MonoidalCategory.tensorIso.

I changed the tensor product of maps from ⊗ to ⊝ and the tensor product of isos to ⊖, played build error whack-a-mole for half an hour and benched it, the result is a -0.10% on the whole build, with big improvement in files related to monoidal categories.

I don’t have any opinion about changing these notations, because the current ones are both convenient and close to the common mathematical practice, but I feel that this is good data to have at hand.

[Yaël Dillies]

I should add that unification with those overloaded notations is very poor, to the point where I now reflexively replace with tensorHom/tensorIso when building a term, so that I can see what's going on in the infoview

[Yaël Dillies]

I would be happy with notations like ⊗ₘ (for ₘorphism) and ⊗ᵢ (for ᵢso)

[Kevin Buzzard]

Just to be clear: the diff for this PR seems to indicate that it is literally only changing notation? And the bench is

+ ~Mathlib.CategoryTheory.Localization.Monoidal       instructions   -23.7%
+ ~Mathlib.CategoryTheory.Monoidal.Category           instructions   -21.1%
+ ~Mathlib.CategoryTheory.Monoidal.Mon_               instructions   -13.0%
+ ~Mathlib.Tactic.CategoryTheory.Monoidal.Normalize   instructions   -40.7%

?!

[Robin Carlier]

Yes Kevin, this is only a notation change.

[Johan Commelin]

Yaël Dillies said:

I would be happy with notations like ⊗ₘ (for ₘorphism) and ⊗ᵢ (for ᵢso)

Seems like a good idea. Especially if we record a todo note to revisit this if the elaborator is improved in this area.

[Yaël Dillies]

Okay, does @Robin Carlier want to update #25922 accordingly?

[Robin Carlier]

I don’t mind running sed to change the notations again in the actual lean code, but this PR did not touch any docstrings and this might be more of a massive pain to go and change all of them everywhere, and I feel like this should be done if we change the notations, even if they’re still "understandable" with the old notations.
So basically I’m okay updating if someone lends a hand for the docstring editions.

[Yaël Dillies]

Sure, happy to do that

[Robin Carlier]

great, I’ll run the sed and give you access to my fork

[Yaël Dillies]

I should have access to that branch already unless you've unticked the box when opening the PR :wink:

[Robin Carlier]

Oh right! even better.

[Robin Carlier]

alright, I pushed the new notations, hopefully the autoreplace went well

[Robin Carlier]

aaaand it rot already :D

[Robin Carlier]

Should be ok now, have fun!

[Yaël Dillies]

Oh actually I can't seem to be able to push to your fork for some reason

[Yaël Dillies]

Wait no I did push. It's just the UI that complained about nothing

[Jz Pan]

Yaël Dillies said:

I would be happy with notations like ⊗ₘ (for ₘorphism) and ⊗ᵢ (for ᵢso)

Are these also notations for TensorProduct.map and TensorProduct.congr?

[Robin Carlier]

I did not touch the notations outside of monoidal categories, so the current algebra notations are unchanged yet. If these are also duplicated, it’s worth investigating the perf drawback they bring.

[Jz Pan]

Robin Carlier said:

so the current algebra notations are unchanged yet.

No I think currently there are no notations for them yet.

[Robin Carlier]

Thanks @Yaël Dillies for going through the docstrings! I’ll format the PR body/title and I think we’re good to go.

[Johan Commelin]

Johan Commelin said:

Yaël Dillies said:

I would be happy with notations like ⊗ₘ (for ₘorphism) and ⊗ᵢ (for ᵢso)

Seems like a good idea. Especially if we record a todo note to revisit this if the elaborator is improved in this area.

Did you also add some such todo? I couldn't quickly find it in the diff

[Robin Carlier]

Nope, did not add any yet. I’ll add something about it soon and keep the PR tagged "WIP" untill it’s done

[Johan Commelin]

Thanks! Please ping me when it's ready

[Robin Carlier]

Johan Commelin said:

Thanks! Please ping me when it's ready

:ping_pong:

[Johan Commelin]

ping-pong -- syn-ack -- :peace_sign: