Static Haskell Array Border Checks

Question

Is there a way to get static checks on Haskell arrays? 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)It should be valid (0, 5), but the compiler accepts the code. An error is detected only at runtime, although it could be detected at compile time.

Answer 1

This cannot be detected at compile time because nothing is stored in the list type, so the function listArraycannot perform such checks. Also, if the data comes from an external file (for example), it would be very difficult to get the static size check to work.

For such things, you need a dependent type system, such as the one you find in Agda .