Notation with letter-like symbols

Stream: mathlib4

[Andrew Yang]

In a PR that was merged earlier, I introduced the notation 𝖲𝗉𝖾𝖼 R for Scheme.Spec.obj (op R), but @Marc Huisinga raised the point that it might cause confusion as it is almost indistinguishable from regular editor text. What do people think?

[Marc Huisinga]

It's worth pointing out that this is also about the question of whether we should add abbreviations like \spec for 𝖲𝗉𝖾𝖼 (vscode-lean4#483).

[Christian Merten]

Is it possible to do this with a custom elaborator? Maybe even so that we can write Spec R and Spec f where R is a ring and f a ring hom?

[Kim Morrison]

I'd prefer we don't introduce notations of this form. To me, the confusion of "is this a weird font?" outweighs saving keystrokes.

[Andrew Yang]

I'd say that the main gain is readability and not saving keystrokes, but I'm open to other options.

[Kim Morrison]

I agree saving keystrokes is not the point. I should have said that even on readability I'm not convinced this is an improvement.

[Andrew Yang]

Do you think that having Spec (actual ascii text) instead of 𝖲𝗉𝖾𝖼 as notation would be better?
I thought it was misleading to have text as notations and it might not be robust, but maybe I'm plain wrong.

[Kim Morrison]

Does it even need to be a notation? Could an abbrev work here?

[Andrew Yang]

I would like it to work on both rings and ring homs.

[Andrew Yang]

Though the current approach (Spec R for rings, Spec(f) for ring homs) might be misleading as well?

[Andrew Yang]

Okay something like

/-- Notation typeclass for `Spec`. -/
class HasSpec (A : Type*) (B : outParam Type*) where
  spec : A → B

attribute[reducible] HasSpec.spec

/-- Notation for `Spec`. See `Scheme.Spec` instead. -/
alias Spec := HasSpec.spec

instance : HasSpec CommRingCat.{u} Scheme.{u} where
  spec R := Scheme.Spec.obj (op R)

instance {R S : CommRingCat} : HasSpec (R ⟶ S) (Spec S ⟶ Spec R) where
  spec f := Scheme.Spec.map f.op

seem to work, though I'll have to test it downstream.

[Andrew Yang]

A downside is Spec f cannot trigger the instances of the form F.map f (with F being Scheme.Spec) but I think only a few such instances are useful and can be duplicated manually.

[Kim Morrison]

If you want it to work for both rings and ring homs, then please have people type X.obj R and X.map f (for some choice of X), just like for any other functor!

[Kim Morrison]

Obscuring this doesn't help anyone? (Disclaimer: I am amongst the most anti-notation people around...)

[Yaël Dillies]

As Kim says, I don't think we should be treating Spec differently from any other (concrete) functor. I'm not against eventually having notation that would unify .obj and .map.

[Andrew Yang]

All the .obj and .map and op (which is { unop := _ } in infoview) and unop are mathematically unimportant (and also not really important to Lean) noise that makes the statements 4x longer and almost unreadable.

[Andrew Yang]

Maybe I'll just make Spec R mean Scheme.Spec.obj (op R) and SpecMap f mean Scheme.Spec.map f.op as ordinary abbrevs to avoid these notations.

[Christian Merten]

I think Spec.obj and Spec.map would be fine on its own, the op R and f.op (and the even worse { unop := _}) are the annoying bits. Is there a way to make Lean interpet Spec.map f as Spec.map f.op and also pretty print Spec.map f.op as Spec.map f?

[Yaël Dillies]

Can't we make Lean pretty-print custom-named constructors?

[Yaël Dillies]

I don't think we ever want the constructor notation for them

[Yaël Dillies]

I'm also thinking about eg Rat.mk'

[Yaël Dillies]

And in fact it would be nice if we could control what constructor notation does by defining .mk separately

[Yaël Dillies]

I'll open an RFC soonish

[Kyle Miller]

@Christian Merten If you add @[pp_using_anonymous_constructor] to docs#Opposite then at least { unop := x } pretty prints as ⟨x⟩ instead. (This is a feature as of Lean 4.8.0)

[Kyle Miller]

@Yaël Dillies If you're talking about a Lean 4 RFC, could you discuss what you have in mind on Zulip before writing one?

[Eric Wieser]

I think the summary is "allow ⟨x, y, z⟩ to resolve to a user-defined function, just like how we now allow induction xyz to do so"

[Yaël Dillies]

Yeah the RFC would be to resolve (⟨⟩ : MyStruct) notation to MyStruct.mk, regardless of whether MyStruct.mk is the default constructor or an arbitrary function.

[Yaël Dillies]

That way, we both:

• stop translation functions for one-field structure type synonyms (and generally any constructor which is supposed to be an implementation detail, or whose status as the default constructor should be an implementation detail)
• get to choose which function the ⟨⟩ notation refers to

[Kim Morrison]

Andrew Yang said:

Maybe I'll just make Spec R mean Scheme.Spec.obj (op R) and SpecMap f mean Scheme.Spec.map f.op as ordinary abbrevs to avoid these notations.

This is an improvement, but I still object to having Spec and SpecMap in the first place. They are parts of a functor, so should look like it!

Moreover, SpecMap breaks the casing rules, and I think this makes it less rather than more readable.

[Andrew Yang]

I don't agree with "They are parts of a functor, so should look like it!". Localization is a functor but we have Localization + Localization.map. Tensor product is a functor but we don't write ((TensorProduct R).obj M).obj N

[Andrew Yang]

How about having SpecMap -> Spec.map that (I think) conforms to the naming convention?

[Christian Merten]

Andrew Yang said:

How about having SpecMap -> Spec.map that (I think) conforms to the naming convention?

Simply as an abbrev /alias this would clash with Scheme.Spec.map after open Scheme right? We could of course just rename the functor Scheme.Spec

[Richard Osborn]

The other issue with 𝖲𝗉𝖾𝖼 is that it often isn't rendered as a monospace characters leading to misaligned text.

[Johan Commelin]

Christian Merten said:

Is it possible to do this with a custom elaborator? Maybe even so that we can write Spec R and Spec f where R is a ring and f a ring hom?

I would be interested in an experiment with this idea. In Lean 3 we couldn't do this. But in Lean 4 we should definitely try. Not just for Spec, but for functors in general.

[Eric Wieser]

My reading of Kim's message is that making F.obj and F.map have the same spelling is not a good thing to aim for?

[Thomas Murrills]

I read Kim’s message as only necessarily saying that functors should have consistent spelling, i.e. this one functor shouldn’t look different from the rest.

I’m not sure what they think about a proposal to change how every functor application looks at once (hopefully they will tell us!), but I’m personally generally in favor of “reflect math notation as long as Lean is essentially doing the same thing”. As such I think having analogues of $Fa$ and $Ff$ (and even maybe $F\eta$ with $\eta$ a natural transformation, with its standard meaning) would be reasonable! :) (Presumably with a pp option to turn this sort of delaboration off if it ever gets confusing, and maybe this notation would be scoped.)

[Yaël Dillies]

I guess you start getting into trouble when it just so happens that F f could be (mathematically) interpreted as @map Dom Range F C D f or @obj (C ⟶ D) Range' F , namely when the same functor polymorphically acts on both objects and morphisms

[Kim Morrison]

I have no in principle objection to something that hides both the .obj and .map, except for my basic total lack of understanding why people like notation. :-)

[Kevin Buzzard]

Makes the lean code closer to what humans write?

[Yaël Dillies]

Yaël Dillies said:

Yeah the RFC would be to resolve (⟨⟩ : MyStruct) notation to MyStruct.mk, regardless of whether MyStruct.mk is the default constructor or an arbitrary function.

@Kyle Miller, does this sound reasonable as an RFC?

[Kyle Miller]

Here are things the RFC should address:

• What are a few case studies for user-specified anonymous constructors? What are concrete examples of things you could do that you couldn't before? Why is it worth implementing this feature rather than having users create custom notation per structure? (For example, MyStruct⟨a,b,c⟩ could be user syntax, without a space before ⟨.)
• What are some possible mechanisms to configure which function to use as the anonymous constructor? What are pros/cons of each, which one does the RFC recommend?
• Do user-specified anonymous constructors need to be usable for pattern matching? That is, should they need to be able to be used as a @[match_pattern]? If not, what can be done to help reduce confusion?
• If so, do they need to integrate into rcases patterns? How would that work? If not, how can you prevent confusing users that angle brackets do something different in rcases patterns for types with user-specified anonymous constructors?
• What can we do in the UI to be sure that users can see which function is being used for anonymous constructor notation? Hovers in the Infoview should automatically show the custom MyStruct.mk function, but to what extent should hovering in the source code show which function is being used?

For strong RFCs, I find the Rust RFC template to be useful.