Haskell数组的静态边界检查

有没有什么办法可以在Haskell数组上进行静态检查？让我们利用这个代码：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)，但是编译器接受的代码。尽管可以在编译时检测到错误，但只能在运行时检测错误。

来源

2012-03-17 quant_dev

也许可以在这种情况下检测* * **如果编译器做了大量的内联和常量折叠以达到无条件的'error'（或其他）调用。在大多数非平凡计划中，至少不能通过合理的努力来检测它。然后有这个讨厌的暂停问题... – delnan 2012-03-17 18:57:44

使用[习惯]（http://hasp.cs.pdx.edu/habit-report-Nov2010.pdf）（PDF）Ix类型获得界限的静态保证。如果您将此工作移植到Haskell，则可获得奖励积分。 – 2012-03-17 19:06:58

有一种方法，但实际上太不方便了。有关这方面的更多信息，请尝试在网上搜索“类型号码haskell”。 – 2012-03-17 20:25:18

在编译时无法检测到这种情况，因为列表中没有任何内容可以保存其大小，所以listArray函数不可能执行此类检查。另外，如果数据来自外部文件（例如），那么要使静态大小检查正常工作将非常困难。

您需要一个依赖类型系统，例如您在Agda中找到的依赖类型系统。

来源

2012-03-17 18:58:07 dflemstr

创建的内容不是列表，而是数组（Data.Array）。 – 2012-03-18 07:20:49

是的，但是您正在使用列表来创建数组。你做'listArray（start，end）someList'。 – dflemstr 2012-03-18 11:34:47

但是在这段代码中，'someList'显式地提供给编译器，所以它可以轻松地进行检查。但我想我现在明白了：Data.Array不是原生的Haskell类型。 – 2012-03-18 11:37:53

Haskell数组的静态边界检查

回答

相关问题