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!