Open Kha opened 1 year ago
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:
Err... you are totally correct, my mind simply assumed it had to be mirrored!
Edit: edited
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.
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.
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.
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.
The current
Std.Range
in my experience has quite a few issues:
Nat
. It should work for anyType u
, with operations using appropriate type classes. The default arguments can probably be removed since we usually use notations to construct ranges.step
are extremely rare and complicate implementations of operations such asmem
(indeed, the current implementation simply ignores it!). If needed at all, stepping should rather become an generalStream
transformer, which I think could still lead to optimal code onRange
.[i:j]
is quite unconventional. The syntax most similar to it is lists, which it is not. While it looks nice inxs[i:j]
, one would be forgiven for thinking the range part isi:j
, not the whole[i:j]
. Indeed, this is problematic for e.g. trying to extend the syntax to multiple dimensions as inm[1:2, 3:]
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:a..b
a<..b
,a..<b
,a<..<b
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 introducea..=b
inclusive ranges at a much later point.