haskell - 这是 unsafeCoerce 的安全使用吗？

Question

我现在正在使用极其可怕的函数 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

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

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

非常感谢您的帮助/建议。

Answer 1

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

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

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

Mart´ın Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. Dynamic typing in a statically typed language. ACM Transactions on Programming Languages and Systems, 13(2):237–268, April 1991.

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