Bạn có an toàn khi sử dụng unsafeCoerce cho các số dư hợp lệ không?

Question

Tôi có một loại chứng cho danh sách loại cấp,

data List xs where 
    Nil :: List '[] 
    Cons :: proxy x -> List xs -> List (x ': xs) 

cũng như các tiện ích sau đây.

-- Type level append 
type family xs ++ ys where 
    '[] ++ ys = ys 
    (x ': xs) ++ ys = x ': (xs ++ ys) 

-- Value level append 
append :: List xs -> List ys -> List (xs ++ ys) 
append Nil ys = ys 
append (Cons x xs) ys = Cons x (append xs ys) 

-- Proof of associativity of (++) 
assoc :: List xs -> proxy ys -> proxy' zs -> ((xs ++ ys) ++ zs) :~: (xs ++ (ys ++ zs)) 
assoc Nil _ _ = Refl 
assoc (Cons _ xs) ys zs = case assoc xs ys zs of Refl -> Refl 

Bây giờ, tôi có hai định nghĩa khác nhau nhưng tương đương với một chức năng ngược lại loại cấp,

-- The first version, O(n) 
type Reverse xs = Rev '[] xs 
type family Rev acc xs where 
    Rev acc '[] = acc 
    Rev acc (x ': xs) = Rev (x ': acc) xs 

-- The second version, O(n²) 
type family Reverse' xs where 
    Reverse' '[] = '[] 
    Reverse' (x ': xs) = Reverse' xs ++ '[x] 

Đầu tiên là hiệu quả hơn, nhưng thứ hai là dễ dàng hơn để sử dụng khi chứng minh điều cần trình biên dịch , vì vậy nó sẽ là tốt đẹp để có một bằng chứng về sự tương đương. Để thực hiện việc này, tôi cần bằng chứng là Rev acc xs :~: Reverse' xs ++ acc. Đây là những gì tôi nghĩ ra:

revAppend :: List acc -> List xs -> Rev acc xs :~: Reverse' xs ++ acc 
revAppend _ Nil = Refl 
revAppend acc (Cons x xs) = 
    case (revAppend (Cons x acc) xs, assoc (reverse' xs) (Cons x Nil) acc) of 
     (Refl, Refl) -> Refl 

reverse' :: List xs -> List (Reverse' xs) 
reverse' Nil = Nil 
reverse' (Cons x xs) = append (reverse' xs) (Cons x Nil) 

Thật không may, revAppend là O (n³), hoàn toàn đánh bại mục đích của bài tập này. Tuy nhiên, chúng tôi có thể bỏ qua tất cả điều này và nhận được O (1) bằng cách sử dụng unsafeCoerce:

revAppend :: Rev acc xs :~: Reverse' xs ++ acc 
revAppend = unsafeCoerce Refl 

Điều này có an toàn không? Điều gì về trường hợp chung? Ví dụ: nếu tôi có hai loại gia đình F :: k -> * và G :: k -> * và tôi biết rằng chúng tương đương nhau, có an toàn để xác định những điều sau không?

equal :: F a :~: G a 
equal = unsafeCoerce Refl 

Answer 1

Nó sẽ là rất tốt đẹp nếu GHC sử dụng một trình kiểm tra kết thúc vào biểu e::T nơi T chỉ có một constructor không có đối số K (ví dụ :~:, ()). Khi kiểm tra thành công, GHC có thể viết lại e như K bỏ qua tính toán hoàn toàn. Bạn sẽ phải loại trừ FFI, unsafePerformIO, trace, ... nhưng có vẻ như khả thi. Nếu điều này được thực hiện, nó sẽ giải quyết câu hỏi được đăng rất độc đáo, cho phép người ta thực sự viết các bằng chứng có chi phí thời gian chạy bằng không.

Nếu không, bạn có thể sử dụng unsafeCoerce trong khi chờ đợi, như bạn đề xuất. Nếu bạn thực sự, thực sự chắc chắn rằng hai loại là giống nhau, bạn có thể sử dụng nó một cách an toàn. Ví dụ điển hình là triển khai Data.Typeable. Tất nhiên, việc sử dụng sai mục đích unsafeCoerce trên các loại khác nhau sẽ dẫn đến các hiệu ứng không thể dự đoán được, hy vọng một sự cố.

Bạn thậm chí có thể viết riêng của bạn "an toàn" biến thể của unsafeCoerce:

unsafeButNotSoMuchCoerce :: (a :~: b) -> a -> b 
#ifdef CHECK_TYPEEQ 
unsafeButNotSoMuchCoerce Refl = id 
#else 
unsafeButNotSoMuchCoerce _ = unsafeCoerce 
#endif 

Nếu CHECK_TYPEEQ được định nghĩa nó dẫn đến mã chậm hơn. Nếu không xác định, nó bỏ qua nó và coerces với chi phí bằng không. Trong trường hợp thứ hai, nó vẫn không an toàn vì bạn có thể vượt qua dưới dạng arg đầu tiên và chương trình sẽ không lặp nhưng thay vào đó sẽ thực hiện cưỡng chế sai. Bằng cách này, bạn có thể kiểm tra chương trình của mình bằng chế độ an toàn nhưng chậm, sau đó chuyển sang chế độ không an toàn và cầu nguyện "chứng minh" của bạn luôn chấm dứt.