Why is there no `OfInt` analogous to `OfNat`?

Stream: general

[samuela]

I am not able to find such a thing, but it would be convenient. In particular I would like to be able to do the following:

inductive SliceTerm where
  | sliceix : Int -> SliceTerm

instance : OfNat SliceTerm n where
  ofNat := .sliceix n

-- This doesn't seem to have any effect:
instance : Coe Int SliceTerm where
  coe := fun n => .sliceix n

syntax "test[" term,* "]" : term
macro_rules
| `(test[$ix,*]) => `(let foo : List SliceTerm := [$ix,*]; foo)

-- This works fine:
example : test[1] = [.sliceix 1] := rfl

-- Want to support negative indexing a la numpy, but these fail
-- "failed to synthesize Neg SliceTerm"
set_option diagnostics true
example : test[-1] = [.sliceix (-1)] := rfl
example : test[(-1)] = [.sliceix (-1)] := rfl

is there another way that i'm missing? how does one use Int's like this?

[Kim Morrison]

Define a new GetElem instance that takes Int as the index type.

[samuela]

IIUC the connection with GetElem here is mostly coincidental. This is a snippet extracted from a larger bit of code designed to support indexing on multiple axes of an array which I believe goes beyond what GetElem allows:

inductive NonEllipsisSliceTerm where
  | Singleton : Int -> NonEllipsisSliceTerm
  | NewAxis : NonEllipsisSliceTerm
  | Colon : NonEllipsisSliceTerm
deriving BEq

inductive SliceTerm where
  | Other : NonEllipsisSliceTerm -> SliceTerm
  | Ellipsis : SliceTerm
deriving BEq

instance : OfNat SliceTerm n where
  ofNat := .Other (.Singleton n)

instance : Coe Int SliceTerm where
  coe := fun n => .Other (.Singleton n)

syntax "..." : term
macro_rules
| `(...) => `(SliceTerm.Ellipsis)

syntax "newaxis" : term
macro_rules
| `(newaxis) => `(.Other .NewAxis)

syntax ":" : term
macro_rules
| `(:) => `(.Other .Colon)

syntax "test[" term,* "]" : term

macro_rules
| `(test[$ix,*]) => `(let foo : List SliceTerm := [$ix,*]; foo)

example : test[...] = [.Ellipsis] := rfl

#check test[...]
#check test[1, ...]
#check test[1, :, ...]
#check test[1, :, :, ...]
#check test[1, :, :, :, ...]
#check test[1, ...]
#check test[1, :, ...]
#check test[1, :, :, ...]
#check test[1, ..., 6]
#check test[0, ..., 0, ..., 0]
#check test[..., newaxis]
#check test[..., 0, newaxis, 0]
#check test[0]
#check test[(-1)]
#check test[-1]
#check test[-6]

Would GetElem support comma-separated values as keys/indices? If so, that would be great. I was under the impression that was not possible

[Kim Morrison]

No, GetElem is already complicated enough and we don't intend to add features like this.

[Chris Bailey]

Alternatively you can add a Neg instance example.

[Eric Wieser]

samuela said:

Would GetElem support comma-separated values as keys/indices? If so, that would be great. I was under the impression that was not possible

This seems RFC worthy to me, especially if you compare to how other languages support this in that RFC. Perhaps now is not the time for Lean to start working on this, an RFC would be something to link next time this comes up

[samuela]

Chris Bailey said:

Alternatively you can add a Neg instance example.

My concern here is that this allows negating things like newaxis: example

Eric Wieser said:

samuela said:

Would GetElem support comma-separated values as keys/indices? If so, that would be great. I was under the impression that was not possible

This seems RFC worthy to me, especially if you compare to how other languages support this in that RFC. Perhaps now is not the time for Lean to start working on this, an RFC would be something to link next time this comes up

This is the sort of thing I would happily updoot. Not sure how the powers that be feel towards the current GetElem. Personally I don't mind the hassle of defining custom syntax, so long as it's possible to get that custom syntax to work with integers

[Niels Voss]

Another option is to not use a minus sign at all and instead use something like arr[←1] to access from the end of the array. Maybe there's some advantage to negative numbers I'm not aware of, but it seems like it can cause arithmetic bugs to lead to accessing random elements of the array rather than crashing, which is better.

[samuela]

There's a fair amount of numpy code that does arithmetic to access things on the "negative" side of the array, eg arr[-i-1]. I suppose it's debatable whether this is good or not

[Eric Wieser]

You could consider writing a more interesting custom elaborator here that first tries to elaborate the argument as an Int before falling back on the general setting

[Eric Wieser]

That would allow -1 to just work

[Alex Meiburg]

I like Niels' suggestion. Julia has a similar thing where you write arr[end-i] for what Python calls arr[-i]. I think a lot of people agree that Numpy's indexing was a bit of hack that had to work with the syntax Python had available to overload; other languages have tried to do better, and I think Lean should be one such.

Allowing /negative integers/ to just happen to wrap around like that, is really responsible for a ton of logic bugs in software these days. Often vulnerabilities too. And yes, Lean has proofs, but I think it would be a big easy thing to mess up on the spec.

[Violeta Hernández]

I agree, to me negative indexing seems like a lot of work for buggier code that adds no new functionality.

[Kenny Lau]

we have Fin.rev you know...

[samuela]

To clarify: the goal is not to design a "good" array indexing system. The goal is to model numpy in lean, warts and all