Làm thế nào để hạn chế giả định thế giới mở trong Haskell

Question

Để nâng cao kiến ​​thức về các phần mở rộng GHC, tôi quyết định thử và thực hiện các số với các đơn vị. Một thứ tôi muốn làm là sử dụng các chữ số cho các giá trị đơn vị. Nhưng điều đó hóa ra là không thực tế do giả định thế giới mở mà Haskell tạo ra. Một ví dụ nhỏ về những gì tôi không thể bắt đầu làm việc như sau:

data Unit u a = Unit a 

data NoUnit 

instance Num a => Num (Unit NoUnit a) where 
    -- (+) (*) (-) abs signum not important 
    fromInteger = Unit . fromInteger 

type family Multiply a b where 
    Multiply NoUnit NoUnit = NoUnit 

multiply :: Num a => Unit u1 a -> Unit u2 a -> Unit (Multiply u1 u2) a 
multiply (Unit a) (Unit b) = Unit $ a * b 

Bây giờ nếu tôi cố gắng và làm điều gì đó như multiply 1 1 tôi mong đợi giá trị kết quả là rõ ràng. Bởi vì cách duy nhất để có được thứ gì đó thuộc loại Num (Unit u a) là bằng cách đặt u thành NoUnit. Và a còn lại phải được xử lý theo các quy tắc mặc định.

Thật không may do giả định thế giới mở của Haskell có thể là một số người xấu đã quyết định rằng ngay cả một số có đơn vị phải là một phiên bản Num hợp lệ mặc dù một điều như vậy sẽ vi phạm (*) :: a -> a -> a như phép nhân số với đơn vị không phù hợp với chữ ký kiểu đó.

Bây giờ giả định thế giới mở không phải là một giả định không hợp lý, đặc biệt là vì các phiên bản trẻ mồ côi không bị báo cáo Haskell cấm. Nhưng trong trường hợp cụ thể này, tôi thực sự muốn nói với GHC rằng loại đơn vị ảo hợp lệ duy nhất cho một ví dụ Num của Unit là NoUnit.

Có cách nào để nói rõ điều này, và về phần nào của một lưu ý phụ sẽ không cho phép trẻ mồ côi trường hợp cho phép GHC để dễ dàng lên trên giả định thế giới mở ở tất cả?

Loại điều này đã xuất hiện một vài lần khi cố gắng làm cho chương trình của tôi an toàn hơn với cách gõ phụ thuộc một phần. Bất cứ khi nào tôi muốn chỉ định một trường hợp Num hoặc IsString hoặc IsList cho trường hợp cơ sở và sau đó sử dụng các giá trị hoặc chức năng tùy chỉnh để có được tất cả các trường hợp có thể khác.

Answer 1

Bạn không thể tắt giả định thế giới mở, nhưng có nhiều cách để hạn chế nó, kể cả thời gian này. Vấn đề, trong trường hợp của bạn, là cách bạn viết Num dụ:

instance Num a => Num (Unit NoUnit a) 

gì bạn thực sự muốn được

instance (Num a, u ~ NoUnit) => Num (Unit u a) 

Bằng cách này, khi GHC thấy rằng nó cần Num (Unit u) a, nó kết luận rằng nó cần cả hai số Num a và u ~ NoUnit. Cách bạn viết nó, bạn còn lại mở khả năng của một số ví dụ bổ sung ở đâu đó.

Bí quyết của các nhà xây dựng kiểu biến ở bên phải của => đối với các ràng buộc bình đẳng ở bên trái thường hữu ích.