这是不安全的Coerce的安全使用吗？

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

还有两点需要注意的是,这些令牌是在monad中使用的,我用它来确保为它们提供整数是唯一的(即我不会两次使用相同的令牌).我也使用forall量化的阴影类型变量,与ST monad一样,以确保(假设只使用我在模块中公开的方法)没有办法返回令牌(或者实际上甚至是F)来自monad而不是类型错误.我也没有公开令牌构造函数.

我认为,据我所知,这应该是对safeafeCoerce的安全使用,正如我可以说的那样(我希望)相当高的信心,我所强迫的价值实际上是我强迫它的类型,但我可能错了.我也尝试过使用Data.Typeable,它工作得很好,但目前我正在尝试避免使用Typeable约束,特别是因为gcast似乎在很多方面做了类似的事情,我仍然需要令牌才能区分不同类型的Fs.

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

Answer 1

您已经实现了一种受限形式的动态类型,大致遵循Data.Dynamic的风格- 即将(不透明)值与其类型的证据相匹配.在运行时,您可以根据数据随附的证据进行不安全的强制操作.

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

这是历史悠久的标准方法,可以追溯到:

Mart'ınAbadi,Luca Cardelli,Benjamin Pierce和Gordon Plotkin.动态键入静态类型语言.ACM Transactions for Programming Languages and Systems,13(2):237 - 268,1991年4月.

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

Answer 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,它无法检查b从retrieve第一个参数提供的内容是否与进入的内容有关F a.

是否保护

还有两点需要注意的是,这些令牌是在monad中使用的,我用它来确保为它们提供整数是唯一的(即我不会两次使用相同的令牌).我也使用forall量化的阴影类型变量,与ST monad一样,以确保(假设只使用我在模块中公开的方法)没有办法返回令牌(或者实际上甚至是F)来自monad而不是类型错误.我也没有公开令牌构造函数.

强大到足以让它在实践中安全,我看不清楚.如果确实Token在计算之外不能创建s,并且唯一的Integer值表示Token类型参数,那么它将是安全的.