使用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)

不幸的是,revAppendO(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定义了它会导致代码变慢.如果未定义,它会跳过它并以零成本强制执行.在后一种情况下,它仍然是不安全的,因为你可以将底部作为第一个arg传递,程序将不会循环,而是执行错误的强制.通过这种方式,您可以使用安全但缓慢的模式测试程序,然后转到不安全模式并祈祷您的"校样"始终终止.