Funktionsweise von Typinferenz bei funktionalen Abhängigkeiten
Betrachten Sie den folgenden Code:
{-# LANGUAGE MultiParamTypeClasses,FlexibleInstances,FunctionalDependencies,UndecidableInstances,FlexibleContexts #-}
class Foo a c | a -> c
instance Foo Int Float
f :: (Foo Int a) => Int -> a
f = undefined
Jetzt, wenn ich den abgeleiteten Typ von f in ghci sehe
> :t f
> f :: Int -> Float
Jetzt wenn ich den folgenden Code hinzufüge
g :: Int -> Float
g = undefined
h :: (Foo Int a) => Int -> a
h = g
Ich bekomme den Fehler
Could not deduce (a ~ Float)
Ich kann nicht verstehen, was hier passiert ist? Die BeschränkungFoo Int a
sollte die Art von beschränkt habenh
zuInt -> Float
wie in der abgeleiteten Art von gezeigtf
.
Liegt es daran, dass eine Typvereinigung stattfindet, bevor die Instanzen aufgelöst werden?
[Aktualisieren]
Eine Erklärung von Dan Doel auf der Mailingliste des Cafés
Die Antwort, glaube ich, ist, dass der Unterschied zwischen der Fundep-Implementierung und den Typfamilien lokale Randbedingungen sind. Fundeps machen keine lokale Verbreitung.
Also haben Sie in Ihrer ersten Definition vor Ort angegeben 'Int -> a
', was für GHC akzeptabel ist. Dann stellt es extern zu der Funktion heraus, die '(Foo Int a) => Int -> a
ist eigentlichInt -> Float
.
In der zweiten Definition versuchen Sie zu geben 'Int -> Float
', aber GHC weiß nur lokal, was Sie bereitstellen müssen'Int -> a
'mit einer Einschränkung'Foo Int a
'was esGewohnheit Verwenden Sie, um das zu bestimmena ~ Float
.
Dies ist Fundeps nicht inhärent. Man könnte eine Version von Fundeps erstellen, die die lokalen Einschränkungsregeln enthält (einfach durch Übersetzen in das neue Material für Typfamilien). Der Unterschied ist jedoch auch der Grund dafür, dass überlappende Instanzen für Fundeps und nicht für Typfamilien unterstützt werden. Aber ich werde jetzt nicht darauf eingehen.
Ich verstehe immer noch nicht, was das bedeutet. Also noch auf der Suche nach besser verständlicher Antwort.