这是安全使用不安全的Coerce吗？ [英] Is this a safe use of unsafeCoerce?

问题描述

我现在有一种情况，就是使用非常可怕的函数unsafeCoerce。幸运的是，这并不是什么重要的事情，但我想知道这是否是这个函数的安全使用，或者是否有另一种方法来解决其他人知道的这个特定问题。

我的代码如下所示：

 数据令牌b =令牌！整数
 
相同::令牌a  - >令牌b  - > Bool 
相同（令牌a）（令牌b）= a == b 
 
数据F a = forall b。 F（令牌b）（a  - > b）
 
检索::令牌b  - > F a  - >可能（a  - > b）
检索t（F t'f）=如果相同t t'则Just（unsafeCoerce f）else Nothing 
  

另外需要注意的是，这些令牌用在monad中，我使用它来确保为它们提供的整数是唯一的（即，我不使相同的令牌两次）。我也使用一个全量化的阴影类型变量，就像ST monad一样，确保（假设只有我在模块中公开的方法被使用），没有办法返回一个标记（或者实际上甚至是F）从monad没有它是一个类型错误。我也不公开这个令牌构造函数。

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

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

解决方案

你已经实现了一种动态类型的限制形式，广泛地遵循 Data.Dynamic - 即将一个（不透明）值与其类型的证据配对。
在运行时，您可以根据数据附带的证据进行不安全的强制。

  fromDyn（动态电视）def 
 | typeOf def == t = unsafeCoerce v 
 |否则= def 
  

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

ACM编程语言和系统事务
13（2）：237-268，1991年4月。

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

I have a situation where I am at the moment using the extremely scary function unsafeCoerce. It's not for anything important fortunately, but I was wondering whether this seems to be a safe usage of this function, or whether there would be another way to solve this particular problem that other people know of.

The code I have is something like the following:

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

Two additional things to note, are that these tokens are used within a monad which I use to ensure that the supply of integers for them is unique (i.e. I don't make the same token twice). I also use a forall quantified shadow type variable, in the same way as the ST monad, to make sure that (assuming only the methods I expose in the module are used) there is no way to return a token (or in fact even an F) from the monad without it being a type error. I also don't expose the token constructor.

I think, as far as I can see, this should be a safe usage of unsafeCoerce, as I can say with (I hope) pretty high confidence that the value I am coercing is in fact of exactly the type that I am coercing it to, but I may be wrong. I have also tried using Data.Typeable, which works nicely, but at the moment I am trying this to avoid the Typeable constraint, especially as gcast seems to do something in many ways similar, and I would still need the tokens anyway to distinguish between different Fs of the same type.

Thanks very much for any help/advice.

解决方案

You have implemented a restricted form of dynamic typing, broadly following the style of Data.Dynamic -- namely, paring an (opaque) value with evidence of its type. At runtime you can do an unsafe coercion, based on the evidence you shipped with the data.

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

This is the canoncial approach, with a long history, going back to:

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.

The safety of the approach relies on the unforgeability of runtime type tokens. In your case, anyone can build a token that equates two types -- you would need to guarantee a 1-1 mapping from types to tokens, and ensure that a malicious user can't construct incorrect tokens. In the GHC case, we trust the Typeable instances (and module abstraction).

这篇关于这是安全使用不安全的Coerce吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！