Naming convention for structure projections and dot notation

Stream: mathlib4

[Bhavik Mehta]

(This was originally for the undocumented informal policy thread, but after writing it I realised it makes a lot more sense as its own thread!)

Here's something that's been on my mind recently: the naming convention for functions which are at least one of a) structure projections (eg Functor.obj) or b) dot notation: should these be prefixed or suffixed?

Currently mathlib often uses suffixes in names for structure projections, eg docs#CategoryTheory.Functor.comp_obj, and these are almost always spelled using dot notation. (The exception is coercions to fun/set, which are named coe_ and written using prefixes). For example named lemmas generated by simps are always suffixed, unless they're special cased otherwise (which happens exactly in coercion case).
The Lean4 Std naming convention explicitly prescribes that structure projections should be suffixed: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md#naming-algorithm-for-theorems-and-some-definitions, but my understanding is that this is not meant to be prescriptive for mathlib.

Mathlib in practice is somewhat split between whether prefixes or suffixes should be used for dot notation, except: predicates are explicitly named in #naming as being prefixes (except for certain common examples like _injective). Yaël claims #mathlib4 > Naming convention @ 💬 here that use of dot notation should not change the name, which didn't seem to have either pushback or general agreement. (Others also suggested that "functions are prefixed" in general might not even be the right rule, let alone dot notation). Before that, a similar discussion happened #general > #naming and dot notation here, where there was general (but not complete) consensus that use of dot notation should change the name. For example Kim suggests that we encourage dot notation to be used, and so the naming should too (although this was quite a while ago, so it's very reasonable for opinions to have changed!).

I would like there to be a clearer convention on when prefix or suffix should be used for these situations.

[Mario Carneiro]

This discussion also came up in Batteries and we went with prefix naming convention for both functions used in dot notation as well as structure projections

[Mario Carneiro]

It's interesting (surprising?) that Std is now going the other way

[Markus Himmel]

The reason why Std has this convention is because I believed that this is the preferred in mathlib, and I guess I believed this because this is the scheme used by the simps attribute.

[Markus Himmel]

I think it's safe to say that the standard library convention will change to match whatever mathlib decides here.

[Bhavik Mehta]

Markus Himmel said:

The reason why Std has this convention is because I believed that this is the preferred in mathlib, and I guess I believed this because this is the scheme used by the simps attribute.

From looking through what happened at the time, it seems to me that mathlib preferred suffix for structure projections, and so simps was implemented to reflect this, so that it could be used out-of-the-box to generate lemmas. So that justification seems reasonable enough!

[Mario Carneiro]

I wanted to link a discussion on Batteries about this but my search-fu is failing. I think it was on a github issue?

[Mario Carneiro]

aha: https://github.com/leanprover-community/batteries/pull/329#issuecomment-1786193983

[Markus Himmel]

Personally, I like the rule "functions are prefixes (except for infix notations) and dot notation does not matter" (which if I understand correctly is the Batteries convention). I like it because it contains very few special cases and it is easy to construct and guess names using this rule.

[Bhavik Mehta]

Note that following this rule would require a lot of changes (and deprecations) in mathlib; especially throughout category theory!

[Mario Carneiro]

I recall that Kim was not happy with this choice in Batteries (well, at least they were advocating for dot notation as suffix)

[Kyle Miller]

I used to be an advocate for "if a function is meant to be used with dot notation, use a suffix". One justification I had for this is that we name theorems for other notations based on how they pretty print (e.g. add comes between operands' names). However, using dot notation is optional, and binary operations are basically not optional. The pretty printer is allowed to not use dot notation when it would not round trip as well.

Because of these reasons, I've shifted toward being pro "always prefix". Somehow still Functor.comp_obj somehow feels more right than Functor.obj_comp (and a point for Functor.comp_obj is in discoverability; comp is more salient than obj), but I don't mind to see the Functor.obj_comp.

[Bhavik Mehta]

In what sense is dot notation more optional than binary operations? I can write HMul.hMul a b just as I could write Functor.obj (F.comp G) X (and in this example, avoiding dot notation for Functor.obj is more painful than avoiding the binary operation!)

[Kyle Miller]

In the sense that no one realistically writes HMul.hMul a. Everyone expects HMul.hMul to be pretty printed using *.

[Kyle Miller]

Well, people probably do write HMul.hMul a sometimes, but at least HMul.hMul a b is unlikely.

[Bhavik Mehta]

But no one realistically writes Functor.obj F X either!

[Kyle Miller]

Wow, it really is never. Prefunctor.obj appears just once in Mathlib.AlgebraicGeometry.Scheme.

[Bhavik Mehta]

On a quick grep through mathlib, I can find two instances (outside of meta code) of fully-applied HMul.hMul a b, and one of Prefunctor.obj, as you mention

[Mario Carneiro]

does that include uses of obj with the appropriate namespace open?

[Bhavik Mehta]

Actually, that one is to define notation:

scoped[AlgebraicGeometry] notation3:90 f:91 " ⁻¹ᵁ " U:90 =>
  @Prefunctor.obj (Scheme.Opens _) _ (Scheme.Opens _) _
    (Opens.map (f : Scheme.Hom _ _).base).toPrefunctor U

[Bhavik Mehta]

Mario Carneiro said:

does that include uses of obj with the appropriate namespace open?

It does not (although I really doubt that happens)

[Mario Carneiro]

well when you have to use the namespace dot notation is clearly better but when it is open they are equally terse

[Bhavik Mehta]

Yeah, I can't find any matches for open.*Prefunctor, and looking through the files which namespace Prefunctor, none of them seem to use obj as a prefix

[Mario Carneiro]

Certainly this happens a lot for list functions

[Mario Carneiro]

Isn't obj also in the Functor namespace?

[Bhavik Mehta]

I don't think so? It's docs#Prefunctor.obj

[Mario Carneiro]

yes, but there is extends magic

[Kyle Miller]

Maybe it should, but that doesn't put it into the Functor namespace

[Kyle Miller]

You can't use Prefunctor.obj on a Functor without using dot notation.

[Kyle Miller]

without writing Prefunctor.obj (Functor.toPrefunctor f)

[Kyle Miller]

(remember the good old days of Lean 4 when it pretty printed as f.toPrefunctor.obj? :-))

[Mario Carneiro]

I see, so that explains why this one in particular is always dot notation

[Kim Morrison]

Mario Carneiro said:

I recall that Kim was not happy with this choice in Batteries (well, at least they were advocating for dot notation as suffix)

I think I was confused by inconsistencies, rather than unhappy with any particular choice. (At least I hope so! I recall also having the same thought Markus mentions above: thinking @[simps] was prescriptive.)

I would prefer "functions are prefixes, ignore dot notation, projections are not special" if we can get there!

[Eric Wieser]

I guess this means that instead of foo_apply and foo_symm_apply we'd have foo_apply and symm_foo_apply?

[Eric Wieser]

Or is symm going to get a special case?

[Bhavik Mehta]

Thinking more about the distinction between List and functor as above, to me the difference is in how the pretty-printer shows it:

import Mathlib

open CategoryTheory

variable (F : Type ⥤ Type) (X Y : Type) (a : List X) (f : X → Y)

#check a.map f -- says List.map f a
#check F.map f  -- says F.map f

Drawing the line here would be a smaller change to mathlib. And for Kyle's point of the pretty printer is allowed to not use dot notation: it's still well-defined what the "standard" behaviour of the pretty printer is for a definition.

[Bhavik Mehta]

Eric Wieser said:

I guess this means that instead of foo_apply and foo_symm_apply we'd have foo_apply and symm_foo_apply?

If I'm understanding correctly, "projections are not special" means that bundled maps would have the apply as prefixed as well, since that's a structure projection. So bare functions would be suffix but bundled functions would be prefix? Or there should be special cases for certain kinds of projections instead

[Aaron Liu]

It's actually not a structure projection, but DFunLike.coe.

[Bhavik Mehta]

I think that's an implementation detail, these are named from (eg) here: https://github.com/leanprover-community/mathlib4/blob/da9d909e9bbfda893df76c07801fe587bc030fc9/Mathlib/Algebra/Group/Hom/Defs.lean#L515

[Aaron Liu]

You can tell they're distinct because we have lemmas to rewrite between them (eg docs#Equiv.toFun_as_coe)

[Bhavik Mehta]

I'm not sure I understand the rule then, it's that structure projections are prefix unless someone makes them into a DFunLike?

[Aaron Liu]

I think the rule for pp is that if the first explicit argument has the type with the same namespace, then it's dot notation

[Aaron Liu]

Should we just mirror that?

[Bhavik Mehta]

Perhaps, but that's inconsistent with Kim's rule from above, I'm pretty sure

[Johan Commelin]

Kyle Miller said:

Because of these reasons, I've shifted toward being pro "always prefix". Somehow still Functor.comp_obj somehow feels more right than Functor.obj_comp (and a point for Functor.comp_obj is in discoverability; comp is more salient than obj), but I don't mind to see the Functor.obj_comp.

To me this salience is an important feature. The status quo somewhat prioritizes it, but not consistently. I would like new conventions to also take it into account.