[RFC] Revise `Std.Range`

[Kha]

The current Std.Range

structure Range where
  start : Nat := 0
  stop  : Nat
  step  : Nat := 1

in my experience has quite a few issues:

• It is unnecessarily limited to Nat. It should work for any Type u, with operations using appropriate type classes. The default arguments can probably be removed since we usually use notations to construct ranges.
• Non-trivial uses of step are extremely rare and complicate implementations of operations such as mem (indeed, the current implementation simply ignores it!). If needed at all, stepping should rather become an general Stream transformer, which I think could still lead to optimal code on Range.
• The literal syntax [i:j] is quite unconventional. The syntax most similar to it is lists, which it is not. While it looks nice in xs[i:j], one would be forgiven for thinking the range part is i:j, not the whole [i:j]. Indeed, this is problematic for e.g. trying to extend the syntax to multiple dimensions as in m[1:2, 3:]
• If we are looking for new syntax anyway, we might as well make sure to find one that is acceptable to mathematicians and covers their needs as well
• Oh and it probably should be moved out of Std given that we're unlikely to remove it from core.

My proposal is to build on top of a simple .. infix syntax and include all the variations present in mathlib:

• inclusive intervals a..b
• exclusive bounds a<..b, a..<b, a<..<b
• infinite/elided bounds a.., ..b, a<.., ..<b, ..

This could be implemented either as separate types, or as a single type taking two bounds that individually encode one of the three above choices.

Note that while this is partially inspired by Rust's a..b, that syntax is in fact a right-exclusive interval! But that seems like an extremely poor fit for potential openness in both directions, and it is not clear to me whether Rust would have made that choice if they had known at the time that they would introduce a..=b inclusive ranges at a much later point.

[JamesGallicchio]

Syntax bikeshedding: I'm a bit confused why the syntax for exclusive lower bound uses >. I expected a<..b :thinking: is there a good reason to use > there?

Otherwise I would be very happy to see this implemented! :smile:

[Kha]

Err... you are totally correct, my mind simply assumed it had to be mirrored!

Edit: edited

[tydeu]

Note that while this is partially inspired by Rust's a..b, that syntax is in fact a right-exclusive interval! But that seems like an extremely poor fit for potential openness in both direction...

If we need some more justification for the approach of this RFC over Rust's, the a..b syntax is also used for inclusive ranges in both Ruby and Perl.

[sullyj3]

It is unnecessarily limited to Nat. It should work for any Type u, with operations using appropriate type classes.

As a data point, I ran into a situation today where a range of Fin would be really nice.

[j-loreaux]

Just to note: Mathlib does use the syntax a..b for something already: intervalIntegral

That's not to say it should necessarily prevent using it for this. I'm only noting the conflict.

[urkud]

In case of interalIntegral, the .. notation causes issues when I try to use it as ∫ x in 0..1, x, because it parses 0. as a Float before recognizing ... I have to use ∫ x in (0)..1, x instead. Probably, this can be fixed by changing some priorities, but this has to be done, if you're going to change notation.

[javra]

We could also use this for the Sail->Lean project for which I cobbled together this version for Int.

While that's enough for us, obviously a more general case with an Int step could also be useful. Could a first step towards more generality just be to have a type class for the range, keeping the current notation?

[Kha]

Closing for now, @datokrat will be working on this and related topics and is aware of this RFC but should not feel tied to it :)