haskell - `coerce` 的所有类型检查都可以安全地替换为 `unsafeCoerce` 吗？

Question

我相信以下内容与 Set.mapMonotonic coerce 一样安全.即可能发生的最坏情况是我将打破 Set不变量 a或 b有不同的Ord实例:

coerceSet :: Coercible a b=> Set.Set a -> Set.Set b
coerceSet = unsafeCoerce

那是对的吗？

编辑 : Set 的相关功能问题: https://github.com/haskell/containers/issues/308

Answer 1

这应该是安全的。

有效的 coerce @a @b始终可以替换为有效的 unsafeCoerce @a @b .为什么？因为，在核心级别，它们是相同的函数，coerce (它只返回其输入，如 id )。问题是 coerce以证明被强制的两件事具有相同表示的证据作为论据。正常coerce ，这个证明是一个实际的证明，但是带有 unsafeCoerce ，这个证明只是一个表示“相信我”的象征。这个证明作为类型参数传递，因此，通过类型删除，对程序的行为没有影响。因此unsafeCoerce和 coerce只要两者都可能，就等价。

现在，Set 的故事还没有结束。 , 因为 coerce不适用于 Set .为什么？让我们看看它的定义。

data Set a = Bin !Size !a !(Set a) !(Set a) | Tip

从这个定义中，我们看到 a不会出现在任何类型等式等内部。这意味着我们在 Set 处具有表示等式的一致性: 如果 a ~#R b (如果 a 与 b 具有相同的表示 - ~#R 未装箱 Coercible )，则 Set a ~#R Set b .所以，根据 Set 的定义一个人， coerce应该在 Set 上工作，因此您的 unsafeCoerce应该是安全的。 containers库必须使用特定的

type role Set nominal

为了向世人隐瞒这个事实，人为地禁用了 coerce .你永远不能禁用 unsafeCoerce ，但是，重申， unsafeCoerce (在这种情况下)是安全的。

(请注意 unsafeCoerce 和 coerce 具有相同的类型!请参阅@dfeuer 的答案，了解“过度热心”类型推断会使所有内容变形的情况示例。)