为什么没有被广义化的类型赋予一个安全的Haskell？

问题描述

从GHC的手册中，：

如何使用 a>

From GHC's manual, Section Safe Language:

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？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！