Quelltext der Seite Typinferenz nach Hindley-Milner

'''Hindley-Milner''' ('''HM''') ist ein Verfahren der [[Typinferenz]] mit [[Polymorphie (Programmierung)#Parametrische Polymorphie|parametrischem Polymorphismus]] für den [[Lambda-Kalkül]]. Es wurde erstmals von [[J. Roger Hindley]]<ref>R. Hindley, (1969) The Principal Type-Scheme of an Object in Combinatory Logic, Transactions of the American Mathematical Society, Vol. 146, S. 29–60 {{JSTOR|1995158}}</ref> beschrieben und später von [[Robin Milner]]<ref>Milner, (1978) A Theory of Type Polymorphism in Programming. Journal of Computer and System Science (JCSS) 17, S. 348–374 [http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.67.5276&rep=rep1&type=pdf online]</ref> wiederentdeckt.
[[Luis Damas]] trug eine genaue formale Analyse und einen Beweis der Methode in seiner Doktorarbeit<ref>Luis Damas (1985): Type Assignment in Programming Languages. PhD thesis, University of Edinburg (CST-33-85)</ref> bei, weshalb das Verfahren auch als [[Damas-Milner]]<ref name="Damas">Damas, Milner (1982), Principal type-schemes for functional programs. 9th Symposium on Principles of programming languages (POPL'82) S. 207–212, ACM: {{Webarchiv|url=http://ian-grant.net/hm/milner-damas.pdf |wayback=20120324053855 |text=PDF }}</ref> bezeichnet wird. Unter den herausragenden Eigenschaften des HM sind Vollständigkeit und die Fähigkeit, den allgemeinsten Typ einer gegebenen Quelle ohne Hinzunahme von Annotationen oder sonstigen Hinweisen bestimmen zu können. HM ist ein effizientes Verfahren, das die Typisierung nahezu in linearer Zeit bzgl. der Größe der Quelle ermitteln kann, womit es praktisch zum Typisieren großer Programme anwendbar ist. HM wird bevorzugt in [[Funktionale Programmierung|funktionalen Sprachen]] wie OCaml/Reason eingesetzt. Es wurde erstmals als Teil des [[Typisierung (Informatik)|Typsystems]] der Programmiersprache [[ML (Programmiersprache)|ML]] implementiert. Seitdem wurde HM auf verschiedene Weise erweitert, insbesondere durch beschränkte Typen, wie sie in [[Haskell (Programmiersprache)|Haskell]] verwendet werden.

== Einleitung ==
Damas und Milner<ref name="Damas" /> trennen in der Gliederung ihrer Original-Veröffentlichung zwei sehr verschiedene Aufgaben, wobei die erste darin besteht, zu beschreiben, welche Typen ein Ausdruck haben kann. Die andere ist, einen Algorithmus anzugeben, der tatsächlich einen Typ ermittelt.

Beide Aspekte getrennt voneinander zu betrachten, erlaubt, sich eigens auf die Logik (d.&nbsp;h. Bedeutung) hinter dem Algorithmus konzentrieren und zugleich einen Prüfstein für die Eigenschaften des Verfahrens festlegen zu können. Wie Ausdrücke und Typen zueinander passen, wird mit Hilfe eines [[Kalkül|Deduktionssystems]] beschrieben. Wie jedes [[Formales System|Beweissystem]] erlaubt es, auf verschiedenen Wegen zu einem Schluss zu gelangen. Da ein und derselbe Ausdruck begründbar verschiedene Typen haben kann, kann das Deduktionssystem auch zu durchaus unterschiedlichen Schlüssen über einen Ausdruck kommen. Im Gegensatz dazu ist bei der Typinferenz-Methode selbst ([[#Algorithmus W|Algorithmus W]]) jeder Ausführungsschritt eindeutig bestimmt. Natürlich können in der Konstruktion des Algorithmus Entscheidungen getroffen worden sein, die so nicht in der Logik vorkommen, und eine genauere Betrachtung und Begründung verlangen, die ohne die obige Differenzierung nicht sichtbar würde.

== Die Syntax ==
{| class="float-right wikitable infobox"
|align=center style="background:#e0e0ff"|'''Ausdrücke'''
|-
| <math>
  \begin{array}{lrll}
  e & =     & x                                   & \textrm{Variable}\\
    & \vert & e\ e'                                & \textrm{Anwendung}\\
    & \vert & \lambda\ x\ .\ e                    & \textrm{Abstraktion} \\
    & \vert & \mathtt{let}\ x = e\ \mathtt{in}\ e \\
  \end{array}
  </math>
|-
|align=center style="background:#e0e0ff"|'''Typen'''
|-
| <math>
  \begin{array}{llrll}
  \textrm{mono} & \tau   &=     & \alpha                    & \ \textrm{Variable} \\
                    &        &\vert &  D\ \tau\dots\tau         & \ \textrm{Anwendung} \\
  \textrm{poly} & \sigma &=    & \tau                                           \\
                    &        &\vert& \forall\ \alpha\ .\ \sigma & \ \textrm{Quantor}\\
  \\
  \end{array}
  </math>
|}

Logik und Algorithmus teilen sich die Begriffe "Ausdruck" und "Typ", deren Form durch die Syntax präzisiert wird.

Die zu typisierenden Ausdrücke sind die des [[Lambda-Kalkül]]s, erweitert um einen let-Ausdruck.

Die Form <math>e\ e'</math> stellt die auch oft als <math>e(e')</math> geschriebene Funktionsanwendung dar, während die Abstraktion
<math>\lambda\ x.e</math> die [[anonyme Funktion]] bzw. das Funktionsliteral meint, die inzwischen in vielen zeitgenössischen Programmiersprachen verfügbar ist, dort vielleicht nur wortreicher etwa als <math>\mathtt{function}\,(x)\ \mathtt{return}\ e\ \mathtt{end}</math> ausgeschrieben.

Das Gesamt der Typen (Sorten) teilt sich in zwei Gruppen, die Mono- und Polytypen genannt werden.<ref group="note">Polytypen werden in der Originalpublikation als Typ-Schemata ("type schemes") bezeichnet.</ref>

Monotypen <math>\tau</math>, syntaktisch [[Term]]e, bezeichnen immer ''bestimmte'' Typen in dem Sinne, dass sie gleich nur sich selbst und verschieden von allen anderen sind. Charakteristische Vertreter der Monotypen sind Typkonstanten wie <math>int</math> oder <math>string</math>.
Typen können parametrisch sein, wie z.&nbsp;B. <math>Map\ (Set\ string)\ int</math>.
All diese Typen sind Beispiele von ''Anwendungen'' von Typfunktionen <math>D</math>, z.&nbsp;B. <math>\left\{int^0, string^0, Map^2, Set^1\right\} \subset D</math> in den vorangegangenen Beispielen, wobei die hochgestellte Ziffer die Zahl der Typparameter angibt.
Während die Wahl von <math>D</math> grundsätzlich beliebig ist, ''muss'' sie im Zusammenhang des HM wenigstens den bequemerweise [[Infixnotation|infix]] geschriebenen Funktionstyp <math>\rightarrow^2</math> enthalten. Beispielsweise hat eine Funktion, die ganze Zahlen auf Zeichenketten abbildet, den Typ <math>int\rightarrow string</math>.<ref group="note">Die parametrischen Typen <math>D\ \tau\dots\tau</math> sind in der Originalpublikation über HM nicht enthalten und für die Darstellung der Methode auch nicht erforderlich. Keine der Inferenzregeln ist für sie zuständig oder würde ihre Abwesenheit bemerken. Dasselbe gilt für die nichtparametrischen "primitiven Typen" im betreffenden Papier. Die gesamte Maschinerie polymorpher Typinferenz kann ohne sie definiert werden. Sie sind hier teils der Beispiele wegen aufgenommen, aber vor allem, da sich die Natur des HM ganz und gar um polymorphe Typen dreht. Der parametrische Polymorphismus tritt im Original nur in spezieller Form durch den in den Inferenzregeln fest verdrahteten Funktionstyp <math>\tau\rightarrow\tau</math> auf, der zwei polymorphe Parameter hat und hier nur als spezieller Fall behandelt wird.</ref>

Vielleicht etwas irritierenderweise sind Typvariablen ebenfalls Monotypen. Eine allein stehende Typvariable <math>\alpha</math> bezeichnet einen Typ, der genau so konkret ist wie etwa <math>int</math> oder <math>\beta</math> und von beiden verschieden ist. Eine als Monotyp auftretende Typvariable verhält sich gerade so, als wäre sie eine Typkonstante, über die man nur eben keine weiteren Informationen besitzt. Entsprechend bildet eine Funktion mit dem Typ <math>\alpha\rightarrow\alpha</math> nur Werte des Typs <math>\alpha</math> auf sich selbst ab und kann nur auf Werte dieses Typs angewendet werden und auf keine anderen sonst.

Im Gegensatz dazu kann eine Funktion mit dem Polytyp <math>\forall\alpha.\alpha\rightarrow\alpha</math> ''jeden'' Wert auf einen Wert gleichen Typs abbilden. Die [[Identische Abbildung|identische Funktion]] ist ein Wert für diesen Typ. Als weiteres Beispiel ist <math>\forall\alpha.(Set\ \alpha)\rightarrow int</math> der Typ einer Funktion, die beliebige endliche Menge auf ganze Zahlen abbildet. Die Zahl der Elemente der Menge ist ein Wert für diesen Typ. Quantoren dürfen allerdings nur auf oberster Ebene auftreten, d.&nbsp;h. der Typ <math>\forall\alpha.\alpha\rightarrow\forall\alpha.\alpha</math> beispielsweise ist durch die Syntax ausgeschlossen. Ferner sind Monotypen eine Teilmenge der Polytypen, so dass Typen insgesamt die allgemeine Form <math>\forall\alpha_1\dots\forall\alpha_n.\tau</math> haben.

=== Freie Typvariablen ===
{| class="float-right wikitable infobox"
|align=center style="background:#e0e0ff"|'''Freie Typvariablen'''
|-
| <math>
\begin{array}{ll}
\text{frei}(\ \alpha\ ) &=\ \left\{\alpha\right\}\\
\text{frei}(\ D\ \tau_1\dots\tau_n\ ) &=\ \bigcup\limits_{i=1}^n{\text{frei}(\ \tau_i\ )} \\
\text{frei}(\ \forall\ \alpha\ .\ \sigma\ ) &=\ \text{frei}(\ \sigma\ )\  -\  \left\{\alpha\right\}\\
\end{array}
</math>
|}

In einem Typ <math>\forall\alpha_1\dots\forall\alpha_n.\tau</math> ist das Symbol <math>\forall</math> der die Typvariablen <math>\alpha_i</math> im Monotyp <math>\tau</math> bindende Quantor. Die Variablen <math>\alpha_i</math> heißen ''quantifiziert''. Jedes Auftreten einer quantifizierten Variablen in <math>\tau</math> heißt ''gebunden'' und alle ungebundenen Typvariablen heißen ''frei''. Wie im [[Lambda-Kalkül#Formale Definition|Lambda-Kalkül]] ist der Begriff der [[Freie Variable und gebundene Variable|freien und gebundenen Variablen]] grundlegend für das Verständnis der Bedeutung der Typen.

Dies ist sicherlich der schwierigste Teil des HM, vielleicht weil Polytypen, die freie Typvariablen enthalten, nicht in Programmiersprachen wie [[Haskell (Programmiersprache)|Haskell]] ausgedrückt werden können. Genauso gibt es keine freien Variablen in [[Prolog (Programmiersprache)|Prolog]]-Klauseln. Insbesondere mit beiden Sprachen erfahrene Entwickler, die somit eigentlich alle Voraussetzungen für den HM kennen, können diesen Punkt leicht übersehen. In Haskell beispielsweise sind alle Typvariablen implizit quantifiziert, z.&nbsp;B. bedeutet der Haskell-Typ <math>\texttt{a~->~a}</math> hier <math>\forall\alpha.\alpha\rightarrow\alpha</math>. Da Typen wie
<math>\alpha\rightarrow\alpha</math>, obwohl sie durchaus in Haskell auftreten können, dort nicht ausdrückbar sind, können sie leicht mit der quantifizierten Version verwechselt werden.

Welche Funktionen können nun einen Typ wie z.&nbsp;B. <math>\forall\beta.\beta\rightarrow\alpha</math>, d.&nbsp;h. eine Mischung von gebundenen und ungebundenen Typvariablen, enthalten und was bedeutet eine freie Typvariable darin?

{| class="float-right wikitable infobox"
|align=center style="background:#e0e0ff"|'''Beispiel 1'''
|-
| <math>
\begin{array}{l}
\textbf{let}\ bar\ [\forall\alpha.\forall\beta.\alpha\rightarrow(\beta\rightarrow\alpha)] = \lambda\ x.\\
\quad\textbf{let}\ foo\ [\forall\beta.\beta\rightarrow\alpha] = \lambda\ y.x\\
\quad\textbf{in}\ foo\\
\textbf{in}\ bar
\end{array}
</math>
|}

In Beispiel 1 ist der let-Ausdruck <math>foo</math> mit Typ-Annotationen in eckigen Klammern versehen. Offensichtlich wird der Parameter <math>y</math> im Körper nicht verwendet, wohl aber die im äußeren Kontext von <math>foo</math> gebundene Variable <math>x</math>. Als Konsequenz akzeptiert <math>foo</math> jeden Wert als Argument, während sie einen Wert liefert, der außerhalb gebunden ist und mithin auch sein Typ.

Im Gegensatz dazu hat <math>bar</math> den Typ <math>\forall\alpha.\forall\beta.\alpha\rightarrow(\beta\rightarrow\alpha)</math>, in dem alle Typvariablen gebunden auftreten. Wertet man z.&nbsp;B. <math>bar\ 1</math> aus, erhält man als Ergebnis eine Funktion vom Typ <math>\forall\beta.\beta\rightarrow\ int</math>, was perfekt wiedergibt, dass der Monotyp <math>\alpha</math> von <math>foo</math> in <math>\forall\beta.\beta\rightarrow\alpha</math> durch den Aufruf verfeinert wurde.

In diesem Beispiel wird die freie Monotypvariable <math>\alpha</math> im Typ von <math>foo</math> durch die Quantifikation im äußeren Geltungsbereich mit Bedeutung beladen, nämlich im Typ von <math>bar</math>. Dies heißt im Zusammenhang dieses Beispiels, dass dieselbe Typvariable <math>\alpha</math> sowohl gebunden als auch frei in verschiedenen Typen auftritt. Insofern kann eine freie Typvariable ohne Kenntnis des Kontexts nicht besser interpretiert werden als zu konstatieren, dass es sich um einen Monotyp handelt. Anders gesagt ist eine Typung im Allgemeinen ohne Kenntnis des Kontexts nicht aussagekräftig.

=== Kontext und Typung ===
{| class="float-right wikitable infobox"
|align=center style="background:#e0e0ff"|'''Syntax'''
|-
| <math>
\begin{array}{llrl}
  \text{Kontext}     & \Gamma & = & \epsilon\ \mathtt{(leer)}\\
                     &        & \vert& \Gamma,\ x : \sigma\\
  \text{Typung}      &        & = & \Gamma \vdash e : \sigma\\
\\
\end{array}
</math>
|-
|align=center style="background:#e0e0ff"|'''Freie Typvariablen'''
|-
|align=center|<math>
\begin{array}{ll}
\text{frei}(\ \Gamma\ ) &=\ \bigcup\limits_{x:\sigma \in \Gamma}\text{frei}(\ \sigma\ )
\end{array}
</math>
|}

Um die bislang getrennten Teile der Syntax, Ausdrücke und Typen sinnvoll zusammenzubringen, wird also ein Drittes, der Kontext, benötigt. Syntaktisch ist dieser einer Liste von Paaren <math>x:\sigma</math>,
[[Belegung (Mathematik)|Belegung]] (s.&nbsp;a. [[Belegung (Logik)|Belegung]], [[Relation (Mathematik)|Zuordnung]], [[Zuweisung]]) genannt, die jeder Wertvariablen <math>x_i</math> im Kontext einen Typ <math>\sigma_i</math> zuordnet. Alle drei Teile zusammen ergeben eine ''Typung'' der Form <math>\Gamma\ \vdash\ e:\sigma</math>, die aussagt, dass unter der Annahme <math>\Gamma</math>
der Ausdruck <math>e</math> den Typ <math>\sigma</math> hat.

Da nun die vollständige Syntax zur Verfügung steht, kann schließlich eine sinnvolle Aussage über den Typ von
<math>foo</math> in Beispiel 1 gemacht werden, nämlich <math>x:\alpha \vdash \lambda\ y.x : \forall\beta.\beta\rightarrow\alpha</math>.
Im Gegensatz zu den vorangehenden Formulierungen ist die Monotypvariable <math>\alpha</math> nicht länger frei, d.&nbsp;h. bedeutungslos, sondern im Kontext als Typ der Wertvariablen <math>x</math> gebunden. Offenbar spielt der Umstand, ob eine Typvariable im Kontext frei oder gebunden auftritt, eine bedeutsame Rolle für einen Typ im Rahmen einer Typung, daher wird <math>\mathrm{frei}(\ \Gamma\ )</math>
im Kasten präzisiert.

=== Anmerkungen zur Ausdrucksstärke ===
Da die Syntax des Ausdrucks einem mit dem [[Lambda-Kalkül]] unvertrauten Leser bei weitem zu ausdrucksschwach erscheinen mag und da die Beispiele dieses Vorurteil eher stützen werden, ist vielleicht der Hinweis hilfreich, dass sich HM nicht auf Spielzeugsprachen bezieht. Ein wesentliches Ergebnis der Forschung im Bereich der [[Berechenbarkeit]] ist, dass obige Ausdruckssyntax (ohne die let-Klausel) stark genug ist, jede berechenbare Funktion zu beschreiben. Darüber hinaus können alle weiteren Konstruktionen in Programmiersprachen relativ direkt syntaktisch in Ausdrücke des Lambda-Kalküls überführt werden. Darum werden diese einfachen Ausdrücke als Modell für Programmiersprachen verwendet. Ein Verfahren, das gut auf das Lambda-Kalkül anwendbar ist, kann leicht auf alle oder wenigstens viele andere syntaktische Konstruktionen einer speziellen Programmiersprache mittels der eben erwähnten Transformationen übertragen werden.

Zum Beispiel kann die zusätzliche Ausdrucksvariante <math>\textbf{let}\ x = e_1\ \textbf{in}\ e_2</math> transformiert werden nach <math>(\lambda x.e_2)\ e_1</math>.
Sie ist der Ausdruckssyntax im HM nur zur Unterstützung der Generalisierung während der Typinferenz hinzugefügt worden und nicht weil es der Syntax an Berechnungsstärke fehlt. HM behandelt also die Inferenz von Typen in Programmen im Allgemeinen und die verschieden funktionalen Sprachen, die diese Methode verwenden, belegen, wie gut ein Ergebnis, das nur für die Syntax des Lambda-Kalküls formuliert ist, auf syntaktisch komplexe Sprachen erweitert werden kann.

Im Gegensatz zum Eindruck, dass die Ausdrücke zu ausdrucksschwach für praktische Anwendungen seien, sind sie tatsächlich zu ausdrucksstark, um (im Allgemeinen) überhaupt typisiert zu werden. Dies ist eine Konsequenz der [[Unentscheidbarkeit]] für inhaltliche Aussagen über Ausdrücke des Lambda-Kalküls. Entsprechend ist die Berechnung der Typung von Programmen i.&nbsp;Allg. ein hoffnungsloses Unterfangen. Abhängig von der Natur des Typsystems wird dieses u.&nbsp;U. entweder nicht terminieren oder anderweitig den Dienst verweigern.

HM gehört zur letzteren Gruppe von Typsystemen. Ein Kollaps des Sortenapparats erscheint hier als eher subtile Situation, in der nur noch ein und derselbe Typ für die interessierenden Ausdrücke ermittelt wird. Dies ist kein Fehler im HM, sondern ein dem Problem der Typisierung selbst innewohnende Eigenschaft, die leicht in jeder stark getypten Sprache erzeugt werden kann. Hierzu kodiert man einen Auswerter (d.&nbsp;h. die [[Universelle Turingmaschine|universelle Funktion]]) für die „zu einfachen“ Ausdrücke. Man erhält damit einen einzelnen konkreten Typ, der den [[Datentyp#Universeller Datentyp|universellen Datentyp]] repräsentiert, wie er in typlosen Sprachen auftritt. Der Sortenapparat der Gastsprache ist dann kollabiert und kann die verschiedenen Typen von Werten nicht mehr unterscheiden, die der Auswertung übergeben oder von dieser erhalten werden. In diesem Zusammenhang ermittelt oder überprüft der Sortenapparat immer noch Typen, aber immer denselben, gerade als wäre das Typsystem gar nicht mehr vorhanden.

== Ordnung polymorpher Typen ==
Während die Gleichheit von Monotypen rein syntaktisch ist, haben Polytypen eine reichere Beziehung zu anderen Sorten, die durch eine Spezialisierungsrelation <math>\sqsubseteq</math> ausgedrückt wird, wobei <math>\sigma \sqsubseteq \sigma'</math> bedeutet, dass <math>\sigma'</math> spezieller ist als <math>\sigma</math>.

Wird eine polymorphe Funktion auf einen Wert angewendet, dann muss sie ihre Form an den speziellen Typ dieses Wertes anpassen. Während dieser Anpassung ändert sie mithin auch ihren Typ, um zu dem des Parameters zu passen. Wird beispielsweise die identische Funktion mit dem Typ
<math>\forall\alpha.\alpha\rightarrow\alpha</math> auf eine Zahl mit dem Typ <math>int</math> angewendet, dann können diese zunächst nicht zusammenwirken, da alle Typen verschieden sind und nicht passen. Was in dieser Lage benötigt wird, ist eine Funktion vom Typ <math>int\rightarrow int</math>. Hierzu wird die polymorphe Identität im Rahmen der Anwendung in eine monomorphe Version ihrer selbst verwandelt. In Begriffen der Spezialisierung ausgedrückt, kann man dies als
<math>\forall\alpha.\alpha\rightarrow\alpha \sqsubseteq\ int\rightarrow int</math> schreiben.

Nun ist die Formwandlung polymorpher Werte nicht völlig beliebig, sondern vielmehr durch den ursprünglichen Polytyp begrenzt. Dem Vorgang in diesem Beispiel folgend kann man die Spezialisierungsregel so umschreiben, dass ein polymorpher Typ <math>\forall\alpha.\tau</math> durch konsistente Ersetzung jedes Auftretens von
<math>\alpha</math> in <math>\tau</math> spezialisiert wird, wonach die Quantifizierung entfällt. Während diese Regel gut für alle Monotypen als Einsetzung funktioniert, schlägt sie fehl, wenn ein Polytyp als Ersetzung auftritt. Versucht man dies z.&nbsp;B. mit <math>\forall\beta.\beta</math>, dann erhält man einen unsyntaktischen Typ <math>\forall\beta.\beta\rightarrow\forall\beta.\beta</math>. Aber nicht nur das. Selbst wenn eine geschachtelte Quantifizierung in der Syntax zulässig wäre, würde das Ergebnis dieser Ersetzung die Eigenschaft des ursprünglichen Typs in dem Parameter und Resultat der Funktion denselben Typ haben, nicht mehr erhalten, da nun beide Untertypen unabhängig voneinander geworden sind und jeder eine Spezialisierung mit verschiedenen Typen erlauben würde, so z.&nbsp;B. <math>string\rightarrow Set\ int</math>, was kaum die richtige Aufgabe für eine identische Funktion wäre.

Die syntaktische Einschränkung der Quantifizierung auf die oberste Ebene verhindert diese unerwünschte Generalisierung während der Spezialisierung. Anstelle von
<math>\forall\beta.\beta\rightarrow\forall\beta.\beta</math> muss in diesem Fall der speziellere Typ <math>\forall\beta.\beta\rightarrow\beta</math> verwendet werden.

Man kann die eben erfolgte Spezialisierung durch eine weitere mit dem Typ <math>\forall\alpha.\alpha</math> wieder aufheben. In Bezeichnungen der Relation erhält man zusammenfassend
<math>\forall\alpha.\alpha\rightarrow\alpha \sqsubseteq \forall\beta.\beta\rightarrow\beta \sqsubseteq\forall\alpha.\alpha\rightarrow\alpha</math>,
was bedeutet, dass syntaktische verschiedene Polytypen gleich bzgl. der Umbenennung ihrer quantifizierten Variablen sind.

{| class="float-right wikitable infobox"
|align=center style="background:#e0e0ff"|'''Spezialisierungsregel'''
|-
| <math>\displaystyle\frac{\tau' = \left[\alpha_i := \tau_i\right] \tau \quad \beta_i \not\in \textrm{frei}(\forall \alpha_1...\forall\alpha_n . \tau)}{\forall \alpha_1...\forall\alpha_n . \tau \sqsubseteq \forall \beta_1...\forall\beta_m . \tau'}</math>
|}

Konzentriert man sich nun nur auf die Frage, ob ein Typ spezieller als ein anderer ist, und mehr, wofür ein speziellerer Typ verwendet wird, dann kann man die Spezialisierung wie im nebenstehenden Kasten zusammenfassen. Im Uhrzeigersinn umschrieben, wird ein Typ <math>\forall\alpha_1\dots\forall\alpha_n.\tau</math> spezialisiert, indem man jede der quantifizierten Variablen <math>\alpha_i</math> konsistent durch einen beliebigen Monotyp <math>\tau_i</math> ersetzt, so dass man insgesamt einen Monotyp <math>\tau'</math> erhält. Abschließend können Typvariablen, die im ursprünglichen Typ nicht frei auftraten, optional quantifiziert werden.

Die Spezialisierungsregel trägt also Sorge, dass keine freie Variable, d.&nbsp;h. Monotyp im ursprünglichen Typ, ungewollt durch einen Quantor gebunden wird. Ursprünglich quantifizierte Variablen können aber beliebig (konsistent) ersetzt werden, auch durch Typen, die neue quantifizierte oder unquantifizierte Variablen einführen.

Beginnend mit dem Polytyp <math>\forall\alpha.\alpha</math> kann eine Spezialisierung den Körper entweder durch eine andere quantisierte Variable ersetzen, letztlich eine Umbenennung, oder durch eine Typkonstante (einschließlich des Funktionstyps), die Parameter haben kann oder nicht, jede gefüllt mit einem Monotyp oder einer quantifizierten Typvariablen. Sobald eine quantifizierte Variable durch eine Typanwendung ersetzt worden ist, kann diese nicht mehr durch eine weitere Spezialisierung wieder aufgehoben werden, wie es bei der Ersetzung durch eine quantifizierte Variable möglich war. Typanwendungen sind also da, um zu bleiben. Nur wenn diese eine weitere quantifizierte Typvariable enthalten, kann die Spezialisierung durch deren weitere Ersetzung fortgeführt werden.

Die Spezialisierung führt also keine weiteren Gleichheiten auf Polytypen außer der bereits bekannten Umbenennung ein. Polytypen sind bis auf die Umbenennung ihrer gebundenen Variablen syntaktisch gleich. Die Gleichheit von Typen ist eine reflexive, antisymmetrische und transitive Relation und die verbleibende Spezialisierung von Polytypen ist transitiv. Damit ist die Relation <math>\sqsubseteq</math> eine [[Partielle Ordnung|Halbordnung]].

== Die Deduktionsmaschinerie ==
{| class="float-right wikitable infobox"
|align=center style="background:#e0e0ff"|'''Die Syntax der Regeln'''
|-
| <math>
\begin{array}{lrl}
  \mathrm{Pr\ddot{a}dikat}  & =      &\sigma\sqsubseteq\sigma\\
                    & \vert\ &\alpha\not\in \mathrm{frei}(\Gamma)\\
                    & \vert\ &x:\alpha\in \Gamma\\
\\
  \text{Urteil}     & =      &\text{Typung}\\
  \mathrm{Pr\ddot{a}misse}  & =      &\text{Urteil}\ \vert\ \mathrm{Pr\ddot{a}dikat}\\
  \text{Schluss}    & =      &\text{Urteil}\\
\\
  \text{Regel}      & =      &\displaystyle\frac{\mathrm{Pr\ddot{a}misse}\ \dots}{\textrm{Schluss}}\quad [\mathtt{Name}]
\end{array}
</math>
|}

Die Syntax von HM wird durch die Syntax der [[Inferenzregel]]n fortgeführt, die den Körper des [[Formales System|formalen Systems]] bilden, indem sie die Typungen als [[Urteil (Logik)|Urteile]] verwenden. Die Regeln definieren, aus welchen Voraussetzungen man welche Schlüsse ziehen kann. Zusätzlich zu den Urteilen können einige weiter oben eingeführte Randbedingungen als Prämissen verwendet werden.

Ein Beweis mittels der Regeln ist eine Sequenz von Urteilen, so dass alle Prämissen vor den Schlüssen aufgelistet werden. Siehe die folgenden Beispiele 2,3 für ein mögliches Format der Beweise. Von links nach rechts zeigt jede Zeile den Schluss, den <math>[\mathtt{Namen}]</math> der angewandten Regel und die Prämissen, entweder durch Verweis auf eine vorangehende Zeile, wenn die Prämisse ein Urteil ist, oder durch explizite Angabe des Prädikats.

== Die Typungsregeln ==
{| class="float-right wikitable infobox"
|align=center style="background:#e0e0ff"|'''Deklaratives Regelsystem'''
|-
| <math>
\begin{array}{cl}
 \displaystyle\frac{x:\sigma \in \Gamma}{\Gamma \vdash x:\sigma}&[\mathtt{Var}]\\ \\
 \displaystyle\frac{\Gamma \vdash e_0:\tau \rightarrow \tau' \quad\quad \Gamma \vdash e_1 : \tau }{\Gamma \vdash e_0\ e_1 : \tau'}&[\mathtt{App}]\\ \\
 \displaystyle\frac{\Gamma,\;x:\tau\vdash e:\tau'}{\Gamma \vdash \lambda\ x\ .\ e : \tau \rightarrow \tau'}&[\mathtt{Abs}]\\ \\
 \displaystyle\frac{\Gamma \vdash e_0:\sigma \quad\quad \Gamma,\,x:\sigma \vdash e_1:\tau}{\Gamma \vdash \mathtt{let}\ x = e_0\ \mathtt{in}\ e_1 : \tau} &[\mathtt{Let}]\\ \\ \\
 \displaystyle\frac{\Gamma \vdash e:\sigma' \quad \sigma' \sqsubseteq \sigma}{\Gamma \vdash e:\sigma}&[\mathtt{Inst}]\\ \\
 \displaystyle\frac{\Gamma \vdash e:\sigma \quad \alpha \notin \text{frei}(\Gamma)}{\Gamma \vdash e:\forall\ \alpha\ .\ \sigma}&[\mathtt{Gen}]\\ \\
 \end{array}</math>
|}

Der seitliche Kasten zeigt die Deduktionsregel des HM-Typsystems. Man kann sie grob in zwei Gruppen einteilen:

Die ersten vier Regeln <math>[\mathtt{Var}]</math>, <math>[\mathtt{App}]</math>, <math>[\mathtt{Abs}]</math> und <math>[\mathtt{Let}]</math> sind um die Syntax zentriert und geben je eine Regel für jede der Ausdrucksformen an. Ihre Bedeutung ist schon auf den ersten Blick recht offensichtlich, da sie jeden Ausdruck aufteilen, die Beweise der Teilausdrücke heranziehen und die Einzeltypen in den Prämissen zum Typ im Schluss kombinieren.

Die zweite Gruppe wird durch die verbleibenden Regeln <math>[\mathtt{Inst}]</math> and <math>[\mathtt{Gen}]</math> gebildet, die die Spezialisierung und Generalisierung von Typen behandeln. Während die  <math>[\mathtt{Inst}]</math> Regel inhaltlich im Abschnitt über die [[#Ordnung polymorpher Typen|Spezialisierung]] bereits beschrieben wurde, vervollständigt die Regel <math>[\mathtt{Gen}]</math> diese durch die umgekehrter Richtung. Sie erlaubt eine Generalisierung, d.&nbsp;h. eine Quantifizierung einer nicht im Kontext gebundenen Monotypvariablen. Die Notwendigkeit für die Einschränkung <math>\alpha \not\in \mathrm{frei}(\ \Gamma\ )</math> wurde im Abschnitt über die [[#Freie Typvariablen|freien Typvariablen]] eingeführt.

Die folgenden beiden Beispiele exerzieren das Regelsystem in Aktion.

'''Beispiel 2''': Ein Beweis für <math>\Gamma \vdash id(n):int</math> mit <math>\Gamma = id:\forall \alpha . \alpha\rightarrow\alpha,\ n:int</math> kann wie folgt geschrieben werden:

<math>\begin{array}{llll}
1:&\Gamma \vdash id : \forall\alpha.\alpha \rightarrow \alpha  &[\mathtt{Var}]& (id : \forall\alpha.\alpha \rightarrow \alpha \in \Gamma) \\
2:&\Gamma \vdash id : int \rightarrow int & [\mathtt{Inst}]&(1),\ (\forall\alpha.\alpha \rightarrow \alpha \sqsubseteq int\rightarrow int)\\
3:&\Gamma \vdash n : int&[\mathtt{Var}]&(n : int \in \Gamma)\\
4:&\Gamma \vdash id(n) : int&[\mathtt{App}]& (2),\ (3)\\
\end{array}
</math>

'''Beispiel 3''': Um die Generalisierung zu demonstrieren, wird <math>\vdash\ \textbf{let}\, id = \lambda x . x\ \textbf{in}\ id\, :\, \forall\alpha.\alpha\rightarrow\alpha</math> gezeigt:

<math>
\begin{array}{llll}
1: & x:\alpha \vdash x : \alpha & [\mathtt{Var}] & (x:\alpha \in \left\{x:\alpha\right\})\\
2: & \vdash \lambda x.x : \alpha\rightarrow\alpha & [\mathtt{Abs}] & (1)\\
3: & \vdash \lambda x.x : \forall \alpha.\alpha\rightarrow\alpha & [\mathtt{Gen}] & (2),\ (\alpha \not\in \mathrm{frei}(\epsilon))\\
4: & id:\lambda\alpha.\alpha\rightarrow\alpha \vdash id : \lambda\alpha.\alpha\rightarrow\alpha & [\mathtt{Var}] & (id:\lambda\alpha.\alpha\rightarrow\alpha \in \left\{id : \lambda\alpha.\alpha\rightarrow\alpha\right\})\\
5: & \vdash \textbf{let}\, id = \lambda x . x\ \textbf{in}\  id\, :\,\forall\alpha.\alpha\rightarrow\alpha  & [\mathtt{Let}] & (3),\ (4)\\
\end{array}
</math>

=== Haupttyp ===
Wie in der [[#Einleitung|Einleitung]] erwähnt, erlauben die Regeln verschiedene Typen für ein und denselben Ausdruck zu erschließen. Siehe Beispiel 2, Schritte 1,2 und Beispiel 3, Schritte 2,3 für drei verschiedene Typungen desselben Ausdrucks. Offenbar sind die verschiedenen Ergebnisse nicht völlig unabhängig, sondern durch die [[#Ordnung polymorpher Typen|Typordnung]] verbunden. Es ist eine wesentliche Eigenschaft des Regelsystems und der Typordnung, dass, wenn mehr als ein Typ für einen Ausdruck erschlossen werden kann, sich unter diesen Typen (modulo Gleichheit) ein eindeutig bestimmter, allgemeinster Typ in dem Sinne befindet, dass alle anderen Spezialisierungen von ihm sind. Während ein Regelsystem es zulassen muss, spezialisierte Typen herzuleiten, sollte ein Typinfernzalgorithmus den allgemeinsten oder Haupttyp als Ergebnis liefern.

=== Let-Polymorphismus ===
Nicht unmittelbar ersichtlich kodiert die Regelmenge eine Vorschrift, unter welchen Umständen ein Typ generalisiert werden darf und wann nicht. Dies geschieht durch eine leichte Variation im Gebrauch von Mono- und Polytypen in den Regeln <math>[\mathtt{Abs}]</math> und <math>[\mathtt{Let}]</math>.

In der Regel <math>[\mathtt{Abs}]</math> wird die Wertvariable des Parameters der Funktion <math>\lambda x.e</math> dem Kontext als ein monomorpher Typ durch die Prämisse <math>\Gamma,\ x:\tau \vdash e:\tau'</math> hinzugefügt, während in der Regel <math>[\mathtt{Let}]</math> die Variable die Umgebung in polymorpher Form <math>\Gamma,\ x:\sigma \vdash e_1:\tau'</math> betritt. Obwohl in beiden Fällen die Anwesenheit von x im Kontext den Gebrauch der Generalisierungsregel für jede Monotypvariable in der Zuordnung verhindert, erzwingt diese Vorschrift, dass ein Parameter x in einem <math>\lambda</math>-Ausdruck monomorph bleibt, während in einem let-Ausdruck die Typvariablen bereits polymorph eingeführt werden können, was Spezialisierungen ermöglicht.

Als Konsequenz dieses Reglements kann ''kein'' Typ für <math>\lambda f.(f\, \textrm{true}, f\, \textrm{0})</math> erschlossen werden, da sich der Parameter <math>f</math> in monomorpher Position befindet, während <math>\textbf{let}\ f = \lambda x . x\, \textbf{in}\, (f\, \textrm{true}, f\, \textrm{0})</math> den
Typ <math>(bool, int)</math> darum ergibt, weil <math>f</math> in einem let-Ausdruck eingeführt und darum polymorph behandelt wird. Beachte, dass dieses Verhalten sich in starkem Gegensatz zu üblichen Definition <math>\textbf{let}\ x = e_1\ \textbf{in}\ e_2\ ::= (\lambda\ x.e_2)\ e_1</math> befindet, was der Grund dafür ist, die let-Variante überhaupt in die Syntax des Ausdrucks aufzunehmen. Diese Unterscheidung wird let-[[Polymorphie (Programmierung)|Polymorphismus]] genannt und ist dem HM eigentümlich.

== Übergang zum Algorithmus ==
Da nun das Deduktionssystem des HMs zur Hand ist, könnte man einen Algorithmus vorstellen diesen gegen die Regel überprüfen.
Alternativ kann man ihn möglicherweise durch einen genaueren Blick darauf, wie die Regeln zusammenwirken und die Beweise
geformt sind, auch herleiten. Dieser Weg wird nun im verbleibenden Rest dieses Artikels durch eine Fokussierung auf die
möglichen Entscheidungen während des Beweisens einer Typung beschritten.

=== Freiheitsgrade bei der Regelauswahl ===
Isoliert man in einem Beweise die Stellen, an denen überhaupt keine Auswahl möglich ist, dann erhält man die um die Ausdruckssyntax zentrierte erste Gruppe von Regeln, die gleichsam das Gerüst des Beweises bestimmt, da jede der Schlussregeln genau einer Regel der Syntax entspricht, während zwischen den Prämissen und Schlüssen dieser festen Regelanwendungen verbindende Ketten von <math>[\mathtt{Inst}]</math> and <math>[\mathtt{Gen}]</math> auftreten können. Alle Beweise müssen die so skizzierte Form haben.

Da die einzige Möglichkeit in einem Beweis im Hinblick auf die Regelauswahl diese <math>[\mathtt{Inst}]</math> und <math>[\mathtt{Gen}]</math> Ketten sind, legt die Gestalt der Beweise die Frage nahe, ob man präzisieren kann
wo diese Ketten benötigt werden. Dies ist in der Tat möglich und führt auf eine Variante des Regelsystems ''ohne'' diese beiden Regeln.

=== Syntaxgesteuertes Regelsystem ===
{| class="float-right wikitable infobox"
|align=center style="background:#e0e0ff"|'''Syntaktisches Regelsystem'''
|-
| <math>
\begin{array}{cl}
\displaystyle\frac{x:\sigma \in \Gamma \quad \sigma \sqsubseteq \tau}{\Gamma \vdash x:\tau}&[\mathtt{Var}]\\ \\
\displaystyle\frac{\Gamma \vdash e_0:\tau \rightarrow \tau' \quad\quad \Gamma \vdash e_1 : \tau }{\Gamma \vdash e_0\ e_1 : \tau'}&[\mathtt{App}]\\ \\
\displaystyle\frac{\Gamma,\;x:\tau\vdash e:\tau'}{\Gamma \vdash \lambda\ x\ .\ e : \tau \rightarrow \tau'}&[\mathtt{Abs}]\\ \\
\displaystyle\frac{\Gamma \vdash e_0:\tau \quad\quad \Gamma,\,x:\bar{\Gamma}(\tau) \vdash e_1:\tau'}{\Gamma \vdash \mathtt{let}\ x = e_0\ \mathtt{in}\ e_1 :  \tau'}&[\mathtt{Let}]
\end{array}
</math>
|-
|align=center style="background:#e0e0ff"|'''Generalisierung'''
|-
| <math>
\bar{\Gamma}(\tau) = \forall\ \hat{\alpha}\ .\ \tau \quad\quad \hat{\alpha} = \textrm{frei}(\tau) - \textrm{frei}(\Gamma)
</math>
|}

Eine zeitgenössische Behandlung des HM verwendet ein rein syntaxgesteuertes Regelsystem nach Clement<ref>Clement, (1987). The Natural Dynamic Semantics of Mini-Standard ML. TAPSOFT'87, Vol 2. LNCS, Vol. 250, pp 67-81</ref> als Zwischenschritt.
In diesem System ist die Spezialisierung direkt hinter der ursprünglichen <math>[\mathtt{Var}]</math> Regel platziert und nun in diese eingemischt, während die Generalisierung mit in die <math>[\mathtt{Let}]</math> Regel aufgenommen wurde. Hierbei ist die Generalisierung zudem durch die Einführung der Funktion <math>\bar{\Gamma}(\tau)</math> so bestimmt, dass sie immer den allgemeinsten Typ erzeugt, indem sie alle nicht in <math>\Gamma</math> gebundenen Monotypvariablen quantifiziert.

Um zu überprüfen, dass dieses neue Regelsystem <math>\vdash_S</math> zum Original <math>\vdash_D</math> äquivalent ist, hat man zu zeigen, dass <math>\Gamma \vdash_D\ e:\sigma \Leftrightarrow \Gamma \vdash_S\ e:\sigma</math>, was in zwei Teilbeweise zerfällt:
* <math>\Gamma \vdash_D\ e:\sigma \Leftarrow \Gamma \vdash_S\ e:\sigma</math> ([[Korrektheit (Logik)|Korrektheit]])
* <math>\Gamma \vdash_D\ e:\sigma \Rightarrow \Gamma \vdash_S\ e:\sigma</math> ([[Vollständigkeit (Logik)|Vollständigkeit]])

Während man die Korrektheit durch Zerlegung der Regeln <math>[\mathtt{Let}]</math> and <math>[\mathtt{Var}]</math> von
<math>\vdash_S</math> zu Beweisen in <math>\vdash_D</math> sehen kann, ist ebenso erkennbar, dass <math>\vdash_S</math>
unvollständig ist, da man z.&nbsp;B. nicht zeigen kann, dass <math>\vdash_S\ \lambda\ x.x:\forall\alpha.\alpha\rightarrow\alpha</math>gilt,
sondern bestenfalls nur <math>\vdash_S\ \lambda\ x.x:\alpha\rightarrow\alpha</math>. Allerdings ist eine nur leicht schwächere
Version der Vollständigkeit nachweisbar<ref name=x>Jeff Vaughan, {{Webarchiv | url=http://www.cs.ucla.edu/~jeff/docs/hmproof.pdf | wayback=20120324105848 | text=A proof of correctness for the Hindley-Milner type inference algorithm}} (PDF, 152 KB)</ref>, nämlich:
* <math>\Gamma \vdash_D\ e:\sigma \Rightarrow \Gamma \vdash_S\ e:\tau \wedge \bar{\Gamma}(\tau)\sqsubseteq\sigma</math>

was besagt, dass man den Haupttyp für einen Ausdruck in <math>\vdash_S</math> herleiten kann, wenn man erlaubt, den Beweis am Ende zu generalisieren.

Beachte, dass <math>\vdash_S</math> im Vergleich zu <math>\vdash_D</math> nur noch Monotypen in den Urteilen seiner Regeln enthält.

=== Freiheitsgrade bei der Regelinstanzierung ===
Bei gegebenem Ausdruck ist man innerhalb der Regeln selber frei die Instanzen
für alle (Regel-)Variablen zu wählen, die nicht bereits durch die Ausdrücke
festgelegt sind. Dies sind die Instanzen für die Typvariablen in den Regeln.
Arbeitet man darauf hin, den Haupttyp zu zeigen, dann lässt sich die Wahl auf
das Aussuchen geeigneter Typen für <math>\tau</math> in <math>[\mathtt{Var}]</math>
und <math>[\mathtt{Abs}]</math> einschränken. Die Entscheidung für eine angemessene
Auswahl kann nicht lokal erfolgen, aber deren Qualität wird in den Prämissen von
<math>[\mathtt{App}]</math> erkennbar, der einzigen Regel, in der zwei unterschiedliche Typen, nämlich der des formalen und der des aktuellen Parameters, zu einem zusammenkommen müssen.

Darum würde eine allgemeine Strategie, um einen Beweis zu finden, darin bestehen,
die allgemeinste Annahme (<math>\alpha \not\in \mathrm{frei}(\Gamma)</math>) für <math>\tau</math>
zu machen und diese sowie die in <math>[\mathtt{Abs}]</math> zu treffende Wahl zu
verfeinern, bis alle durch die <math>[\mathtt{App}]</math> Regeln geforderten
Randbedingungen endlich erfüllt sind. Glücklicherweise sind hierfür weder Versuch und
Irrtum noch irgendwelche Iterationen erforderlich, da eine effektive Methode zur Berechnung
aller notwendigen Entscheidungen bekannt ist, die [[Unifikation (Logik)|Unifikation]] nach [[John Alan Robinson|Robinson]]
in Verbindung mit dem sogenannten [[Union-Find-Struktur|Union-Find]]-Algorithmus.

Um das Union-Find-Verfahren kurz zusammenzufassen, erlaubt es bei gegebener Menge aller Typen in einem
Beweis, diese mittels der Prozedur <math>\mathtt{union}</math> in [[Äquivalenzklasse]]n
zu teilen und mittels der Prozedur <math>\mathtt{find}</math> einen [[Repräsentant (Mathematik)|Repräsentanten]]
zu bestimmen. Das Wort [[Prozedur (Programmierung)|Prozedur]] im Sinne von [[Wirkung (Informatik)|Nebenwirkung]] betonend, wird das Reich der
Logik hier verlassen, um einen effektiven Algorithmus vorzubereiten. Der Repräsentant von <math>\mathtt{union}(a,b)</math>
ist hierbei so bestimmt, dass, falls sowohl <math>a</math> und auch <math>b</math> Typvariablen sind, der Repräsentant
beliebig eine von ihnen ist, während bei einer Vereinigung von einer Variablen und einer Anwendung letztere zum Repräsentanten
gewählt wird. Hat man eine solche Implementierung des Union-Find zur Hand, dann kann man die Unifikation zweier
Monotypen wie folgt formulieren:

 unify(ta,tb):
   ta = find(ta)
   tb = find(tb)
   '''wenn''' ta,tb beide Anwendungen der Form D p1..pn mit identischen D,n sind '''dann'''
     unify(ta[i],tb[i]) für jeden korrespondierenden i-ten Parameter
   '''sonst'''
   '''wenn''' wenigstens einer von ta,tb eine Typvariable ist '''dann'''
     union(ta,tb)
   '''sonst'''
     fehler 'Die Typen ta,tb passen nicht zusammen.'

== Algorithmus W ==
{| class="float-right wikitable infobox"
|align=center style="background:#e0e0ff"|'''Algorithmus W'''
|-
| <math>
\begin{array}{cl}
\displaystyle\frac{x:\sigma \in \Gamma \quad \tau = \mathit{inst}(\sigma)}{\Gamma \vdash x:\tau}&[\mathtt{Var}]\\ \\
\displaystyle\frac{\Gamma \vdash e_0:\tau_0 \quad \Gamma \vdash e_1 : \tau_1 \quad \tau'= \mathit{newvar} \quad \mathit{unify}(\tau_0,\ \tau_1 \rightarrow \tau') }{\Gamma \vdash e_0\ e_1 : \tau'}&[\mathtt{App}]\\ \\
\displaystyle\frac{\tau = \mathit{newvar} \quad \Gamma,\;x:\tau\vdash e:\tau'}{\Gamma \vdash \lambda\ x\ .\ e : \tau \rightarrow \tau'}&[\mathtt{Abs}]\\ \\
\displaystyle\frac{\Gamma \vdash e_0:\tau \quad\quad \Gamma,\,x:\bar{\Gamma}(\tau) \vdash e_1:\tau'}{\Gamma \vdash \mathtt{let}\ x = e_0\ \mathtt{in}\ e_1 :  \tau'}&[\mathtt{Let}]
\end{array}
</math>
|}

Die Präsentation des Algorithmus W wie er im Kasten an der Seite gezeigt wird, weicht nicht nur signifikant vom Original<ref name="Damas" /> ab, sondern stellt auch einen erheblichen Fehlgebrauch der Notation logischer Regeln dar, da er Nebeneffekte mit einschließt. Dies ist hier dadurch legitimiert, um einen direkten Vergleich mit <math>\vdash_S</math> zu ermöglichen und zugleich eine effektive Implementierung anzugeben.
Die Regeln spezifizieren nun eine Prozedur mit Parametern  <math>\Gamma, e</math> und Resultat <math>\tau</math> im Schluss, wobei die Ausführung der Prämissen von links nach rechts verläuft. Alternativ zu einer Prozedur können die Regeln als eine [[Attributgrammatik|Attributierung]] (mit denselben Anmerkungen bzgl. der Nebeneffekte) angesehen werden.

Die Prozedur '<math>inst(\sigma)</math>' spezialisiert den Polytyp <math>\sigma</math>, indem sie den Term kopiert und die darin enthaltenen gebundenen Variablen konsistent durch (global) neue Monotypvariablen ersetzt. '<math>newvar</math>' erzeugt eine neue Monotypvariable. In ähnlicher Weise hat <math>\bar{\Gamma}(\tau)</math> eine Kopie des Typs herzustellen, in der (global) neue Typvariablen für die Quantifikation eingeführt werden, um ungewollte Bindungen zu vermeiden.

Insgesamt verfährt der Algorithmus nun, indem er immer die allgemeinst mögliche Auswahl triff und die Spezialisierung der Unifikation überlässt, die ihrerseits das allgemeinst mögliche Resultat erzeugt. Wie [[#Syntaxgesteuertes Regelsystem|oben]] angemerkt, ist das Ergebnis <math>\tau</math> am Ende noch einmal zu <math>\bar{\Gamma}(\tau)</math> zu generalisieren, um den Haupttyp für einen gegebenen Ausdruck zu erhalten.

Da die im Algorithmus verwendeten Prozeduren Kosten nahe <math>O(1)</math> haben, sind die Gesamtkosten des Verfahrens nahezu linear zur Größe des Ausdrucks, für den ein Typ zu inferieren ist. Es steht damit in starkem Kontrast zu vielen anderen Versuchen, ein Typinferenzverfahren herzustellen, die sich oft als [[NP-schwer]], wenn nicht [[Unentscheidbarkeit|unentscheidbar]] bzgl. Terminierung herausgestellt haben. Mithin hat HM denselben Durchsatz, den das beste voll informierte Typprüfungsverfahren haben kann. Typprüfung heißt hier, dass ein Algorithmus keinen Beweis zu finden hat, sondern diesen nur zu überprüfen braucht.

Die Effizienz ist aus zwei Gründen geringfügig niedriger. Zum ersten sind die Bindungen der Typvariablen im Kontext zu verwalten, um die Berechnung von <math>\bar{\Gamma}(\tau)</math> zu erlauben. Ferner ist ein [[occurs check]] erforderlich, um die Entstehung rekursiver Typen während Unifikation
zu verhindern. Ein Beispiel für einen solchen Fall ist <math>\lambda\ x.(x\ x)</math>, für das kein Typ mit dem HM hergeleitet werden kann. Da in der Praxis die Typen nur kleine Terme sind und sich zudem nicht zu expandierenden Strukturen aufbauen, kann man sie in der Komplexitätsanalyse als kleiner als eine bestimmte Konstante betrachten, so dass die O(1)-Kosten gewahrt bleiben.

=== Der Algorithmus W im Original ===
In der Originalpublikation<ref name="Damas" /> wird der Algorithmus formaler in einem [[Substitution (Logik)|Substitutionsstil]] beschrieben statt durch Nebeneffekte wie in der Methode oben. In letzter Form kümmert sich der Nebeneffekte unsichtbar um alle Stellen, in denen Typvariablen verwendet werden. Explizite Verwendung der Substitution macht nicht nur den Algorithmus schwerer zu lesen, da die Nebeneffekte praktisch überall auftreten, sondern vermittelt auch den falschen Eindruck, dass die Methode teuer ist. Wird sie hingegen mit rein funktionalen Mitteln oder zum Zweck des Beweises der Äquivalenz zum Deduktionssystem implementiert, ist voll Explizitheit natürlich notwendig und die Originalformulierung eine notwendige Verfeinerung.

== Weitere Themen ==
=== Rekursive Definitionen ===
Eine zentrale Eigenschaft des Lambda-Kalküls ist, dass rekursive Definitionen nicht elementar sind, sondern mit Hilfe des [[Kombinatorische Logik#Fixpunktkombinator|Fixpunktkombinators]] ausgedrückt werden können. In der Originalpublikation<ref name="Damas" /> wird angemerkt, dass Rekursion mit dem Typ <math>fix:\forall\alpha.(\alpha\rightarrow\alpha)\rightarrow\alpha</math> dieses Kombinators realisiert werden kann. Eine mögliche rekursive Definition kann damit als <math>\mathtt{rec}\ v = e_1\ \mathtt{in}\ e_2\ ::=\mathtt{let}\ v = fix(\lambda v.e_1)\ \mathtt{in}\ e_2</math> formuliert werden.

Alternativ ist eine Erweiterung der Ausdruckssyntax und eine zusätzliche Typregel möglich mit:

<math>\displaystyle\frac{
\Gamma, \Gamma' \vdash e_1:\tau_1\quad\dots\quad\Gamma, \Gamma' \vdash e_n:\tau_n\quad\Gamma, \Gamma'' \vdash e:\tau
}{
\Gamma\ \vdash\ \mathtt{rec}\ v_1 = e_1\ \mathtt{and}\ \dots\ \mathtt{and}\ v_n = e_n\ \mathtt{in}\ e:\tau
}\quad[\mathtt{Rec}]</math>

mit
* <math>\Gamma' = v_1:\tau_1,\ \dots,\ v_n:\tau_n</math>
* <math>\Gamma'' = v_1:\bar\Gamma(\ \tau_1\ ),\ \dots,\ v_n:\bar\Gamma(\ \tau_n\ )</math>

Hierin sind grundsätzlich <math>[\mathtt{Abs}]</math> und <math>[\mathtt{Let}]</math> zusammengemischt,
wobei die rekursiv definierten Variablen monomorph behandelt werden, wenn sie links vom <math>\mathtt{in}</math>
auftreten, aber polymorph rechts davon. Diese Formulierung fasst die Essenz des [[#Let-Polymorphismus|let-Polymorphismus]]
vielleicht am besten zusammen.

== Anmerkungen ==
<references group="note" />

== Einzelnachweise ==
<references />

[[Kategorie:Typentheorie]]
[[Kategorie:Theoretische Informatik]]
[[Kategorie:Compilerbau]]
[[Kategorie:Algorithmus]]