`Let` Inferenz in Hindley-Milner

Question

Ich versuche, mich selbst Hindley-Milner Typ Inferenz beizubringen durch die Implementierung von Algorithmus W in der Sprache, die ich normalerweise verwende, Clojure. Ich stoße auf ein Problem mit let Inferenz, und ich bin mir nicht sicher, ob ich etwas falsch mache, oder wenn das Ergebnis, das ich erwarte, etwas außerhalb des Algorithmus erfordert.

Grundsätzlich mit Haskell-Notation, wenn ich versuche, den Typ dieser zu folgern:

\a -> let b = a in b + 1 

ich diese:

Num a => t -> a 

Aber ich sollte diese:

Num a => a -> a 

Noch einmal, ich mache das eigentlich in Clojure, aber ich glaube nicht, dass das Problem Clojure-spezifisch ist, also benutze ich die Haskell-Notation mach es klarer. Wenn ich es in Haskell versuche, bekomme ich das erwartete Ergebnis.

Wie dem auch sei, kann ich dieses spezielle Problem lösen, indem sie jeden let in eine Funktion Anwendung, zum Beispiel die Umwandlung:

\a -> (\b -> b + 1) a 

Aber dann verliere ich let Polymorphismus. Da ich keine Vorkenntnisse von HM habe, ist meine Frage, ob ich hier etwas verpasse oder ob dies genau die Art ist, wie der Algorithmus funktioniert.

EDIT

Falls jemand ein ähnliches Problem hat und fragt sich, wie ich es gelöst wurde folgende ich Algorith W Step By Step. Unten auf Seite 2 heißt es: "Es wird gelegentlich nützlich sein, die Typen Methoden zu Listen zu erweitern." Da es sich für mich nicht zwingend anhört, habe ich beschlossen, diesen Teil zu überspringen und ihn später erneut zu besuchen.

Ich übersetzte dann die ftv Funktion für TypeEnv direkt in Clojure wie folgt: (ftv (vals env)). Da ich ftv als cond Formular implementiert hatte und keine Klausel für seq s hatte, gab es einfach nil für (vals env) zurück. Dies ist natürlich genau die Art von Fehler, die ein statisches System zu fangen versucht! Wie auch immer, ich habe gerade die Klausel in ftv in Bezug auf die env Karte als (reduce set/union #{} (map ftv (vals env))) neu definiert und es funktioniert.

Answer 1

Es ist schwer zu sagen, was falsch ist, aber ich denke, Ihre Generalisierung ist falsch.

Geben Sie den Begriff manuell ein.

\a -> let b = a in b + 1 

Zuerst wir a mit einer frischen Art Variable zuzuordnen, sagen a :: t0.

Dann geben wir b = a ein. Wir bekommen auch b :: t0.

Jedoch, und das ist der Schlüsselpunkt, sollten wir nicht verallgemeinern den Typ b zu b :: forall t0. t0.Dies liegt daran, dass wir nur über eine Tyvar verallgemeinern können, die nicht in der Umgebung vorkommt: Hier haben wir stattdessen t0 in der Umgebung, da a :: t0 da ist.

Wenn Sie es verallgemeinern, erhalten Sie einen Weg zu allgemeinen Typ für b. dann b+1 wird b+1 :: forall t0. Num t0 => t0, und der gesamte Begriff bekommt forall t0 t1. Num t1 => t0 -> t1 seit die Typen für a und b sind nicht verwandt (t0, einmal verallgemeinert, kann alpha-konvertiert werden zu t1).