Sự khác biệt giữa Haskell và Idris: Sự phản ánh của Runtime/Compiletime trong các loại vũ trụ

Question

Vì vậy, trong Idris nó hoàn toàn hợp lệ để viết như sau.

item : (b : Bool) -> if b then Nat else List Nat 
item True = 42 
item False = [1,2,3] // cf. https://www.youtube.com/watch?v=AWeT_G04a0A 

Không có chữ ký loại, điều này trông giống như ngôn ngữ được nhập động. Nhưng, quả thật vậy, Idris được đánh máy một cách phụ thuộc. Loại bê tông item b chỉ có thể được xác định trong thời gian chạy.

Đây là, tất nhiên, một lập trình viên Haskell nói: Loại item b trong ý nghĩa Idris được đưa ra trong thời gian biên dịch, nó là if b then Nat ....

Bây giờ câu hỏi của tôi: Tôi có quyền kết luận rằng trong Haskell, ranh giới giữa thời gian chạy và compiletime chạy chính xác giữa thế giới của các giá trị (False, "foo", 3) và thế giới của các loại (Bool, String , Integer) trong khi ở Idris, biên giới giữa thời gian chạy và compiletime đi qua vũ trụ? Ngoài ra, tôi có quyền giả định rằng ngay cả với các loại phụ thuộc trong Haskell (sử dụng DataKinds và TypeFamilies, xem this article) ví dụ trên là không thể trong Haskell, vì Haskell trái với Idris không cho phép các giá trị bị rò rỉ cho loại -cấp độ?

Answer 1

Có, bạn có quyền quan sát thấy sự khác biệt về loại so với giá trị trong Idris không phù hợp với phân biệt compiletime-only so với runtime-and-compiletime. Đó là một điều tốt. Nó rất hữu ích để có các giá trị chỉ tồn tại ở chế độ compiletime, giống như trong các chương trình logic, chúng ta có "các biến ma" chỉ được sử dụng trong các đặc tả. Nó cũng hữu ích để có các biểu diễn kiểu tại thời gian chạy, cho phép lập trình kiểu dữ liệu chung.

Trong Haskell, DataKinds (và PolyKinds) chúng ta hãy viết

type family Cond (b :: Bool)(t :: k)(e :: k) :: k where 
    Cond 'True t e = t 
    Cond 'False t e = e 

và trong tương lai không xa, chúng ta sẽ có thể viết

item :: pi (b :: Bool) -> Cond b Int [Int] 
item True = 42 
item False = [1,2,3] 

nhưng cho đến khi công nghệ được thực hiện, chúng tôi phải thực hiện với các loại giả đơn lẻ của các loại chức năng phụ thuộc, như sau:

data Booly :: Bool -> * where 
    Truey :: Booly 'True 
    Falsey :: Booly 'False 

item :: forall b. Booly b -> Cond b Int [Int] 
item Truey = 42 
item Falsey = [1,2,3] 

Bạn có thể nhận được khá xa với fakery như vậy, nhưng nó sẽ tất cả nhận được rất nhiều dễ dàng hơn nếu chúng ta chỉ có thật.

Điều quan trọng, kế hoạch cho Haskell là duy trì và tách biệt forall và pi, hỗ trợ đa hình và tham số đặc biệt, tương ứng. Các lambdas và các ứng dụng đi kèm với forall vẫn có thể bị xóa trong quá trình tạo mã thời gian chạy, giống như bây giờ, nhưng các ứng dụng cho pi được giữ lại. Nó cũng sẽ có ý nghĩa để có kiểu trừu tượng kiểu thời gian chạy pi x :: * -> ... và ném tổ hợp của chuột phức tạp đó là Data.Typeable vào thùng rác.

Answer 2

Bây giờ câu hỏi của tôi: Tôi có quyền kết luận rằng trong Haskell, biên giới giữa thời gian chạy và compiletime chạy chính xác giữa các thế giới các giá trị (False, "foo", 3) và thế giới của các loại (Bool, String, Integer) trong khi ở Idris, biên giới giữa thời gian chạy và compiletime đi qua vũ trụ?

Idris biên dịch để Epic (UPDATE: không, nó không còn biên dịch để Epis như Spearman nói trong bình luận dưới đây):

Không kiểm tra ngữ nghĩa, khác hơn là để xem nếu tên nằm trong phạm vi --- nó giả định rằng ngôn ngữ cấp cao hơn sẽ thực hiện đánh máy, và trong mọi trường hợp, Epic sẽ không đưa ra giả định về hệ thống loại cấp cao hơn hoặc bất kỳ biến đổi nào bạn đã áp dụng. Chú thích loại là bắt buộc, nhưng chúng chỉ đưa ra gợi ý cho trình biên dịch (tôi có thể thay đổi điều này).

Vì vậy, các loại không quan trọng mang tính quốc tế, tức là ý nghĩa của cụm từ không phụ thuộc vào loại của từ đó. Hơn nữa, một số thứ mức giá trị có thể bị xóa, ví dụ: trong Vect n A (nơi Vect là loại danh sách với chiều dài tĩnh biết) n (chiều dài) có thể được xoá hoàn toàn, because

Có nhiều phương pháp được mô tả bởi Brady, McBride và McKinna trong BMM04 để loại bỏ các chỉ số từ dữ liệu cấu trúc, khai thác thực tế rằng các chức năng của hoạt động trên chúng hoặc đã có một bản sao của chỉ số thích hợp hoặc chỉ mục có thể được xây dựng lại nhanh chóng nếu cần.

Điều ở đây là pi trong Idris hoạt động với nhiều loại trong hầu theo cùng một cách như forall trong Haskell: họ là cả hai tham số (tuy nhiên, những parametricities là khác nhau) trong trường hợp này. Trình biên dịch có thể sử dụng các loại để tối ưu hóa mã, nhưng trong cả hai ngôn ngữ kiểm soát dòng chảy không phụ thuộc vào loại, tức là bạn không thể nói if A == Int then ... else ... (mặc dù, nếu A là ở dạng kinh điển, sau đó bạn biết tĩnh cho dù đó là Int hay không và do đó can ghi A == Int, nhưng điều đó vẫn không ảnh hưởng đến luồng điều khiển, bởi vì tất cả các quyết định được thực hiện trước khi chạy). Loại bê tông item b không quan trọng khi chạy.

Tuy nhiên, như pigworker nói rằng không nhất thiết phải tham số theo loại. Cũng như nó không nhất thiết phải không tham số trong các giá trị. Loại cấp - giá trị cấp và tham số - phi tham số là các hàm lưỡng hoàn toàn trực giao. Xem this câu trả lời để biết chi tiết. Vì vậy, Haskell và Idris là khác nhau trong cách họ xử lý những thứ cấp giá trị wrt thời gian chạy/biên dịch nội dung (bởi vì trong Idris bạn có thể đánh dấu một đối số với . để làm cho nó erasable), nhưng họ đối xử với các loại theo cùng một cách.