gpt4 book ai didi

haskell - 为什么 GeneralizedNewtype 不派生一个安全的 Haskell?

转载 作者:行者123 更新时间:2023-12-04 20:50:33 26 4
gpt4 key购买 nike

来自 GHC 的手册,第 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.



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

最佳答案

Luqui 链接到 my blog post就此主题而言。基本上,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.我对现在的原因有了更好的理解,并且对 GeneralizedNewtypeDeriving 更有信心。无法生产 unsafeCoerce没有“System FC”样式扩展(类型家族,GADT)。 Sill,它是不安全的,如果有的话,应该小心使用。我的理解是 Lennart Augustsson(用户 augustss)在 hbc 中实现它的方式非常不同,而且这种实现是安全的。一个安全的实现会更受限制,也更复杂。

更新:使用足够新的 GHC 版本(从 7.8.1 开始,所有问题都应该消失) GeneralizedNewtypeDeriving是安全的,因为新的 roles system

关于haskell - 为什么 GeneralizedNewtype 不派生一个安全的 Haskell?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/17137111/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com