RFC: adjust argument explicitness on typeclass projections

Stream: lean4

[Kevin Buzzard]

Sometimes it would be nice to able to change Lean's default choices for binder types on typeclass projections. Example from mathlib4:

variable (R : Type u)

class CharP [AddMonoidWithOne R] (p : ℕ) : Prop where
  cast_eq_zero_iff' : ∀ x : ℕ, (x : R) = 0 ↔ p ∣ x

-- porting note: the field of the structure had implicit arguments where they were
-- explicit in Lean 3
theorem CharP.cast_eq_zero_iff (R : Type u) [AddMonoidWithOne R] (p : ℕ) [CharP R p] (x : ℕ) :
    (x : R) = 0 ↔ p ∣ x :=
  CharP.cast_eq_zero_iff' (R := R) (p := p) x

Here the binder type for R on CharP.cast_eq_zero_iff' is implicit. But in practice we want an explicit binder type here, and in Lean 4 this necessitates making a "bogus" primed field for the CharP class, instantly defining the correct field with the right binder type, and then having to explain to newcomers why, when making new instances of this class, the name of the field has got some weird prime in which never shows up in any code and is not supposed to be used anywhere. In Lean 3c we had the (very counterintuitive IMO) syntax

class char_p [add_monoid_with_one R] (p : ℕ) : Prop :=
(cast_eq_zero_iff [] : ∀ x:ℕ, (x:R) = 0 ↔ p ∣ x)

with the [] meaning "make R have the () binder", leading to more compact code (no need for an auxiliary definition) and a different kind of user confusion ("what are those square brackets?"). I'm no regex guru but searching for \(.*\[\] : in mathlib3 gives me 165 hits, most of which look genuine.

This just came up in a PR I was making to mathlib4 and it was suggested I open a Lean 4 issue, but reading the instructions there it advised me to bring this up on the Zulip first. Should I open this as an RFC issue on the lean 4 github repo? I think perhaps the most interesting discussion is suggestions of possible syntax; I think the lean 3c [] is not ideal, but IIRC we couldn't have () for some reason.

[Eric Wieser]

Maybe the syntax could be

class CharP [AddMonoidWithOne R] (p : ℕ) : Prop where
  variable (R) in
  cast_eq_zero_iff' : ∀ x : ℕ, (x : R) = 0 ↔ p ∣ x

[Eric Wieser]

I agree the lean3 syntax was completely incomprehensible

[Eric Wieser]

One place where this would have been very useful is docs#CategoryTheory.MonoidalCategory.tensorUnit; for now we work around the argument explicitness with a custom notation and elaborator that pretends it is explicit

[Eric Wieser]

The situation at the moment is worse for data fields (like tensorUnit and HopfAlgebra.antipode) than it is for prop fields, since if you make primed and unprimed versions of your data, you now need to do the same for all the proof fields that mention that data

[Jireh Loreaux]

That data issue came up several times during porting. I consider this one area of our "technical debt" as discussed at the last meeting.

[Kevin Buzzard]

So am I allowed to make an RFC on the Lean repo now?

[François G. Dorais]

This was removed long ago - https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Workaround.20for.20.60.7B.7D.60.20annotation.20in.20structures/near/278993577

[Kevin Buzzard]

Well it's used over 100 times in mathlib3 and I've just spent quite a lot of pain creating this horrible workaround branch#kbuzzard-coalgebra-refactor making a bunch of stuff more ugly (with more to come if I'm to push this through). If I could make R and A explicit in comul and counit it would be a lot less hassle

[Kim Morrison]

Kevin Buzzard said:

So am I allowed to make an RFC on the Lean repo now?

I think good advice for RFCs is to try to summarise the problem, but that it is better if you have ideas about a preferred solution that these go in comments, rather than the top post. There's no need to have disagreements about the solution get in the way about agreement about the problem.

[Kyle Miller]

I thought an RFC is supposed to be an explanation of a design along with an analysis of the current situation and a comparative analysis of multiple alternative solutions. Just summarizing a problem sounds like a standard Issue to me.

[Kyle Miller]

A good RFC is a design document that, once accepted, is enough to go and implement the design.

[Kim Morrison]

Yes, you're right, and I said the wrong thing.

[Kim Morrison]

I should have expressed it a hope that people writing issues and RFCs avoid writing: "X is a problem, and should be fixed as Y".

[Kim Morrison]

That is, don't be prescriptive about what you think the solution should be, as then criticism of the proposed solution can implicitly derail the discussion of the existence of the problem.

[Kim Morrison]

I'm not complaining about the good RFCs, I'm complaining about the bad ones. :-)

[Timo Carlin-Burns]

Scott Morrison said:

I should have expressed it a hope that people writing issues and RFCs avoid writing: "X is a problem, and should be fixed as Y".

But if an RFC is a design document for a specific solution, won't it take that form? Or are you trying to say that the RFC shouldn't take that form because the problem should already be established by first opening an issue?

[Kevin Buzzard]

I tried to open an issue, but I was immediately forced to choose between a bug report and an RFC. I chose RFC and it told me I should discuss on Zulip first. That's how we got here.

[Thomas Murrills]

What are some concrete examples of "good RFCs"? Maybe that would help communicate the intention here (which I also find a bit confusing—sometimes there's a somewhat blurry line between a proposed design and a proposed implementation!).

[Eric Wieser]

In the interest of not just forgetting this RFC, I think you should make the GitHub issue

[Kevin Buzzard]

Sorry for the delay; there was a student coursework deadline for my course this week and it's been quite hectic. lean4#3574 . Please feel free to edit/clarify/add comments; I am certainly not an expert in this area; all I knew was that the combination of having CoalgebraStruct and Coalgebra together with fields with bad binders was quite a mess to fix (and indeed I still haven't managed to get things working; I wouldn't even be doing this if I could choose my binders in the definition).

[Kyle Miller]

What do we think about solving this not by altering the syntax, but by making the binder list be interpreted with variable binder update rules?

class CharP [AddMonoidWithOne R] (p : ℕ) : Prop where
  cast_eq_zero_iff' (R) : ∀ x : ℕ, (x : R) = 0 ↔ p ∣ x

For a first version, the rules could be:

1. Binder updates must come first. No writing cast_eq_zero_iff' (x : ℕ) (R) : (x : R) = 0 ↔ p ∣ x.
2. To prevent confusion, shadowing in structure field binders won't be allowed. For example, foo (p : Int) : ... would not be allowed since it shadows the p parameter.
3. The binder updates are applied to the computed projection type. The alternative is updating the binder kinds before adjusting implicitness. While doing it before could result in fewer binders that need updating (since the binder kinds for other parameters could adjust themselves based on what's now explicit/implicit), the results are likely to be hard to predict.

I have things mostly set up now to be able to implement this.

[Kyle Miller]

Expanding on point 3, the current algorithm when generating projections includes these steps:

1. generate the full type of the projection
2. with some exceptions, reset the binder kinds of all the structure type parameters to be explicit
3. run an inference procedure that makes explicit structure parameters be implicit if they can be inferred from types of later parameters or the return type

My proposal here is that user-provided binder kind updates would be a step 4 to override the inferred kinds, rather than a step 2.5 that overrides kinds before the remaining kinds are inferred. As a step 4, all you need to do as a user is look at the type of a projection, decide you don't like some of the arguments, and override just those ones. However, if it were a step 2.5, you would have to iterate this process in trial-and-error, since it's likely no one really knows how to run this algorithm in their head. (It's subtle too, since the results can depend on whether a parameter appears within some instance in some parameter.)

[Kyle Miller]

I have an implementation of this at lean4#7742, with some small differences:

• Only parameters in the declaration itself can be overridden — no parameters from variables. This is motivated by the fact that there are a number of cases where variables are clearly not meant to be parameters (see mathlib4#23469 for cases that needed to be fixed). Key design constraint: we cannot know whether variables are going to be parameters or not when we have to decide whether a binder is an override. (The variable .. in proposal would avoid this.)
• Only a prefix of the binders are considered for overrides. Multi-identifier binders are allowed for overrides, but if any of the identifiers aren't possible parameters, then the whole binder isn't used for overrides, without any warnings.

My thinking is that this might not be the finalized design, but we should have the feature in some capacity, and this version would let people get started applying it to mathlib.