¿Por qué no es GeneralizedNewtypeDeriving un Safe Haskell?

ghc language-extension

Question

Del manual de GHC, Sección Safe Language :

Control de límites de módulo : se garantiza que el código Haskell compilado usando un lenguaje seguro solo tendrá acceso a los símbolos que están disponibles públicamente a través de otras listas de exportación de módulos. Una parte importante de esto es que el código compilado seguro no puede examinar o crear valores de datos utilizando constructores de datos que no puede importar. Si un módulo M establece algunos invariantes mediante el uso cuidadoso de su lista de exportación, el código compilado utilizando el lenguaje seguro que importa M está garantizado para respetar esos invariantes. Debido a esto, Template Haskell y GeneralizedNewtypeDeriving están deshabilitados en el lenguaje seguro ya que pueden utilizarse para violar esta propiedad.

¿Cómo se puede romper las invariantes de un módulo utilizando GeneralizedNewtypeDeriving ?

Answer 1

Luqui vinculado a mi blog sobre el tema. Básicamente, el uso GeneralizedNewtypeDeriving de newtype implementado en GHC supone que cierto tipo de isomorfismo (es decir, el isomorfismo operacionalmente irrelevante que implica newtype ) implica la igualdad de leibniz. Esto fue cierto en Haskell 98, pero no lo es en absoluto en las extensiones Haskell plus.

Es decir, un newtype proporciona un par de funciones.

a -> b
b -> a

Eso no hace nada en el núcleo, pero no está bien concluir.

forall f. f a -> f b

porque f podría ser una función de tipo o una GADT. Esta es la forma de igualdad necesaria para GeneralizedNewtypeDeriving

Incluso en Haskell 98 rompe los límites del módulo. Puedes tener cosas como

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

que hará cosas malas ...

La publicación de mi blog muestra cómo implementar unsafeCoerce varias maneras utilizando otras extensiones (todas seguras) y GeneralizedNewtypeDeriving. Ahora comprendo mejor por qué esto es así y confío mucho más en que GeneralizedNewtypeDeriving no puede producir unsafeCoerce sin las extensiones de estilo "System FC" (familias de tipo, GADT). Sin embargo, es inseguro y debe usarse con cuidado, si es que lo hace. Mi entendimiento es que Lennart Augustsson (usuario augustos) lo implementó de manera muy diferente en hbc, y esta implementación fue segura. Una implementación segura sería más limitada y más complicada.

ACTUALIZACIÓN: Con nuevas versiones suficientes de GHC (todos los problemas deberían haberse solucionado a partir de 7.8.1) GeneralizedNewtypeDeriving es seguro debido al nuevo sistema de roles