arrays - 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 中找到的那种系统。让这样的事情成为可能。