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 -> aist 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.

Antworten auf die Frage(1)

Ihre Antwort auf die Frage