Haskell/GHC UndecidableInstances - ví dụ về kiểm tra loại không chấm dứt?

Question

Tôi đã viết một số mã Haskell cần -XundecidableInstances để biên dịch. Tôi hiểu tại sao điều đó xảy ra, rằng có một điều kiện nhất định bị vi phạm và do đó GHC hét lên.

Tuy nhiên, tôi chưa bao giờ gặp phải tình huống mà trình kiểm tra loại thực sự treo hoặc cuộn lên trong vòng lặp vô tận.

Định nghĩa cá thể không chấm dứt trông như thế nào - bạn có thể đưa ra ví dụ không?

Answer 1

Ví dụ:

{-# LANGUAGE UndecidableInstances #-} 

class C a where 
    f :: a -> a 

instance C [[a]] => C [a] where 
    f = id 

g x = x + f [x] 

gì đang xảy ra: Khi gõ f [x] trình biên dịch cần phải đảm bảo rằng x :: C [a] đối với một số a. Khai báo cá thể nói rằng x có thể thuộc loại C [a] chỉ khi nó cũng thuộc loại C [[a]]. Vì vậy, trình biên dịch cần phải đảm bảo rằng x :: C [[a]], v.v. và bị bắt trong một vòng lặp vô hạn.

Xem thêm Can using UndecidableInstances pragma locally have global consequences on compilation termination?

Answer 2

Có một cổ điển, một chút ví dụ đáng báo động (liên quan đến sự tương tác với phụ thuộc hàm) trong this paper from HQ:

class Mul a b c | a b -> c where 
    mul :: a -> b -> c 
instance Mul a b c => Mul a [b] [c] where 
    mul a = map (mul a) 

f b x y = if b then mul x [y] else y 

Chúng ta cần mul x [y] có cùng loại như y, vì vậy, lấy x :: x và y :: y, chúng tôi cần

instance Mul x [y] y 

whi ch, theo trường hợp nhất định, chúng ta có thể có. Dĩ nhiên, chúng ta phải mất y ~ [z] đối với một số z mà

instance Mul x y z 

ví dụ:

instance Mul x [z] z 

và chúng tôi đang ở trong một vòng lặp.

Thật đáng lo ngại, vì ví dụ Mul có vẻ như đệ quy của nó là cấu trúc giảm, không giống như trường hợp bệnh lý rõ ràng trong câu trả lời của Petr. Tuy nhiên, nó làm cho vòng lặp GHC (với ngưỡng nhàm chán đá vào để tránh treo).

Sự cố, vì tôi chắc chắn rằng tôi đã đề cập ở đâu đó một cách khác biệt, là việc nhận dạng y ~ [z] được thực hiện mặc dù thực tế là z phụ thuộc chức năng trên y. Nếu chúng ta sử dụng một ký pháp chức năng cho sự phụ thuộc chức năng, chúng ta có thể thấy rằng ràng buộc nói y ~ Mul x [y] và từ chối sự thay thế như vi phạm kiểm tra xuất hiện.

Bị kích thích, tôi nghĩ rằng tôi muốn cung cấp cho này một whirl,

class Mul' a b where 
    type MulT a b 
    mul' :: a -> b -> MulT a b 

instance Mul' a b => Mul' a [b] where 
    type MulT a [b] = [MulT a b] 
    mul' a = map (mul' a) 

g b x y = if b then mul' x [y] else y 

Với UndecidableInstances được kích hoạt, nó mất nhiều thời gian cho vòng lặp để thời gian ra. Với UndecidableInstances bị tắt, phiên bản vẫn được chấp nhận và máy đánh chữ vẫn lặp lại, nhưng việc cắt bỏ diễn ra nhanh hơn nhiều.

Vì vậy, ... thế giới cũ vui nhộn.