Array boundary check

Stream: lean4

[👀？]

def mkArray' (l : Nat) (v : Nat) := (mkArray l 0).set! l v

[👀？]

Is this a bug?

[👀？]

The error is not reported until it is evaluated

[Jason Rute]

The docs4#Array.get! with the !gives a runtime error. Logically it evaluates to a default value if out of bounds for the sake of theorem proving. That is why the type must be inhabited.

[Jason Rute]

def l := [1, 2, 3]
def e := ([] : List Nat)

#eval l.get (2 : Fin 3)  -- 3  (Index is in `Fin (l.length)`, not `Nat`.)
#eval l[(2 : Fin 3)]     -- 3  (Short hand for l.get)
#eval e[(2 : Fin 0)]     -- Fails to compile.  Fin 0 is empty.

#eval l.get? 2   -- some 3  (Answer is an Option.)
#eval l[2]?      -- some 3  (Answer is an Option.)
#eval e[2]?      -- none    (Answer is an Option.)

#eval l.get! 2  -- 3
#eval l[2]!     -- 3
#eval e[2]!     -- 0  (If run in `#eval`, gives default value for `Nat`, which is 0)
                --     If run inside `main : IO unit`, gives runtime error.)

#eval l.getD 2 100  -- 3
#eval e.getD 2 100  -- 100  (We supplied a default value.)

[Jason Rute]

(Code copied from a PA.SE answer of mine.)

[Jason Rute]

While proving that the index is in bounds or using an Option are the safest, sometimes it is most expedient to use the version with the runtime error if you know your code won’t make an out of bounds access. IMHO get! is better than getD, since you know when your code is broken, whereas getD will just silently return garbage.

[Jason Rute]

Sorry, you are referring to docs4#Array.set! (not get!).

[Jason Rute]

Mathematically, it is the same as docs4#setD which is a no-op if the index is out of bounds.