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數組的靜態邊界檢查

回答

相關問題