haskell - normalizacion - ¿Puedo hacer magia para arriba la igualdad de tipos de una dependencia funcional?

normalizacion de base de datos ejemplos

Question

Estoy tratando de tener una idea de MultiParamTypeClasses y FunctionalDependencies , y lo siguiente me pareció algo obvio:

{-# LANGUAGE MultiParamTypeClasses
, FunctionalDependencies
, TypeOperators #-}
import Data.Type.Equality
class C a b | a -> b
fob :: (C a b, C a b'') => proxy a -> b :~: b''
fob _ = Refl

Desafortunadamente, esto no funciona; GHC no concluye b ~ b'' de ese contexto. ¿Hay alguna forma de hacer que esto funcione, o la dependencia funcional no está "internamente" disponible?

Answer 1

No creo que este hecho (como lo indica el tipo de fob ) sea realmente cierto. Debido a la propiedad de mundo abierto de las clases de tipo, puede violar el fundep con los límites de los módulos.

Esto se muestra en el siguiente ejemplo. Este código solo se ha probado con GHC 7.10.3 (los fundeps se rompieron de forma masiva en versiones anteriores; no sé qué sucede entonces). Supongamos que puede implementar lo siguiente:

module A
(module A
,module Data.Type.Equality
,module Data.Proxy
)where
import Data.Type.Equality
import Data.Proxy
class C a b | a -> b
inj_C :: (C a b, C a b'') => Proxy a -> b :~: b''
inj_C = error "oops"

A continuación, algunos módulos más:

module C where
import A
instance C () Int
testC :: C () b => Int :~: b
testC = inj_C (Proxy :: Proxy ()) 

y

module B where
import A
instance C () Bool
testB :: C () b => b :~: Bool
testB = inj_C (Proxy :: Proxy ()) 

y

module D where
import A
import B
import C
oops :: Int :~: Bool
oops = testB
oops_again :: Int :~: Bool
oops_again = testC 

Int :~: Bool claramente no es cierto, por lo que, por contradicción, inj_C no puede existir.

Creo que aún puede escribir de forma segura inj_C con unsafeCoerce si no exporta la clase C del módulo en el que está definido. He usado esta técnica, y he probado ampliamente, y no he podido escribir una contradicción. No quiere decir que sea imposible, pero al menos muy difícil y un caso de borde raro.

Answer 2

No es necesario recurrir a varios módulos para engañar al verificador de dependencia funcional. Aquí hay dos ejemplos de fundeps incorrectos que aún se construyen con HEAD. Están adaptados de la suite de pruebas de GHC.

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
FlexibleInstances, FlexibleContexts,
UndecidableInstances, DataKinds, PolyKinds,
GADTs #-}
module M where
data K x a = K x
class Het a b | a -> b where
het :: m (f c) -> a -> m b
instance Het t t where het = undefined
class GHet (a :: * -> *) (b :: * -> *) | a -> b
instance GHet (K a) (K [a])
instance Het a b => GHet (K a) (K b)
data HBool = HFalse | HTrue
class TypeEq x y b | x y -> b
instance {-# OVERLAPS #-} (HTrue ~ b) => TypeEq x x b
instance {-# OVERLAPS #-} (HFalse ~ b) => TypeEq x y b

¡El corrector fundep sigue siendo mucho mejor de lo que solía ser!