haskell - 将 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³)，这完全违背了本练习的目的。但是，我们可以绕过所有这些并使用 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定义它会导致代码变慢。如果未定义，它会跳过它并以零成本强制执行。在后一种情况下，它仍然是不安全的，因为您可以将底部作为第一个参数传递，并且程序不会循环，而是会执行错误的强制转换。通过这种方式，您可以使用安全但缓慢的模式测试您的程序，然后转到不安全模式并祈祷您的“证明”总是终止。