Warum überprüft diese Haskell-Code-Typ mit fundeps aber einen unantastbaren Fehler mit Typfamilien?

Question

Da einige Typdefinitionen:

data A 
data B (f :: * -> *) 
data X (k :: *) 

... und das typeclass:

class C k a | k -> a 

... diese (sehr gekünstelt im Sinne eines minimalen Beispiel) Funktionsdefinitionen typecheck:

f :: forall f. (forall k. (C k (B f)) => f k) -> A 
f _ = undefined 

g :: (forall k. (C k (B X)) => X k) -> A 
g = f 

Wenn wir jedoch eine Typfamilie anstelle einer Klasse mit einer funktionalen Abhängigkeit verwenden:

type family F (k :: *) 

... dann die entsprechenden Funktionsdefinitionen nicht typecheck:

f :: forall f. (forall k. (F k ~ B f) => f k) -> A 
f _ = undefined 

g :: (forall k. (F k ~ B X) => X k) -> A 
g = f 

• Couldn't match type ‘f0’ with ‘X’ 
    ‘f0’ is untouchable 
     inside the constraints: F k ~ B f0 
     bound by a type expected by the context: 
       F k ~ B f0 => f0 k 
    Expected type: f0 k 
    Actual type: X k 
• In the expression: f 
    In an equation for ‘g’: g = f 

I Abschnitt 5.2 der the OutsideIn(X) paper lesen, die berührbaren und unberührbaren Typ Variablen, und ich Art beschreibt verstehe, was hier vor sich geht. Wenn ich ein zusätzliches Argument f hinzufügen, die die Wahl der f außerhalb des inneren forall drückt, dann geht das Programm typechecks:

f :: forall f a. f a -> (forall k. (F k ~ B f) => f k) -> A 
f _ _ = undefined 

g :: forall a. X a -> (forall k. (F k ~ B X) => X k) -> A 
g = f 

Doch was speziell hat mich so verwirrt, in diesem Beispiel ist, warum die funktionale Abhängigkeit verschiedener hat Verhalten. Ich habe gehört, dass Leute zu verschiedenen Zeiten behaupten, funktionale Abhängigkeiten wie diese seien äquivalent zu einer Typfamilie plus einer Gleichheit, aber dies zeigt, dass das nicht wirklich wahr ist.

Welche Informationen liefert die funktionale Abhängigkeit in diesem Fall, die f in einer Weise instanziiert werden kann, die die Typenfamilie nicht enthält?

Answer 1

Ich weiß nicht, ob ich dies als eine Antwort schreiben soll, weil es immer noch ziemlich hand wavey ist, aber ich denke, das ist, was im Wesentlichen auf ist ist los:

einen (C k (B X)) => X k Wert zu bewerten, müssen Sie entscheiden, ein konkreter Typ für k, und zeigen Sie auf die instance C k (B X), die die Einschränkungen erfüllt. Um dies zu tun, müssen Sie ausdrücken, dass die Klasse 'a Argument die Form B f hat, aus dem der Compiler den f Typ extrahieren kann (und herausfinden, dass es in diesem Fall X ist) – wichtig ist, kann es vor tatsächlich suchen an der Instanz, die der Punkt wäre, an dem f unantastbar werden würde.

Um eine (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 garantieren, dass , wenn der Compiler die typefamily für F k nachgeschlagen hat, dann wäre dieser Typ der gleiche Typ wie B X. Bevor jedoch die Instanz tatsächlich nachgeschlagen wird, kann der Compiler hier nicht folgern, dass F k die Form B f hat, und daher auch nicht verwenden, um f mit dem äußeren Quantifizierungsargument wegen Unberührbarkeit zu vereinheitlichen.

Daher ist GHC Verhalten zumindest nicht völlig unangemessen. Ich bin mir immer noch nicht sicher, ob es sich so verhalten sollte.

Answer 2

OK Ich hatte eine Chance, damit zu spielen. Es gibt mehrere Ablenkungen:

In der Type Family-Version gibt nur die Definition für f Fehler 'f0' is untouchable. (Sie können das mit AllowAmbiguousTypes unterdrücken; das verschiebt den Fehler einfach auf g). Lassen Sie uns g hier auf ignorieren.

Dann ohne AllowAmbiguousTypes die Fehlermeldung für f gibt weitere Informationen:

• Couldn't match type ‘f0’ with ‘f’ 
    ‘f0’ is untouchable 
     inside the constraints: F k ~ B f0 
     bound by the type signature for: 
       f :: F k ~ B f0 => f0 k 
    ‘f’ is a rigid type variable bound by 
    the type signature for: 
     f :: forall (f :: * -> *). (forall k. F k ~ B f => f k) -> A 
    Expected type: f0 k 
    Actual type: f k 

Aha! ein rigid type variable Problem. Ich denke, weil f durch die Gleichheit Einschränkung von k festgelegt ist, die ebenfalls starr ist, weil ...

zum FunDep Version Drehen ohne g, auf welche Arten können wir f nennen? Versuchen

f (undefined undefined :: X a)   -- OK 
f (undefined "string" :: X String)  -- rejected 
f Nothing        -- OK 
f (Just 'c')        -- rejected 

die Ablehnungsnachricht (für das X String Beispiel)

• Couldn't match type ‘k’ with ‘String’ 
    ‘k’ is a rigid type variable bound by 
    a type expected by the context: 
     forall k. C k (B X) => X k 
    Expected type: X k 
    Actual type: X String 
• In the first argument of ‘f’, namely 
    ‘(undefined "string" :: X String)’ 

Beachten Sie die Nachricht über k ist, nichtf, die aus dem FunDep bestimmt wird - oder wäre, wenn wir könnten finden Sie eine geeignete k.

Erklärung

Die Signatur für die Funktion f sagt k existenzquantifizierte ist/höherrangigen. Dann können wir keine Typinformationen über k in den umgebenden Kontext entkommen lassen. Wir können keinen (nicht unteren) Wert für k angeben, da sein Typ in die forall eindringen würde.

Hier ist ein einfacheres Beispiel:

f2 :: forall f. (forall k. f k) -> A 
f2 _ = undefined 

f2 Nothing         -- OK 
f2 (Just 'c')        -- rejected rigid type var 

so dass die ursprüngliche FunDep Version kompiliert ist eine Ablenkung: Es ist nicht bewohnt werden kann. (Und das ist ein häufiges Symptom mit FunDep s, nach meinem früheren Verdacht.)