default "/" meaning

Stream: mathlib4

[Thomas Murrills]

I think that if people type e.g. 3 / 4, there's a ≥90% chance they mean three fourths instead of 0—but 0 is the default interpretation, since / among nats defaults to Nat.div, and / among ints defaults to the similar Int.div.

I understand the desire to have operations default to a α → α → α type signature, but my expectation is that that just doesn't reflect the most common actual usage in this particular case.

I feel as though type annotations should be required to specify that I actually want e.g. Int.div instead of type annotations being required to get a rational number. (If type annotations wouldn't work in this case for whatever reason, could we either move to another symbol or just rely on Int.div or Nat.div?)

Is there any support for having / among nats and ints always land in ℚ in mathlib4?

[Yury G. Kudryashov]

Currently, we try to be as close to mathlib3 as possible.

[Yury G. Kudryashov]

While Lean 4 supports HDiv, we don't use it (yet).

[Yury G. Kudryashov]

Once the migration is complete, we can talk about possible refactors.

[Yury G. Kudryashov]

E.g., we don't use HMul for scalar multiplication.

[Thomas Murrills]

You’re right, I should have saved this thought until after the port! :)

…If we dare to think that far in advance, though, how do people feel about this? 👀

[Heather Macbeth]

I guess you'll also propose making nat-subtraction give an integer?

[Thomas Murrills]

That DOES seem reasonable to me! :) But if I had to make a case for just one change, I would say that there’s a bit of a stronger one for /, since / is not “just” a binary operation, but also our primary way of writing nonintegral rational numbers.

[Reid Barton]

Agda uses ∸ for Nat subtraction, which seems sensible and would reduce the number of "how come I can't prove this [false] lemma" questions

[Thomas Murrills]

I might also suggest the notation ÷ for nat and int division, which would coincidentally be visually consistent with ∸! (…In the distant future, of course. 🙃)

[Sebastian Ullrich]

We considered monus early in Lean 4 and discarded it for being entirely too strange for programming. I'm afraid I don't have a satisfying answer here.

[Sebastian Ullrich]

Perhaps making the "bad" instances scoped would be acceptable for programmers if we also had a system to suggest opening that namespace on failed TC inference to avoid the immediate "WTF" reaction

[Thomas Murrills]

Hmm, it might be too strange for programming, but is it too strange for mathematics? If not, would localizing the notation to mathlib4 somehow be a potential solution?

[Sebastian Ullrich]

How would that help if there is still a global Sub Nat instance in core?

[Eric Wieser]

Would it make sense for 2 / 3 with natural number literals to desugar to ofFraction 2 3? Then that typeclass could just be missing for Int and Nat, and you could force int division with (2)/3 or something

[Reid Barton]

Sebastian Ullrich said:

We considered monus early in Lean 4 and discarded it for being entirely too strange for programming. I'm afraid I don't have a satisfying answer here.

But isn't the semantics of - on Nat even more "too strange for programming"? I thought this would be an advantage of monus, not a disadvantage

[Reid Barton]

For instance if you write a[i-1] and i : Nat is zero then I think it's very unlikely you silently want to return a[0]

[Sebastian Ullrich]

Right, but usually we use subtraction in that way when we're relatively sure it cannot overflow... famous last words. What I'm trying to say is, I think programmers expect that there is some subtraction that does the right thing in the happy case, and are aware that it probably doesn't do what they need in other cases.

[Reid Barton]

If i - 1 = -1 : Int then you can make a GetElem instance that does the right thing e.g. a[-1]? = none, or you can use dotminus and then be aware that you need to check somethinig

[Reid Barton]

In advent of code I basically never used Nat, since it's so obviously full of footguns

[Reid Barton]

Like it's possible to write correct code with Nat sure, but why try

[Sebastian Ullrich]

True, our APIs are perhaps more Nat-focused than they should be. Though / is not quite as easy to solve.