Zulip Chat Archive

Stream: lean4

Topic: Array boundary check


๐Ÿ‘€๏ผŸ (Dec 07 2022 at 00:37):

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

๐Ÿ‘€๏ผŸ (Dec 07 2022 at 00:38):

Is this a bug?

๐Ÿ‘€๏ผŸ (Dec 07 2022 at 00:40):

The error is not reported until it is evaluated

Jason Rute (Dec 07 2022 at 00:49):

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 (Dec 07 2022 at 00:50):

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 (Dec 07 2022 at 00:51):

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

Jason Rute (Dec 07 2022 at 00:57):

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 (Dec 07 2022 at 01:08):

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

Jason Rute (Dec 07 2022 at 01:11):

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


Last updated: Dec 20 2023 at 11:08 UTC