Gegebene Typdefinitionen:
%Vor%... und diese Typklasse:
%Vor%... diese (im Sinne eines minimalen Beispiels höchst konstruierte) Funktionsdefinitionen typecheck:
%Vor%Wenn wir jedoch eine Typfamilie anstelle einer Klasse mit einer funktionalen Abhängigkeit verwenden:
%Vor%... dann können die entsprechenden Funktionsdefinitionen nicht ticken:
%Vor%%Vor%
Ich habe Abschnitt 5.2 von OutsideIn ( X) Papier , das berührbare und unantastbare Typvariablen beschreibt, und ich Art verstehe, was hier vor sich geht. Wenn ich ein zusätzliches Argument zu f hinzufüge, das die Auswahl von f außerhalb der inneren forall verschiebt, dann prüft das Programm typeChecks:
Was mich jedoch gerade in diesem speziellen Beispiel so verwirrt hat, ist, warum die funktionale Abhängigkeit ein unterschiedliches Verhalten hat. Ich habe gehört, dass die Leute zu verschiedenen Zeiten behaupten, dass funktionale Abhängigkeiten wie diese einer Typfamilie plus einer Gleichheit gleichwertig sind, aber dies zeigt, dass das nicht stimmt.
Welche Informationen liefert die funktionale Abhängigkeit in diesem Fall, damit f in einer Weise instanziiert werden kann, die die Typfamilie nicht besitzt?
Ich weiß nicht, ob ich das als Antwort schreiben sollte, weil es immer noch ziemlich hand-wavey ist, aber ich denke, das ist im Wesentlichen so:
Um einen (C k (B X)) => X k -Wert auszuwerten, müssen Sie einen konkreten Typ für k auswählen und auf den instance C k (B X) zeigen, der die Einschränkungen erfüllt. Um das zu tun, müssen Sie aussprechen, dass das Argument ' a ' der Klasse 'typeclass' die Form B f hat, aus der der Compiler den f -Typ extrahieren kann (und in diesem Fall X ermittelt). Dies kann erfolgen, bevor Sie die Instanz betrachten. Dies wäre der Punkt, an dem f unantastbar werden würde.
Um ein (F k ~ B X) => X k auszuwerten, ist es ein bisschen anders. Hier müssen Sie nicht auf eine konkrete Instanz verweisen, Sie müssen lediglich sicherstellen, dass wenn der Compiler die Typefamilie nach F k gesucht hat, dann wäre dieser Typ der gleiche Typ wie B X . Bevor aber die Instanz tatsächlich nachgeschlagen wird, kann der Compiler hier nicht folgern, dass F k die Form B f hat und damit auch nicht f mit dem äußeren Quantifizierungsargument wegen Unberührbarkeit vereinheitlichen.
Daher ist das Verhalten von GHC zumindest nicht völlig unangemessen. Ich bin mir immer noch nicht sicher, ob sich so verhalten soll.
OK, ich hatte eine Chance, damit zu spielen. Es gibt mehrere Ablenkungen:
In der Type Family Version gibt nur die Definition für f den Fehler 'f0' is untouchable an. (Sie können dies mit AllowAmbiguousTypes unterdrücken; das verschiebt den Fehler nur auf g .) Lassen Sie uns g hier ignorieren.
Dann ohne AllowAmbiguousTypes gibt die Fehlermeldung für f weitere Informationen:
Aha! ein rigid type variable Problem. Ich denke, weil f durch die Gleichheitsbedingung von k festgelegt wird, was auch starr ist, weil ...
Wenn Sie FunDep version ohne g wählen, bei welchen Typen können wir f aufrufen? Probieren Sie
Die Ablehnungsnachricht (für das Beispiel X String ) ist
Beachten Sie, dass die Nachricht über k , nicht f lautet, was aus dem FunDep ermittelt wird - oder wenn wir ein passendes k finden könnten.
Erläuterung
Die Signatur für die Funktion f sagt k ist existentiell quantifiziert / höher eingestuft. Dann können wir nicht zulassen, dass Typinformationen über k in den umgebenden Kontext gelangen. Wir können keinen (nicht unteren) Wert für k angeben, da sein Typ in forall eindringen würde.
Hier ist ein einfacheres Beispiel:
%Vor% So dass die ursprüngliche FunDep Version kompiliert ist eine Ablenkung: Es kann nicht bewohnt werden. (Und das ist ein häufiges Symptom mit FunDep s, nach meinem früheren Verdacht.)
Tags und Links haskell type-families functional-dependencies