Bằng chứng về luật áp dụng cho các trường hợp haskell

Question

Có tất cả các trường hợp Haskell của typeclass áp dụng mà chúng tôi nhận được với nền tảng Haskell đã được chứng minh là đáp ứng tất cả các luật áp dụng? Nếu có, chúng tôi sẽ tìm thấy bằng chứng đó ở đâu?

Mã nguồn của Control.Applicative dường như không chứa bất kỳ bằng chứng nào cho thấy luật áp dụng cho các trường hợp khác nhau được giữ. Nó chỉ đề cập rằng

-- | A functor with application. 
-- 
--Instances should satisfy the following laws: 

Sau đó, chỉ nêu rõ luật trong nhận xét.

Tôi cũng tìm thấy một trường hợp tương tự cho các trường hợp của typeclasses khác (Alternative và Monad).

Người dùng của các thư viện này có phải tự xác minh các luật này không?

Nhưng tôi đã tự hỏi liệu bằng chứng nghiêm ngặt về các luật này đã được các nhà phát triển đưa ra ở nơi nào khác?

Một lần nữa, tôi biết rằng bằng chứng khắt khe về áp dụng (hoặc Monad) cho IO Monad, có liên quan đến nói chuyện với thế giới bên ngoài, nói chung, có thể rất phức tạp.

Cảm ơn.

Answer 1

Vâng, gánh nặng của bằng chứng hoàn toàn là trên các nhà văn thư viện. Có một số ví dụ về việc triển khai vi phạm các luật này. Ví dụ kinh điển về vi phạm pháp luật là ListT, không tuân thủ luật đơn lẻ đối với hầu hết các đơn vị cơ bản (xem examples). Điều này mang lại hành vi rất lỗi và không ai thực sự sử dụng kết quả là ListT.

Tôi khá chắc chắn rằng hầu hết các loại bằng chứng này chưa được khắc trên đá ở một nơi tiêu chuẩn. Hầu hết các bằng chứng đơn giản đã được lặp đi lặp lại và kiểm tra đến chết bởi các thành viên tò mò khác nhau của cộng đồng vì vậy sau một thời gian, chúng tôi biết những triển khai nào làm và không thỏa mãn luật của họ.

Để cung cấp cho một ví dụ cụ thể, khi tôi viết thư viện pipes của tôi, tôi phải chứng minh rằng tôi pipes đáp ứng các Category luật, nhưng tôi chỉ giữ những bằng chứng trong một tập tin văn bản hoặc một hpaste cho kỷ lục trong tương lai nếu ai đó yêu cầu chúng. Bao gồm cả họ trong nguồn là không thực sự khả thi bởi vì họ có thể nhận được rất dài, đặc biệt là cho các luật kết hợp.

Tuy nhiên, tôi nghĩ thực hành tốt có thể là bao gồm, khi có thể, bằng chứng được kiểm tra bằng máy trong kho gốc để người dùng có thể tham khảo chúng khi cần thiết.

Answer 2

Có thư viện tuyệt vời checkers cung cấp các thuộc tính QuickCheck để kiểm tra luật.

Answer 3

Thư viện thực nghiệm ghc-proofs phép bạn sử dụng trình biên dịch để xác minh pháp luật như vậy cho bạn:

app_law_2 a b (c :: Succs a) = pure (.) <*> a <*> b <*> c 
          === a <*> (b <*> c) 

Nó chỉ hoạt động trong một vài trường hợp, chẳng hạn như một trong những mô tả in my blog post, và tốt nhất là xem như một thí nghiệm , không phải là một công cụ sẵn sàng.