Kann ich die Gleichheit aus einer funktionalen Abhängigkeit herauszaubern?

Question

Ich versuche, ein Gefühl von MultiParamTypeClasses und FunctionalDependencies, und die folgende fiel mir als eine offensichtliche Sache zu bekommen, um zu versuchen:

{-# 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 

Leider ist dies nicht funktioniert; GHC schließt b ~ b' aus diesem Kontext nicht ab. Gibt es eine Möglichkeit, dies zum Funktionieren zu bringen, oder ist die funktionale Abhängigkeit nicht "intern" verfügbar?

Answer 1

Ich glaube nicht, dass diese Tatsache (wie von der Art der fob angegeben) tatsächlich wahr ist. Aufgrund der Open-World-Eigenschaft von Typklassen können Sie die Fundecke mit Modulgrenzen verletzen.

Dies wird durch das folgende Beispiel gezeigt. Dieser Code wurde nur mit GHC 7.10.3 getestet (fundeps waren in älteren Versionen massiv kaputt - weiß nicht, was dann passiert). Angenommen, Sie in der Tat die folgende implementieren können:

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" 

dann noch ein paar Module:

module C where 
import A 

instance C() Int 

testC :: C() b => Int :~: b 
testC = inj_C (Proxy :: Proxy()) 

und

module B where 
import A 

instance C() Bool 

testB :: C() b => b :~: Bool 
testB = inj_C (Proxy :: Proxy()) 

und

module D where 

import A 
import B 
import C 

oops :: Int :~: Bool 
oops = testB 

oops_again :: Int :~: Bool 
oops_again = testC 

Int :~: Bool ist eindeutig nicht wahr , so vorbei Widerspruch, inj_C kann nicht existieren.

Ich glaube, Sie können inj_C mit unsafeCoerce immer noch sicher schreiben, wenn Sie nicht die Klasse C aus dem Modul exportieren, wo es definiert ist. Ich habe diese Technik benutzt, habe es ausgiebig versucht und konnte keinen Widerspruch schreiben. Nicht zu sagen, es ist unmöglich, aber zumindest sehr schwierig und ein seltener Randfall.

Answer 2

Sie müssen nicht auf mehrere Module zurückgreifen, um den funktionalen Abhängigkeitsüberprüfer zu täuschen. Hier sind zwei Beispiele für falsche Funde, die immer noch mit HEAD erstellt werden. Sie sind von der GHC-Testsuite angepasst.

{-# 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 

Der fundep checker ist immer noch viel besser als früher!