Jemand einmal zeigte mir ein kleines "Trick" in SML, wo sie über 3 oder 4 Funktionen in ihrer REPL geschrieben und der resultierende Typ für den letzten Wert war extrem lang (wie viele Seiten scrollen lang).Wachstum von Typ Definition in SML mit Hindley Milner Typ Inferenz
Weiß jemand, welcher Code einen so langen Typ generiert oder ob es einen Namen für diese Art von Verhalten gibt?
Die Typen, die von Hindley/Milner-Typ-Inferenz abgeleitet werden, können exponentiell groß werden, wenn Sie sie in der richtigen Weise zusammensetzen. Zum Beispiel:
fun f x = (x, x, x)
val t = f (f (f (f (f 0))))
Hier ist ein verschachtelter t triple, dessen Verschachtelungstiefe entspricht der Anzahl n von Invokationen von f. Folglich hat der Gesamttyp die Größe 3^n.
Dies ist jedoch nicht der schlechteste Fall, da der Typ eine regelmäßige Struktur hat und durch einen Graph effizient im linearen Raum dargestellt werden kann (weil auf jeder Ebene alle drei konstituierenden Typen gleich sind und geteilt werden können) .
Der eigentliche schlimmste Fall verwendet polymorphe Instanziierung dieses zu besiegen:
fun f x y z = (x, y, z)
val p1 = (f, f, f)
val p2 = (p1, p1, p1)
val p3 = (p2, p2, p2)
In diesem Fall ist der Typ wieder exponentiell groß, aber im Gegensatz zu oben, alle konstituierenden Typen sind verschiedener frischer Typ Variablen, so dass auch eine Diagrammdarstellung wächst exponentiell (in der Anzahl der pN-Deklarationen).
Also ja, Hindley/Milner-Stil Typ Rückschluss ist im schlimmsten Fall exponentiell (in Raum und Zeit). Es ist jedoch darauf hinzuweisen, dass die exponentiellen Fälle nur auftreten können, wenn Typen exponentiell groß werden - d. H. In Fällen, in denen Sie nicht einmal ohne Typschluss schlussfolgern können.
Awesome Erklärung nicht nur wie es geht, sondern vor allem warum dies geschieht. Vielen Dank! – jkcorrea
Recht, aber in diesem bestimmten Fall wird die Worst-Case-Komplexität des Inferenzsystems ausgestellt und der resultierende Typ umfasst viele Seitenrollen. Nur neugierig, wie man das neu erstellt. – jkcorrea
Nun "viele Seitenrollen" in der Frage enthalten - das ist eine andere Version von "long" als ich denke. – user2864740