Verwirrung über Haskell-Typ-Inferenz

Question

Ich habe gerade angefangen, Haskell zu lernen. Als Haskell statisch typisiert und polymorphe Typinferenz hat, ist die Art der Identitätsfunktion

id :: a -> a 

was darauf hindeutet, id jede Art als Parameter übernimmt und sich selbst zurück. Es funktioniert gut, wenn ich versuche:

a = (id 1, id True) 

Ich nehme nur, dass zum Zeitpunkt der Kompilierung, die erste ID ist Num a :: a -> a, und die zweite ID ist Bool -> Bool. Wenn ich den folgenden Code versuchen, gibt es eine Fehlermeldung:

foo f a b = (f a, f b) 
result = foo id 1 True 

Es zeigt den Typ eines müssen die gleiche Art von b sein, da sie mit

result = foo id 1 2 

gut funktioniert Aber ist das wahr, dass Der Typ des ID-Parameters kann polymorph sein, so dass a und b unterschiedliche Typen sein können.

Answer 1

In Ordnung, das ist eine seltsame gruselige Ecke von Haskells Typensystem. Das Problem hier ist, dass es zwei Möglichkeiten gibt, um die Funktion foo zu schließen.

Der zweite Typ ist der, den Sie wollen, aber der erste Typ ist der, den Sie bekommen. Der zweite Typ, wie amalloy hervorgehoben wurde, ist ein Rang-2-Typ (wir werden ignorieren, was die beiden bedeuten, aber lies die Einführung in "Practical type inference for arbitrary-rank types", wenn du eine gute Erklärung der Ränge willst - lass dich nicht vom Akademiker abschrecken Art der PDF - Datei als Anfang ist zugänglich und klar geschrieben).

Wir werden die Definition von höherrangigen Typen vorerst zurückstellen und nur sagen, dass das Problem darin besteht, dass GHC nicht auf den Rang-2-Typ schließen kann. Zitieren Sie das Papier:

Complete type inference is known to be undecidable for higher-rank (impredicative) type systems, but in practice programmers are more than willing to add type annotations to guide the type inference engine, and to document their code....

Kfoury and Wells show that typeability is decidable for rank ≤ 2, and undecidable for all ranks ≥ 3 (Kfoury & Wells, 1994). For the rank-2 fragment, the same paper gives a type inference algorithm. This inference algorithm is somewhat subtle, does not interact well with user-supplied type annotations, and has not, to our knowledge, been implemented in a production compiler.

Unentscheidbare bedeutet, dass es keinen Algorithmus, der immer führt eine korrekte Ja-oder-Nein-Entscheidung. So, da haben Sie es: unmöglich, einen Rang-3-oder-höher-Typ abzuleiten, und es ist zu verdammt schwer, den Rang-2-Typ abzuleiten.

Jetzt, zurück auf Rang 2. Die (forall a. a -> a) ist, was es Rang-2 macht. There's already an excellent Stack Overflow question about what the forall keyword means so werde ich Sie zu, dass beziehen, aber im Grunde bedeutet es, Sie in der Lage sind f a und f b im Ausdruck zu nennen (f a, f b) während a und b verschiedene Arten, sein, das ist, was Sie in erster Linie wollten vor allem diese heiße Sauerei.

Eine letzte Sache: Der Grund, warum Sie forall s in GHCi normalerweise nicht sehen, ist, dass irgendwelche forall s auf dem sehr äußeren Bereich weg sind. So entspricht forall a b. (a -> b) -> a -> a -> (b, b)(a -> b) -> a -> a -> (b, b).

Insgesamt ist dies ein Schwachpunkt der Sprache, die schlecht erklärt wird.

(Hutspitze in den Kommentaren @amalloy.)