Zulip Chat Archive

Stream: mathlib4

Topic: default "/" meaning


Thomas Murrills (Jan 21 2023 at 03:31):

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 (Jan 21 2023 at 06:04):

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

Yury G. Kudryashov (Jan 21 2023 at 06:05):

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

Yury G. Kudryashov (Jan 21 2023 at 06:06):

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

Yury G. Kudryashov (Jan 21 2023 at 06:08):

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

Thomas Murrills (Jan 21 2023 at 06:44):

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 (Jan 21 2023 at 06:47):

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

Thomas Murrills (Jan 21 2023 at 06:51):

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 (Jan 21 2023 at 06:55):

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 (Jan 21 2023 at 06:56):

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 (Jan 21 2023 at 09:16):

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 (Jan 21 2023 at 09:17):

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 (Jan 21 2023 at 09:20):

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 (Jan 21 2023 at 09:21):

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

Eric Wieser (Jan 21 2023 at 10:11):

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 (Jan 21 2023 at 10:23):

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 (Jan 21 2023 at 10:27):

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 (Jan 21 2023 at 10:30):

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 (Jan 21 2023 at 10:31):

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 (Jan 21 2023 at 10:31):

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

Reid Barton (Jan 21 2023 at 10:33):

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

Sebastian Ullrich (Jan 21 2023 at 10:33):

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


Last updated: Dec 20 2023 at 11:08 UTC