Können wir Typvariablen in der Konstruktorposition im Hindley-Milner-Typsystem haben?

Question

In Haskell wir den folgenden Datentyp schreiben:

data Fix f = Fix { unFix :: f (Fix f) } 

Die Art variable f hat die Art * -> * (d.h. es ist ein unbekannter Typkonstruktor). Daher hat Fix die Art (* -> *) -> *. Ich fragte mich, ob Fix ein gültiger Typenkonstruktor im Hindley Milner Typ System war.

Von dem, was ich read on Wikipedia, es scheint, dass Fix ist kein gültiger Typkonstruktor in das Typsystem Hindley Milner, da alle Variablen vom Typ HM konkret sein muss (d muss die Art haben *). Ist das tatsächlich der Fall? Wenn Typvariablen in HM nicht immer konkret wären, würde HM dann unentscheidbar werden?

Answer 1

Es kommt darauf an, ob Typkonstruktoren eine Ausdruckssprache erster Ordnung (kein Reduktionsverhalten von Typkonstruktorausdrücken) oder eine höhere (mit lambdas oder ähnlichen Konstrukten auf Typebene) bilden.

Im ersteren Fall sind die sich aus Fix ergebenden Beschränkungen immer auf eine allgemeinste Art und Weise vereinheitlichbar (vorausgesetzt, dass wir bei HM bleiben). In jeder c a b ~ t Gleichung muss t zu einem konkreten Anwendungsausdruck mit der gleichen Form wie c a b aufgelöst werden, da c a b nicht auf einen anderen Ausdruck reduziert werden kann. Höhergestufte Parameter sind kein Problem, da sie auch nur statisch dort sitzen, beispielsweise wird c [] ~ c f durch f = [] gelöst.

In letzterem Fall kann c a b ~ t möglicherweise oder nicht lösbar sein. In einigen Fällen ist es durch c = \a b -> t gelöst, in anderen Fällen gibt es keinen allgemeinen Unifier.

Answer 2

Höhere Arten gehen über das grundlegende Hindley-Milner-Typsystem 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 generiert einen Satz von Gleichungsbedingungen gegenüber Typbegriffen, die Typvariablen gemäß den Typisierungsregeln enthalten. Das gleiche kann mit höheren Arten gemacht werden.

Dann werden die Einschränkungen durch Vereinheitlichung gelöst. Ein typischer Schritt bei der Vereinigung Algorithmus (pseudo-Haskell folgt)

(F t1 ... tn := G s1 ... sk) = 
    | n/=k || F/=G -> fail 
    | otherwise  -> { t1 := s1 , ... , tn := sn } 

(Beachten Sie, dass dies nur ein Teil des Unifikationsalgorithmus.)

Above F, G sind Typkonstruktor Symbole, und nicht Variablen. Bei der höheren Vereinheitlichung müssen wir auch die Variablen F, G berücksichtigen. Wir könnten versuchen, die folgende Regel:

(f t1 ... tn := g s1 ... sk) = 
    | n/=k   -> fail 
    | otherwise  -> { f := g , t1 := s1 , ... , tn := sn } 

Aber warten Sie! Das obige ist nicht korrekt, da z.B. f Int ~ Either Bool Int muss vereinheitlichen, wenn f ~ Either Bool. Also müssen wir auch den Fall betrachten, wo n/=k.Im Allgemeinen ist ein einfacher Regelsatz ist

(f t := g s) = 
    { f := g , t := s } 
(F := G) =  -- rule for atomic terms 
    | F /= G -> fail 
    | otherwise -> {} 

(Auch dies ist nur ein Teil des Unifikationsalgorithmus. Andere Fälle auch behandelt werden müssen, wie Andreas Roßberg unten weist darauf hin.)