13

我有一种情况，我目前正在使用极其可怕的功能 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。

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

4

2 回答 2

14

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

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

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

Mart´ın Abadi、Luca Cardelli、Benjamin Pierce 和 Gordon Plotkin。静态类型语言中的动态类型。ACM Transactions on Programming Languages and Systems，13(2):237–268，1991 年 4 月。

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

于 2013-01-14T16:46:01.480 回答
9

它本身并不安全：

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，它无法检查提供b的 fromretrieve的第一个参数是否与F a.

无论您的保护

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

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

于 2013-01-14T16:44:42.257 回答