Menu
Is there any way to get static checks on Haskell arrays? Let's take this code:
import Data.Array
let a = listArray (0, 10) [-3.969683028665376e+01, 2.209460984245205e+02, -2.759285104469687e+02, 1.383577518672690e+02, -3.066479806614716e+01, 2.506628277459239e+00]
(0, 10) should really be (0, 5), but the compiler accepts the code. The error is only detected at runtime, despite the fact that it could be detected at compile-time.
413
Yes, checking if the index is within the bounds of the array.
Array bound checking refers to determining whether all array references in a program are within. their declared ranges. This checking is critical for software verification and validation because. subscripting arrays beyond their declared sizes may produce unexpected results, security holes, or failures.
Bounds checking is easy for arrays because the array subscript syntax specifies both the address calculation and the array within which the resulting pointer should point. With pointers in C, a pointer can be used in a context divorced from the name of the storage region for which it is valid.
This cannot be detected at compile-time, because there's nothing in the list's type that saves its size, so the listArray function cannot possibly perform such checks. Also, if the data came from an external file (for example), it would be very difficult to get the static size checking to work.
You need a dependent type system such as the one you find in Agda for things like this to be possible.
60
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
