这是对 unsafeCoerce 的安全使用吗？答案

【问题标题】：Is this a safe use of unsafeCoerce?这是对 unsafeCoerce 的安全使用吗？
【发布时间】：2012-12-28 15:23:14
【问题描述】：

我目前有一种情况，我正在使用极其可怕的功能 unsafeCoerce。幸运的是，这不是什么重要的事情，但我想知道这是否是对这个函数的安全使用，或者是否有其他方法可以解决其他人知道的这个特定问题。

我的代码如下：

data Token b = Token !Integer

identical :: Token a -> Token b -> Bool
identical (Token a) (Token b) = a == b

data F a = forall b. F (Token b) (a -> b)

retrieve :: Token b -> F a -> Maybe (a -> b)
retrieve t (F t' f) = if identical t t' then Just (unsafeCoerce f) else Nothing

另外需要注意的两件事是，这些标记是在一个 monad 中使用的，我用它来确保为它们提供的整数是唯一的（即，我不会两次制作相同的标记）。我还使用了一个 forall 量化的影子类型变量，与 ST monad 一样，以确保（假设仅使用我在模块中公开的方法）没有办法返回令牌（或者实际上什至是F) 来自 monad，而不是类型错误。我也不公开令牌构造函数。

我认为，据我所知，这应该是 unsafeCoerce 的安全用法，正如我可以说（我希望）非常自信地说，我强制的值实际上正是我的类型强迫它，但我可能是错的。我也尝试过使用 Data.Typeable，它工作得很好，但目前我正在尝试这样做以避免 Typeable 约束，特别是因为 gcast 似乎在许多方面做了类似的事情，而且我仍然需要令牌来区分同类型的不同F。

非常感谢任何帮助/建议。

【问题讨论】：

这看起来很像Data.Typeable，它在后台使用unsafeCoerce 来实现cast。
很像 - 事实上，iirc 我在问题的最后一段的后半部分已经说了很多。还是谢谢。
如果您有效地复制了cast，那么使用unsafeCoerce 是安全的，但您确实会丢失编译器生成的typeOf/TypeRep。您可以考虑在令牌中使用TypeRep 而不是Integer。
嗯，原来的原因是我还需要区分两个相同类型的不同值，但是可能还需要使用Typeable/TypeRep。

标签： haskell types dynamic-typing

【解决方案1】：

您已经实现了一种受限形式的动态类型，大致遵循Data.Dynamic 的风格——即将（不透明）值与其类型的证据相匹配。在运行时，您可以根据随数据提供的证据进行不安全的强制。

fromDyn (Dynamic t v) def
  | typeOf def == t = unsafeCoerce v
  | otherwise       = def

这是具有悠久历史的规范方法，可以追溯到：

Mart´ın Abadi、Luca Cardelli、Benjamin Pierce 和 Gordon Plotkin。静态类型语言中的动态类型。 ACM 编程语言和系统交易， 13(2):237–268，1991 年 4 月。

该方法的安全性依赖于运行时类型令牌的不可伪造性。在您的情况下，任何人都可以构建等同于两种类型的令牌 - 您需要保证从类型到令牌的 1-1 映射，并确保恶意用户无法构建不正确的令牌。在 GHC 案例中，我们信任 Typeable 实例（和模块抽象）。

【讨论】：

【解决方案2】：

这本身并不安全：

oops :: F Bool
oops = F (Token 12) not

bad :: Token Int
bad = Token 12

*Token> maybe 3 ($ True) $ retrieve bad oops
1077477808

F a 是一种存在量化类型，你不知道b 属于哪个类型。由于identical 不关心Token 的类型参数，它无法检查retrieve 的第一个参数提供的b 是否与F a 中的内容有关。

是否保护你

另外需要注意的两件事是，这些标记是在一个 monad 中使用的，我用它来确保为它们提供的整数是唯一的（即，我不会两次制作相同的标记）。我还使用了一个 forall 量化的影子类型变量，与 ST monad 一样，以确保（假设仅使用我在模块中公开的方法）没有办法返回令牌（或者实际上什至是F) 来自 monad，而不是类型错误。我也没有公开令牌构造函数。

足够强大以使其在实践中安全，我不看就无法判断。如果确实不能在计算之外创建Tokens，并且Token的Integer值唯一地表征了类型参数，那将是安全的。

【讨论】：