New range syntax in lean 4.22

Stream: general

[Alfredo Moreira-Rosa]

It's unfortunate that the new range syntax is a breaking change and not an additive one.
This could have been done i'm sure:

1...*, 1...=3, 1...<3, 1<...=2, *...=3..
-- could have been
[1:] , [1:3=] , [1:3] , [≠1:2=], [: 3=]

this would have allowed non breaking change. am i missing something ?

[Notification Bot]

2 messages were moved here from #announce > v4.22.0 by Kim Morrison.

[Kim Morrison]

ecyrbe said:

It's unfortunate that the new range syntax is a breaking change and not an additive one.
This could have been done i'm sure:

1...*, 1...=3, 1...<3, 1<...=2, *...=3..
-- could have been
[1:] , [1:3=] , [1:3] , [≠1:2=], [: 3=]

this would have allowed non breaking change. am i missing something ?

Non-breaking wasn't the highest priority consideration for this change.

[Alfredo Moreira-Rosa]

Can you elaborate why breaking was needed ? i expect that since lean has a lot of third party libraries depending upon it, that if there is a path to not break them, that it would be taken care to not.
But, yes, too late.

[Yaël Dillies]

What's the motivation for this range syntax? I find it

1. very hard to parse
2. unlike anything else I know

[Ruben Van de Velde]

Looks similar to Rust's ranges, I think

[Weiyi Wang]

Do they get recommended spelling like Ico?

[Eric Wieser]

See also #mathlib4 > dropping Set.Ico etc in favor of new core syntax @ 💬

[Eric Wieser]

In what sense is this a breaking change? This still works:

#check [1:3]
#check 1...<3

[François G. Dorais]

Using three dots instead of two is going to take some getting used to.

[François G. Dorais]

It would be nice to have … (U+2026) as an alternative.

[Edward van de Meent]

that would also solve the scientific parsing/highlighting issue

[François G. Dorais]

This is a bit over the top: could something like a[1] +⋯+ a[k] be made to work as expected? (⋯ is U+22EF)

[Alfredo Moreira-Rosa]

Eric Wieser said:

In what sense is this a breaking change? This still works:

#check [1:3]
#check 1...<3

Thanks for the clarification. I was under the impression that old one was removed. If not, that's good news.

[Eric Wieser]

it does now seem slightly strange to have two ways to spell the "same" thing, but I'm confident that if they were merged, the old spelling would be deprecated first to give people warning.

[Kim Morrison]

I'm pretty happy with this change: avoiding [] in notations helps avoid the fragility that comes with interacting with the rather greedy list notation. The new notation both parses well, and I think is pretty straightforward to learn to read.

[Paul Reichert]

I've tried out various notations and the one I chose seemed like the best compromise:

• It avoids many parsing ambiguities. .. is used for ellipses in many places. Making the parser happy was much trickier than it seemed.
• It should support unbounded ranges, too (e.g. 1...*, or even *...*). Without the *, this caused more ambiguities (granted, the [] syntax would have solved this, too).
• [] syntax reminds of lists, even though ranges aren't lists. Moreover, [] is usually used for closed intervals in mathematics, so it seemed suboptimal.
• The new ranges are different in that they are polymorphic. They can be put to work for types other than Nat. Therefore, parts of the API need to be different. So I think that having a different notation for the new ranges is actually beneficial for backward compatibility -- this way we could introduce the new ranges before deprecating/deleting the old ones.

If you use the new ranges, feel free to let me know of your experience using them so that we polish rough edges quickly!

[Jireh Loreaux]

What are the naming conventions? That is, how do you distinguish between lemmas about PRanges which have open lower bounds and lemmas which have closed lower bounds?

[Paul Reichert]

François G. Dorais said:

It would be nice to have … (U+2026) as an alternative.

That seems reasonable, but every additional notation in core means that downstream projects are more restricted in their custom notation. Not a no-go but something to keep in mind.

[Paul Reichert]

Jireh Loreaux said:

What are the naming conventions? That is, how do you distinguish between lemmas about PRanges which have open lower bounds and lemmas which have closed lower bounds?

Weiyi Wang said:

Do they get recommended spelling like Ico?

Right now, there's only the standard library naming scheme without a special recommended spelling. I think Ico spelling is already used by Mathlib for set intervals, and I don't think we had a recommended spelling for Std.Range, right?

So I think right now, the naming can be prangeMk_open_closed for an open and closed interval, which is admittedly clunky. There aren't many lemmas so far for which the question of spelling arose. For convenience, the standard library sometimes uses namespaces like in ClosedOpen.mem_succ_iff. I'm happy to brainstorm ideas for improvements of the spelling or other parts of the design (but perhaps in a different thread).

[Yaël Dillies]

My personal expectation would have been {a < x < b} for bounded intervals, and some thought to be put in the notation for half-unbounded and unbounded intervals

[Eric Wieser]

with x hard-coded as the name? {a < · < b} might be a better alternative

[Notification Bot]

22 messages were moved here from #general > v4.22.0-rc2 by Ruben Van de Velde.

[Yaël Dillies]

Yes, that's a great idea! Then {a < ·} also makes sense

[Eric Wieser]

But this only really makes sense for Set / Finset notation

[Eric Wieser]

If you wanted a list version, then presumably you'd write [a < ·]

[Eric Wieser]

And it's ambiguous whether({a < ·}) is Set.Ioi a or (fun x => {a < x})

[Kyle Miller]

Eric Wieser said:

And it's ambiguous whether({a < ·}) is Set.Ioi a or (fun x => {a < x})

Yeah, there's ambiguity, and depending on how it's implemented it would take core support, due to the way · expansion works.

In the {a < · < b} case, it could have · as part of the notation and not have any · expansion issues.

Any reason not to embrace {a <...< b}, etc., using the new range syntax? I'm sure we can figure out how to deal with the Singleton ambiguity, and mathlib can also have unicode extensions to write a <...≤ b rather than a <...= b.

[Arthur Paulino]

I think {a < ... < b} is pretty innovative and expressive. And even better if using ⋯ is a possible alternative to ....

Personally, I'd prefer the following specific notations:

• {a < ⋯} and respective alternative for ≤
• {⋯ < b} and respective alternative for ≤
• {a < ⋯ < b} and respective alternatives for ≤

[Eric Wieser]

Kyle Miller said:

I'm sure we can figure out how to deal with the Singleton ambiguity,

One way would be to require (1...<3) to always be parenthesized

[Eric Wieser]

Then {1...<3} (the range as a Set) and {(1...<3)} (a singleton) are distinguishable

[Eric Wieser]

Kyle Miller said:

Any reason not to embrace {a <...< b}, etc., using the new range syntax?

Are you proposing only embracing the syntax or additionally embracing Std.PRange?

[Kyle Miller]

Eric Wieser said:

Are you proposing only embracing the syntax or additionally embracing Std.PRange?

Either.

Option 1: Have Mathlib add a custom elaborator, where if e in {e} is a PRange syntax, then it elaborates to a Set.Ixx set. Pro: keeps in sync with the PRange syntaxes. Cons: custom elaborators add complexity, and this is a non-standard meaning of the Singleton syntax. In the unlikely event that a macro pieces together some syntax that includes a PRange in {_}, it will be interpreted in an unexpected way.

Option 2: Be inspired by the PRange syntax and create {a < ... < b} notation (maybe it needs higher priority to avoid being interpreted as a Singleton). Pros: less of a hack, hovering over the notation will certainly be able to explain what it does, don't need to wait on core for ≤ support, can pretty print it the way we want, don't need to accept the mathematically unfamiliar {a <... b} in pretty printing. Cons: won't necessarily be in sync with PRange syntax, but that might be ok.

In both cases, it might be worth having the underlying term be something like Set.ofPRange (a...b), though it might also be worth keeping the Set.Ixx functions as-is so that when people hover over the intervals and figure out what's going on without wading through a lot of stuff.

[François G. Dorais]

Why not just let users figure out what they prefer and let it converge? Top-down dictated notation is at least 80% a bad idea. Convergence is slow but it narrows down fast enough for a top decision to be made that is less than 20% a bad idea.

[Kyle Miller]

We're the users figuring it out @François G. Dorais. I've got my Mathlib maintainer hat on here; notation for Mathlib won't just happen without discussing what we'd prefer.

[Niels Voss]

Was PRange intended just for finite collections or also for Set? Is there any circumstance under which a <... b would be elaborated directly to Set.Ioo a b without requiring extra notation around a <... b? Imo this could cause problems

[François G. Dorais]

@Kyle Miller I think the tone of my earlier comment came out wrong. Apologies.

This discussion is important but it is also important to actually try these alternatives to see what works and what doesn't.

[Niels Voss]

Another option would be to have a <... b never elaborate to anything (not even a PRange object) unless there's some clue that indicates what type it would elaborate to. So like [a <... b] would elaborate to something like List.ofPRange (PRange.mk _ a b), #[a <... b] would elaborate to Array.ofPRange (PRange.mk _ a b), and {a <... b} would elaborate to Set.ofPRange (PRange.mk _ a b).

This should prevent the possibility of it being interpreted as a singleton

[Niels Voss]

Maybe then (a <... b) could be parsed as the PRange object directly, and a <... b by itself could act as an iterable in for statements for performance

[Kyle Miller]

@Niels Voss I believe the PRange object is meant to be an abstract interval. One of the main use cases you'd see in programming is for i in a <... b do ...

I could be mistaken, but I don't think these will be used as concrete data structures. Instead you write (a <... b).toList, etc.

[a <... b] is cute, but the ambiguity is a little unnerving. It feels Haskell, with its [a] instead of List a.

[Kyle Miller]

Using {a <...< b} has precedence in existing mathematical notation, which is a reason I personally think it's worth considering, despite the ambiguity (plus, in math, we likely will not be working with the abstract interval itself; abstract intervals do appear, but they'd show up using the language of category theory, not the language of Std.PRange).

[Niels Voss]

I agree that overloading [] beyond what's already done is not great. If a <... b is a valid expression by itself without parentheses, then I think that's problematic, because then [a <... b] could be parsed as a singleton. My suggestion was to make it so that a <... b doesn't parse unless surrounded by a delimiter of some type.

[Kyle Miller]

I get that, and that's why I mentioned for loops, where it would be nice not to have to insert delimiters.

I'd expect in most cases you don't want [a <... b] the list, since it's likely being immediately mapped over, so you'd want an iterator anyway. There seem to be very few use cases for reifying an interval, so requiring extra delimiters for for loops is more a burden than a help, I think.

[Eric Wieser]

This has reminded me of the one time I wrote ruby code, and immediately got it wrong: https://stackoverflow.com/a/12433441/102441

[Niels Voss]

Yeah, in that case, I think (a <... b).toList is fine notation, and then downstream projects can implement [a <... b] notation themselves if they think it is worth the parsing ambiguity

[Eric Wieser]

Kyle Miller said:

One of the main use cases you'd see in programming is for i in a <... b do _

My take on this is that forcing users to write for i in (a <... b) do _ would be no great loss, but I can see that I'm now playing with paint.

[Niels Voss]

what does "playing with paint" mean?

[Eric Wieser]

Kyle Miller said:

In both cases, it might be worth having the underlying term be something like Set.ofPRange (a...b), though it might also be worth keeping the Set.Ixx functions as-is so that when people hover over the intervals and figure out what's going on without wading through a lot of stuff.

Can we write a custom delaborator like we did for sup?

[Kyle Miller]

(@Niels Voss "choosing the color for a bikeshed")

[Eric Wieser]

I don't think keeping around both Icc and ofPRange and managing simp-normal forms will be a pleasant experience

[Niels Voss]

We could just add special parsing for for i in a <... b do _ where in ... do acts as the delimiter like [] or {}.

[Niels Voss]

though having to add special parsing for individual circumstances isn't great

[Floris van Doorn]

Eric Wieser said:

with x hard-coded as the name? {a < · < b} might be a better alternative

Earlier discussion about this: #mathlib4 > notation for intervals

[Kyle Miller]

(Continued discussion there.)

[Paul Reichert]

For those that were interested in this: I'm considering a recommended spelling for the Std ranges: lean4#10059

The spelling I'm proposing in this PR is to write, for example, Rco for a right-open bounded range, following Mathlib's naming of intervals. This should make it easier to name lemmas involving ranges.