Xúc tiến kiểu dữ liệu cho các thách thức phụ thuộc

Question

Sau khi đọc qua ghc 7.4. ghi chú trước khi phát hành và giấy Giving Haskell a Promotion, tôi vẫn còn bối rối về những gì bạn thực sự làm với các loại quảng bá. Ví dụ: sách hướng dẫn GHC cung cấp các ví dụ sau về các kiểu dữ liệu được quảng cáo:

data Nat = Ze | Su Nat 

data List a = Nil | Cons a (List a) 

data Pair a b = Pair a b 

data Sum a b = L a | R b 

Loại sử dụng nào có dạng như vậy? Bạn có thể đưa ra các ví dụ (mã) không?

Answer 1

Nat có thể là ví dụ: được sử dụng để xây dựng các vectơ số chỉ có thể được thêm nếu chúng có cùng độ dài, được kiểm tra tại thời gian biên dịch.

Answer 2

Có ít nhất hai ví dụ trong giấy bản thân:

"1. Giới thiệu" nói: "Ví dụ, chúng ta có thể để đảm bảo [tại thời gian biên dịch] rằng một cây đỏ-đen bị cáo buộc thực sự có tài sản màu đỏ đen ".

"2.1 Loại dữ liệu quảng cáo" thảo luận về vectơ được lập chỉ mục độ dài (có nghĩa là, vectơ có lỗi "lập chỉ mục thời gian biên dịch").

Bạn cũng có thể xem xét công việc trước đó theo hướng này, ví dụ: Thư viện HList cho các danh sách không đồng nhất loại an toàn và các bộ sưu tập có thể mở rộng. Oleg Kiselyov có nhiều công trình liên quan. Bạn cũng có thể đọc các tác phẩm về lập trình với các loại phụ thuộc. http://www.seas.upenn.edu/~sweirich/ssgip/main.pdf có các ví dụ giới thiệu cho các phép tính mức loại trong Agda, nhưng chúng cũng có thể được áp dụng cho Haskell.

Nói chung, ý tưởng là head cho danh sách được cung cấp loại chính xác hơn. Thay vì

head :: List a -> a 

nó là

head :: NotEmptyList a -> a 

Chức năng đầu thứ hai là typesafe hơn fomer: nó không bao giờ có thể được áp dụng cho danh sách trống rỗng, vì nó sẽ gây ra lỗi biên dịch.

Bạn cần tính toán loại mức để thể hiện các loại như NotEmptyList. Gõ các lớp với các phụ thuộc chức năng, các nhóm GAGT và (được lập chỉ mục) đã cung cấp các dạng tính toán mức loại yếu cho haskell. Công việc bạn đề cập chỉ cần xây dựng thêm theo hướng này.

Xem http://www.haskell.org/haskellwiki/Non-empty_list để triển khai chỉ sử dụng các loại lớp Haskell98.