In Haskell können wir den folgenden Datentyp schreiben:
%Vor% Die Typvariable f hat die Art * -> * (d. h. es ist ein Konstruktor des unbekannten Typs). Daher hat Fix die Art (* -> *) -> * . Ich frage mich, ob Fix ein gültiger Typkonstruktor im Hindley-Milner-System ist.
Von dem, was ich auf Wikipedia gelesen habe, scheint Fix nicht gültig zu sein Typkonstruktor im Hindley-Milner-Typensystem, weil alle Typvariablen in HM konkret sein müssen (dh die Art * haben müssen). Ist das tatsächlich der Fall? Wenn Typvariablen in HM nicht immer konkret wären, würde dann HM unentscheidbar werden?
Es kommt darauf an, ob Typkonstruktoren eine Ausdruckssprache erster Ordnung (kein Reduktionsverhalten von Typkonstruktorausdrücken) oder eine höhere Ordnung (mit lambdas oder ähnlichen Konstrukten auf Typebene) bilden.
Im ersten Fall sind Constraints, die sich aus Fix ergeben, immer auf die allgemeinste Art und Weise vereinheitlichbar (unter der Annahme, dass wir bei HM bleiben). In jeder c a b ~ t -Gleichung muss t in einen konkreten Anwendungsausdruck mit derselben Form wie c a b aufgelöst werden, da c a b nicht auf einen anderen Ausdruck reduziert werden kann. Höherwertige Parameter sind kein Problem, da sie auch nur statisch dort sitzen, zB c [] ~ c f wird gelöst durch f = [] .
Im letzteren Fall ist c a b ~ t möglicherweise nicht lösbar. In einigen Fällen ist es gelöst durch c = \a b -> t , in anderen Fällen gibt es keinen allgemeinen Unifier.
Höhere Arten gehen über das grundlegende Hindley-Milner-System hinaus, aber sie können auf die gleiche Weise behandelt werden.
Sehr grob, analysiert HM den Syntaxbaum eines Ausdrucks, ordnet jedem Unterausdruck eine freie Typvariable zu und erzeugt einen Satz von Gleichgewichtsbedingungen gegenüber Typbegriffen, die Typvariablen gemäß den Typisierungsregeln umfassen. Das Gleiche kann mit höheren Arten gemacht werden.
Dann werden die Beschränkungen durch Vereinigung gelöst. Ein typischer Schritt im Vereinheitlichungsalgorithmus ist (Pseudohaskell folgt)
%Vor%(Beachten Sie, dass dies nur ein Teil des Vereinigungsalgorithmus ist.)
Über F , G sind Typkonstruktorsymbole und keine Variablen. Bei der höheren Vereinheitlichung müssen wir auch F , G als Variablen berücksichtigen.
Wir könnten die folgende Regel versuchen:
Aber warte! Das obige ist nicht korrekt, da z.B. f Int ~ Either Bool Int muss vereinheitlicht werden, wenn f ~ Either Bool . Also müssen wir auch den Fall betrachten, in dem n/=k . Im Allgemeinen ist ein einfacher Regelsatz
(Dies ist wiederum nur ein Teil des Vereinheitlichungsalgorithmus. Andere Fälle müssen ebenfalls behandelt werden, wie Andreas Rossberg unten ausführt.)
Tags und Links haskell functional-programming hindley-milner type-inference ocaml