为什么GeneralizedNewtypeDeriving不是安全的Haskell?

20
从 GHC 的手册中,第 Safe Language 章节得知:

模块边界控制 —— 使用 safe 语言编译的 Haskell 代码仅能访问通过其他模块的导出列表公开的符号。其中一个重要部分是 safe 编译后的代码不能使用它无法导入的数据构造函数来检查或创建数据值。如果某个模块 M 通过谨慎使用其导出列表建立了一些不变量,则使用导入 M 的 safe 语言编译的代码将保证尊重这些不变量。因此,在 safe 语言中禁用 Template Haskell 和 GeneralizedNewtypeDeriving,因为它们可以用来违反该属性。

问:如何使用 GeneralizedNewtypeDeriving 来破坏模块的不变量?
答:未提及。

2
请查看此工单,其中链接了详细说明。 - Daniel Fischer
3
因为它可以用来编写unsafeCoerce(http://joyoftypes.blogspot.com/2012/08/generalizednewtypederiving-is.html)。 - luqui
3
有一个安全的版本,但比 GHC 拥有的版本要不强大得多。 - augustss
或者是关于“安全 Haskell”的论文,它在第二和第三页上。http://research.microsoft.com/en-us/um/people/simonpj/papers/safe-haskell/safe-haskell.pdf - tomferon
4
较低版本的限制是什么? - Gabriella Gonzalez
2
较弱的版本只是构建实例。当类型变量以非平凡的方式使用时,您可以想象这如何崩溃。具有“Functor”实例的容器可以工作,但没有更多了。尽管如此,这已足以推导出所有常规类型类,例如“Eq”,“Ord”,“Num”等。 - augustss
1个回答

29
Luqui在我的博客文章中分享了关于此主题的内容。基本上,GHC实现的GeneralizedNewtypeDeriving假定某种类型同构(即newtype所暗示的操作上不相关的同构)意味着Leibniz等式。这在Haskell 98中有些正确,但在加入扩展的Haskell中完全不正确
换句话说,一个newtype提供了一对函数。
a -> b
b -> a

有些东西在核心中不起作用,但得出结论是不可以的。

forall f. f a -> f b

因为 f 可能是类型函数或者 GADT。这种等式形式适用于 GeneralizedNewtypeDeriving
即使在 Haskell 98 中,它也会打破模块边界。你可以有像这样的东西。
class FromIntMap a where
  fromIntMap :: Map Int b -> Map a b

instance FromIntMap Int where
  fromIntMap = id

newtype WrapInt = WrapInt Int deriving FromIntMap

instance Ord WrapInt where
  WrapInt a <= WrapInt b = b <= a

这篇博客介绍了如何使用其他扩展(全部安全)和GeneralizedNewtypeDeriving实现unsafeCoerce的几种方法。现在我更好地理解了为什么会这样,并且更加自信,认为GeneralizedNewtypeDeriving不能在没有“System FC”风格的扩展(类型族、GADTs)的情况下产生unsafeCoerce。但是,它仍然是不安全的,如果必须使用,应该小心使用。据我了解,Lennart Augustsson(用户augustss)在hbc中实现了完全不同的方法,这个实现是安全的。安全实现将更加有限制,也更加复杂。

更新:使用新版本的GHC(7.8.1及以上版本应该已经解决了所有问题),由于新的roles systemGeneralizedNewtypeDeriving是安全的。


5
在 GHC 7.8 或 7.10 中仍不安全:https://mail.haskell.org/pipermail/haskell-cafe/2015-April/118970.html - massysett

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接