Kiểm tra giới hạn tĩnh trên mảng Haskell

Question

Có cách nào để kiểm tra tĩnh trên mảng Haskell không? Chúng ta hãy xem đoạn mã này:

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) thực sự nên (0, 5), nhưng trình biên dịch chấp nhận mã. Lỗi này chỉ được phát hiện trong thời gian chạy, mặc dù thực tế là nó có thể được phát hiện tại thời gian biên dịch.

Answer 1

Điều này không thể được phát hiện tại thời gian biên dịch, vì không có gì trong loại danh sách tiết kiệm kích thước của nó, do đó, chức năng listArray không thể thực hiện kiểm tra như vậy. Ngoài ra, nếu dữ liệu đến từ một tập tin bên ngoài (ví dụ), nó sẽ rất khó khăn để kiểm tra kích thước tĩnh hoạt động.

Bạn cần hệ thống loại phụ thuộc như hệ thống bạn tìm thấy trong Agda cho những việc như thế này để có thể.