使用unsafeCoerce進行有效平等總是安全的嗎？

Question

我有型層級清單證人類型，

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

以及以下實用程序。現在

-- 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 

，我有一個類型級反轉函數的兩個不同但等價的定義，

-- 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] 

首先是更有效的，但第二個是更容易證明東西到編譯器時使用，所以有一個等價的證明是很好的。爲了做到這一點，我需要Rev acc xs :~: Reverse' xs ++ acc的證明。這是我想出了：

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) 

不幸的是，revAppend是O（N 3），這完全違背了這項工作的目的。但是，我們可以繞過這一切，通過使用unsafeCoerce得到O（1）：

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

這安全嗎？一般情況如何？例如，如果我有兩個類型系列F :: k -> *和G :: k -> *，並且我知道它們是等價的，那麼定義以下內容是否安全？

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

Answer 1

如果GHC使用上表達e::T終止檢查，其中T只有一個不帶參數的構造函數K（例如:~:，()）這將是非常好的。當檢查成功時，GHC可以重寫e爲K完全跳過計算。你將不得不排除FFI，unsafePerformIO，trace，...但它似乎是可行的。如果這樣做，它會很好地解決發佈的問題，從而允許人們實際編寫運行時成本爲零的證明。

如果不符合要求，您可以按照您的建議使用unsafeCoerce。如果你確實確信兩種類型是相同的，你可以安全地使用它。典型的例子是實施Data.Typeable。當然，在不同類型上使用unsafeCoerce會導致不可預知的影響，希望能夠發生崩潰。

你甚至可以寫出unsafeCoerce自己的「安全」的變種：

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

如果CHECK_TYPEEQ定義它會導致慢的代碼。如果未定義，則跳過它並以零成本強制執行。在後一種情況下，它仍然是不安全的，因爲您可以將第一個參數傳遞給底部，程序不會循環，而是執行錯誤的強制。通過這種方式，您可以使用安全但緩慢的模式測試您的程序，然後轉向不安全模式，並祈禱您的「證明」始終終止。