Ich spielte mit dem Haskell Reflektionspaket , und ich stieß auf einen Typfehler, den ich nicht vollständig verstehe. Zuerst habe ich versucht, die folgende Funktion zu schreiben, die gerne checket:
%Vor%Interessanterweise macht dieses etwas andere Programm nicht typecheck:
%Vor%%Vor%
Die Ausdrücke sind identisch, beachten Sie jedoch den Unterschied zwischen den Typ-Signaturen:
%Vor% Ich finde das merkwürdig. Auf den ersten Blick ist das ungültig, weil im zweiten Beispiel der Skolem s seinen Gültigkeitsbereich verlassen würde. Das stimmt jedoch nicht wirklich - die Fehlermeldung erwähnt Skolem Escape im Gegensatz zu diesem etwas anderen Programm nie:
%Vor%
Also vielleicht ist hier etwas anderes im Spiel.
Untersucht man den Typ von reify , wird ein wenig klar, dass etwas nicht stimmt:
Die Bereiche von a und s unterscheiden sich deutlich, so dass es sinnvoll erscheint, dass GHC sie nicht vereinigen würde. Es scheint jedoch etwas über die lokale Gleichheitsbedingung, die durch die funktionale Abhängigkeit von Reifies verursacht wird, eine Art von merkwürdigem Verhalten zu verursachen. Interessanterweise prüft dieses Funktionspaar Folgendes:
... aber das Entfernen der Gleichheitsbedingung in der Typsignatur von foo führt dazu, dass sie nicht typenüberprüfen können und einen Skolem-Escape-Fehler erzeugen:
An diesem Punkt bin ich perplex. Ich habe ein paar (sehr verwandte) Fragen.
Warum kann reifyBad die Typüberprüfung überhaupt nicht ausführen?
Genauer gesagt, warum erzeugt es einen Fehler fehlende Instanz ?
Darüber hinaus ist dieses Verhalten erwartet und gut definiert, oder ist es nur ein seltsamer Rand Fall der Typchecker, die passiert, um dieses bestimmte Ergebnis zu produzieren?
Die Skolem-Anforderung besagt im Wesentlichen, dass r im obigen Typ nicht von der s abhängen kann, die im zweiten Argument quantifiziert wird. Andernfalls würde es in der Tat seinen Geltungsbereich "verlassen", da reify r zurückgibt.
In
%Vor% Wir sehen, dass das zweite Argument von reify \(_ :: Proxy t) -> p @t 'seq' () ist, also wäre der Typ r der Rückgabetyp dieser Funktion, also () . Da r ~ () nicht von s abhängt, gibt es hier kein Problem.
Allerdings erfordert p @t gemäß dem Typ von p Reifies t t .
Da reify t ~ s wählt, ist die Einschränkung identisch mit Reifies s s .
Stattdessen liefert reify nur Reifies s a , wobei a den Typ von undefined darstellt.
Der subtile Punkt hier ist, dass, während undefined einen beliebigen Typ a erzeugen kann, der Typ-Checker s und a nicht vereinen kann. Dies liegt daran, dass eine Funktion mit demselben Typ wie reify berechtigt ist, nur einen Wert eines festen (starren) Typs a zu erhalten, und dann so viele Typen s wie gewünscht auswählen. Die Vereinheitlichung all dieser s s mit einer einzigen a wäre falsch, wodurch die Auswahl von s by reify effektiv eingeschränkt wird.
Stattdessen in der Variante
%Vor% hier wird r als Rückgabetyp von \(_ :: Proxy t) -> p @t angenommen, was Proxy t ist, wobei t ~ s . Da r ~ Proxy s von s abhängt, lösen wir einen Skolem-Fehler aus.
Tags und Links haskell