为什么不是GeneralizedNewtypeDeriving一个安全的Haskell？

Question

从GHC的手册,安全语言部分:

模块边界控制 - 使用安全语言编译的Haskell代码保证只能访问通过其他模块导出列表公开可用的符号.其中一个重要的部分是安全编译的代码无法使用无法导入的数据构造函数来检查或创建数据值.如果模块M通过仔细使用其导出列表建立了一些不变量,则使用导入M的安全语言编译的代码保证遵守这些不变量.因此,模板Haskell GeneralizedNewtypeDeriving以安全语言禁用,因为它们可用于违反此属性.

如何使用GeneralizedNewtypeDeriving？打破模块的不变量？

Answer 1

Luqui链接到我关于这个主题的博客文章.基本上,GeneralizedNewtypeDeriving正如在GHC中实现的那样,假设某种同构(即隐含的操作上无关的同构newtype)意味着莱布尼茨平等.这在Haskell 98中是正确的 - 但在Haskell plus扩展中却完全没有.

也就是说,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

这会做坏事......

我的博客文章展示unsafeCoerce了如何使用其他扩展(所有安全)实现多种方式,并且GeneralizedNewtypeDeriving. 我对现在的原因有了更好的理解,并且更加自信,如果没有"System FC"样式扩展,GeneralizedNewtypeDeriving就无法生成unsafeCoerce(类型为familes, GADTs).Sill,它是不安全的,如果有的话应该小心使用.我的理解是Lennart Augustsson(用户augustss)在hbc中实现它的方式非常不同,这种实现是安全的.安全的实施将更加有限,而且更加复杂.

更新:由于GeneralizedNewtypeDeriving新的角色系统,GHC的新版本(所有问题应该从7.8.1起消失)是安全的