Haskell数组上的静态边界检查

Question

有没有办法在Haskell数组上进行静态检查？我们来看看这段代码:

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)应该是(0, 5),但编译器接受代码.该错误仅在运行时检测到,尽管它可以在编译时检测到.

Answer 1

这在编译时无法检测到,因为列表类型中没有任何内容可以保存其大小,因此该listArray函数无法执行此类检查.此外,如果数据来自外部文件(例如),则很难让静态大小检查工作.

您需要一个依赖类型系统,例如您在Agda中找到的类似系统,这样的事情是可能的.