Làm cách nào để kết hợp hai loại ràng buộc với một lôgic hoặc trong Haskell?

Question

Trong Haskell, chúng tôi có khả năng kết hợp các ràng buộc trên các loại với một lôgic và.

Hãy xem xét những điều sau

type And (a :: Constraint) b = (a, b) 

hoặc phức tạp hơn

class (a, b) => And a b 
instance (a, b) => And a b 

Tôi muốn biết làm thế nào để hợp lý hoặc hai khó khăn cùng nhau trong Haskell.

Cố gắng gần nhất của tôi là điều này, nhưng nó không hoạt động. Trong lần thử này, tôi sửa lại các ràng buộc kiểu với các thẻ và hơn là xác định chúng với các tham số ngầm định.

data ROr a b where 
L :: a => ROr a b 
R :: b => ROr a b 

type Or a b = (?choose :: ROr a b) 

y :: Or (a ~ Integer) (Bool ~ Integer) => a 
y = case ?choose of 
L -> 4 

x :: Integer 
x = let ?choose = L in y 

Nó hầu như hoạt động, nhưng người dùng phải áp dụng phần cuối cùng và trình biên dịch nên làm điều đó cho tôi. Đồng thời, trường hợp này không cho phép người ta chọn lựa chọn thứ ba khi cả hai ràng buộc đều được thỏa mãn.

Làm cách nào để hợp lý hoặc hai ràng buộc với nhau?

Answer 1

Tôi tin rằng không có cách nào để tự động chọn ROr a b; nó sẽ vi phạm giả định thế giới mở nếu, ví dụ b đã được hài lòng, nhưng sau đó cũng được đáp ứng a; bất kỳ quy tắc giải quyết xung đột nào cũng sẽ gây ra sự bổ sung một cá thể để thay đổi hành vi của mã hiện có.

Đó là, chọn R khi b là hài lòng nhưng a không được phá vỡ giả định thế giới mở, bởi vì nó liên quan đến quyết định rằng một thể hiện là không hài lòng; ngay cả khi bạn thêm một hàm tạo "hài lòng", bạn có thể sử dụng nó để quyết định xem một cá thể là không phải là (bằng cách xem bạn có nhận được L hoặc R) hay không.

Do đó, tôi không tin rằng có thể có ràng buộc hoặc này; nếu bạn có thể quan sát cá thể nào bạn nhận được, thì bạn có thể tạo một chương trình có hành vi thay đổi bằng cách thêm một cá thể, và nếu bạn không thể quan sát cá thể nào bạn nhận được, thì nó khá vô ích.

Sự khác biệt giữa độ phân giải thể hiện bình thường và điều này cũng có thể thất bại, bình thường, trình biên dịch không thể quyết định rằng một ràng buộc được thỏa mãn; ở đây, bạn đang yêu cầu trình biên dịch quyết định rằng ràng buộc không thể được thỏa mãn. Một sự khác biệt tinh tế nhưng quan trọng.