为什么没有被广义化的类型赋予一个安全的Haskell？ [英] Why isn't GeneralizedNewtypeDeriving a Safe Haskell?

问题描述

从GHC的手册中，安全语言：

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

如何使用 GeneralizedNewtypeDeriving ？

解决方案

Luqui与我的博客文章。基本上，在GHC中实现的 GeneralizedNewtypeDeriving 假定某种同构（即 newtype 隐含的操作上无关的同构）意味着莱布尼茨的平等。这在Haskell 98中是正确的 - 但在Haskell plus扩展中完全不是。

也就是说，一个新类型提供了一对函数

  a - > b 
 b  - > a 
  

在核心中没有做任何事情，但是不能总结

  forall f。 f a  - > fb 
  

因为 f 可能是一个类型函数或GADT。这是 GeneralizedNewtypeDeriving

所需的平等形式。即使在Haskell 98中，它也会打破模块边界。你可以拥有像

  class FromIntMap a where 
 fromIntMap :: Map Int b  - >映射ab 
 
实例FromIntMap Int其中
 fromIntMap = id 
 
 newtype WrapInt = WrapInt Int派生FromIntMap 
 
实例Ord WrapInt其中
 WrapInt a< = WrapInt b = b< = a 
  

这会做坏事。 ..

我的博客文章展示了如何使用其他扩展（全部安全）和<$实现 unsafeCoerce c $ c> GeneralizedNewtypeDeriving。我更好地理解了现在的原因，并且更加确信 GeneralizedNewtypeDeriving 无法产生 unsafeCoerce 没有System FC风格扩展（类型familes，GADT）。槛，这是不安全的，应该小心使用，如果有的话。我的理解是，Lennart Augustsson（用户八月）在hbc中实现它的方式非常不同，并且此实现是安全的。一个安全的实现将更加有限，并且更复杂。

更新：新版本的GHC（所有问题应该从7.8.1开始） GeneralizedNewtypeDeriving 是安全的，因为新的角色系统 a>

From GHC's manual, Section Safe Language:

Module boundary control — Haskell code compiled using the safe language is guaranteed to only access symbols that are publicly available to it through other modules export lists. An important part of this is that safe compiled code is not able to examine or create data values using data constructors that it cannot import. If a module M establishes some invariants through careful use of its export list then code compiled using the safe language that imports M is guaranteed to respect those invariants. Because of this, Template Haskell and GeneralizedNewtypeDeriving are disabled in the safe language as they can be used to violate this property.

How can one break a module's invariants using GeneralizedNewtypeDeriving?

解决方案

Luqui linked to my blog post on the subject. Basically, GeneralizedNewtypeDeriving as implemented in GHC assumes that a certain kind of isomorphism (namely the operationally irrelevant isomorphism implied by newtype) implies leibniz equality. This was true in Haskell 98 sort of--but is not at all true in Haskell plus extensions.

That is, a newtype provides a pair of functions

a -> b
b -> a

that don't do anything in the core, but it is not okay to conclude

forall f. f a -> f b

because f might be a type function or a GADT. This is the form of equality needed for GeneralizedNewtypeDeriving

Even in Haskell 98 it breaks module boundries. You can have things like

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

which will do bad things...

My blog post shows how to implement unsafeCoerce several ways using other extensions (all safe) and GeneralizedNewtypeDeriving. I have a better understanding of why this is now, and am much more confident that GeneralizedNewtypeDeriving is unable to produce unsafeCoerce without the "System FC" style extensions (type familes, GADTs). Sill, it is unsafe, and should be used with care if at all. My understanding is that Lennart Augustsson (user augustss) implemented it very differently in hbc, and this implementation was safe. A safe implementation would be more limited, and more complicated.

UPDATE: With new enough versions of GHC (all problems should be gone as of 7.8.1) GeneralizedNewtypeDeriving is safe because of the new roles system

这篇关于为什么没有被广义化的类型赋予一个安全的Haskell？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！