Chuyển đổi một ràng buộc lớp tùy ý `C a` thành` C a Bool`

Question

Vì vậy, có rất nhiều ưu điểm khi có typeclasses ở dạng C a Bool. Chủ yếu là vì chúng cho phép bạn thực hiện bất kỳ thao tác lôgic nào giữa hai ràng buộc khi thông thường C a chỉ ngầm ẩn tất cả mọi thứ.

Nếu chúng ta xem xét ~ một hạn chế lớp, điều này có thể được thực hiện như vậy

class Equal x y b | x y -> b 
instance Equal x x True 
instance False ~ b => Equal x y b 

Nhưng những gì làm cho trường hợp này đặc biệt là một thực tế rằng việc đưa x x vào đầu của các ví dụ tương đương với x ~ y => và sau đó x y trong đầu. Đây không phải là trường hợp cho bất kỳ typeclass khác. Vì vậy, nếu chúng ta cố gắng làm điều gì đó tương tự cho một lớp C chúng tôi nhận một cái gì đó giống như

class C' x b | x -> b 
instance C x => C' x True 
instance False ~ Bool => C' x b 

Thật không may điều này không làm việc kể từ khi chỉ là một trong những trường hợp đó bao giờ sẽ được chọn vì họ không phân biệt đối xử vào loại x vì vậy bất kỳ loại nào khớp với cả hai đầu.

Tôi cũng đọc https://www.haskell.org/haskellwiki/GHC/AdvancedOverlap lại không áp dụng cho bất kỳ lớp học nào C vì yêu cầu bạn viết lại tất cả các phiên bản của lớp gốc. Lý tưởng nhất, tôi muốn mã của tôi để làm việc với GHC.Exts.Constraint và KindSignatures để C có thể tham số.

Vì vậy, đối với một lớp học như thế này

class Match (c :: * -> Constraint) x b | c x -> b 

Làm thế nào để viết các trường hợp để Match c x True khi và chỉ khi c x, Match c x False khác?

Answer 1

Điều này là không thể trong Haskell do cái gọi là Giả định thế giới mở. Nó nói rằng tập hợp các cá thể cho typeclasses được mở, có nghĩa là bạn có thể tạo các cá thể mới bất kỳ lúc nào (trái ngược với một thế giới khép kín, nơi phải có một tập hợp các cá thể cố định). Ví dụ, trong khi Functor typeclass được định nghĩa trong Prelude, tôi vẫn có thể tạo các cá thể cho nó trong mã của riêng tôi mà không có trong Prelude.

Để thực hiện những gì bạn đã đề xuất, trình biên dịch sẽ cần cách kiểm tra xem loại T là phiên bản của lớp C. Tuy nhiên, điều này đòi hỏi trình biên dịch biết tất cả các trường hợp có thể của lớp đó và điều đó là không thể vì giả định thế giới mở (trong khi biên dịch Prelude, một trình biên dịch chưa biết rằng sau này bạn cũng làm cho YourOwnFunctor một cá thể của Functor).

Cách duy nhất để làm cho nó hoạt động là chỉ xem xét các trường hợp hiện đang hiển thị (vì chúng được xác định trong mô-đun hiện tại hoặc bất kỳ nhập nào của nó). Nhưng điều đó sẽ dẫn đến hành vi khá khó đoán: tập các trường hợp hiển thị không chỉ phụ thuộc vào việc nhập khẩu mô-đun, mà còn phụ thuộc vào nhập khẩu của các nhập khẩu vì bạn không thể ẩn các cá thể. Vì vậy, hành vi của mã của bạn sẽ phụ thuộc vào chi tiết triển khai của các phụ thuộc của bạn.

Nếu bạn muốn có một thế giới khép kín, thay vào đó bạn có thể sử dụng closed type families, được giới thiệu trong GHC 7.8. Sử dụng chúng, bạn có thể viết:

type family Equal a b :: Bool where 
    Equal x x = True 
    Equal x y = False