Typinferenz nach Hindley-Milner

Hindley-Milner (HM) ist ein Verfahren der Typinferenz mit parametrischem Polymorphismus für den Lambda-Kalkül. Es wurde erstmals von J. Roger Hindley beschrieben und später von Robin Milner wiederentdeckt. Luis Damas trug eine genaue formale Analyse und einen Beweis der Methode in seiner Doktorarbeit bei, weshalb das Verfahren auch als Damas-Milner 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 funktionalen Sprachen wie OCaml/Reason eingesetzt. Es wurde erstmals als Teil des Typsystems der Programmiersprache ML implementiert. Seitdem wurde HM auf verschiedene Weise erweitert, insbesondere durch beschränkte Typen, wie sie in Haskell verwendet werden.

Einleitung

Damas und Milner 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. 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 Deduktionssystems beschrieben. Wie jedes 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) 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

Ausdrücke

${\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}}$

Typen

${\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}}$

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üls, erweitert um einen let-Ausdruck.

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

Das Gesamt der Typen (Sorten) teilt sich in zwei Gruppen, die Mono- und Polytypen genannt werden.

Monotypen $\tau$, syntaktisch Terme, 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 $int$ oder $string$. Typen können parametrisch sein, wie z. B. $Map\ (Set\ string)\ int$. All diese Typen sind Beispiele von Anwendungen von Typfunktionen $D$, z. B. $\left\{int^{0},string^{0},Map^{2},Set^{1}\right\}\subset D$ in den vorangegangenen Beispielen, wobei die hochgestellte Ziffer die Zahl der Typparameter angibt. Während die Wahl von $D$ grundsätzlich beliebig ist, muss sie im Zusammenhang des HM wenigstens den bequemerweise infix geschriebenen Funktionstyp $\rightarrow ^{2}$ enthalten. Beispielsweise hat eine Funktion, die ganze Zahlen auf Zeichenketten abbildet, den Typ $int\rightarrow string$.

Vielleicht etwas irritierenderweise sind Typvariablen ebenfalls Monotypen. Eine allein stehende Typvariable $\alpha$ bezeichnet einen Typ, der genau so konkret ist wie etwa $int$ oder $\beta$ 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 $\alpha \rightarrow \alpha$ nur Werte des Typs $\alpha$ 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 $\forall \alpha .\alpha \rightarrow \alpha$ jeden Wert auf einen Wert gleichen Typs abbilden. Die identische Funktion ist ein Wert für diesen Typ. Als weiteres Beispiel ist $\forall \alpha .(Set\ \alpha )\rightarrow int$ 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. h. der Typ $\forall \alpha .\alpha \rightarrow \forall \alpha .\alpha$ beispielsweise ist durch die Syntax ausgeschlossen. Ferner sind Monotypen eine Teilmenge der Polytypen, so dass Typen insgesamt die allgemeine Form $\forall \alpha _{1}\dots \forall \alpha _{n}.\tau$ haben.

Freie Typvariablen

Freie Typvariablen

${\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}}$

In einem Typ $\forall \alpha _{1}\dots \forall \alpha _{n}.\tau$ ist das Symbol $\forall$ der die Typvariablen $\alpha _{i}$ im Monotyp $\tau$ bindende Quantor. Die Variablen $\alpha _{i}$ heißen quantifiziert. Jedes Auftreten einer quantifizierten Variablen in $\tau$ heißt gebunden und alle ungebundenen Typvariablen heißen frei. Wie im Lambda-Kalkül ist der Begriff der 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 ausgedrückt werden können. Genauso gibt es keine freien Variablen in 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. B. bedeutet der Haskell-Typ ${\texttt {a~->~a}}$ hier $\forall \alpha .\alpha \rightarrow \alpha$. Da Typen wie $\alpha \rightarrow \alpha$, 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. B. $\forall \beta .\beta \rightarrow \alpha$, d. h. eine Mischung von gebundenen und ungebundenen Typvariablen, enthalten und was bedeutet eine freie Typvariable darin?

Beispiel 1

${\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}}$

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

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

In diesem Beispiel wird die freie Monotypvariable $\alpha$ im Typ von $foo$ durch die Quantifikation im äußeren Geltungsbereich mit Bedeutung beladen, nämlich im Typ von $bar$. Dies heißt im Zusammenhang dieses Beispiels, dass dieselbe Typvariable $\alpha$ 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

Syntax

${\begin{array}{llrl}{\text{Kontext}}&\Gamma &=&\epsilon \ {\mathtt {(leer)}}\\&&\vert &\Gamma ,\ x:\sigma \\{\text{Typung}}&&=&\Gamma \vdash e:\sigma \\\\\end{array}}$

Freie Typvariablen

${\begin{array}{ll}{\text{frei}}(\ \Gamma \ )&=\ \bigcup \limits _{x:\sigma \in \Gamma }{\text{frei}}(\ \sigma \ )\end{array}}$

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 $x:\sigma$, Belegung (s. a. Belegung, Zuordnung, Zuweisung) genannt, die jeder Wertvariablen $x_{i}$ im Kontext einen Typ $\sigma _{i}$ zuordnet. Alle drei Teile zusammen ergeben eine Typung der Form $\Gamma \ \vdash \ e:\sigma$, die aussagt, dass unter der Annahme $\Gamma$ der Ausdruck $e$ den Typ $\sigma$ hat.

Da nun die vollständige Syntax zur Verfügung steht, kann schließlich eine sinnvolle Aussage über den Typ von $foo$ in Beispiel 1 gemacht werden, nämlich $x:\alpha \vdash \lambda \ y.x:\forall \beta .\beta \rightarrow \alpha$. Im Gegensatz zu den vorangehenden Formulierungen ist die Monotypvariable $\alpha$ nicht länger frei, d. h. bedeutungslos, sondern im Kontext als Typ der Wertvariablen $x$ 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 $\mathrm {frei} (\ \Gamma \ )$ 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 ${\textbf {let}}\ x=e_{1}\ {\textbf {in}}\ e_{2}$ transformiert werden nach $(\lambda x.e_{2})\ e_{1}$. 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. Allg. ein hoffnungsloses Unterfangen. Abhängig von der Natur des Typsystems wird dieses u. 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. h. die universelle Funktion) für die „zu einfachen“ Ausdrücke. Man erhält damit einen einzelnen konkreten Typ, der den 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 $\sqsubseteq$ ausgedrückt wird, wobei $\sigma \sqsubseteq \sigma '$ bedeutet, dass $\sigma '$ spezieller ist als $\sigma$.

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 $\forall \alpha .\alpha \rightarrow \alpha$ auf eine Zahl mit dem Typ $int$ 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 $int\rightarrow int$. 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 $\forall \alpha .\alpha \rightarrow \alpha \sqsubseteq \ int\rightarrow int$ 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 $\forall \alpha .\tau$ durch konsistente Ersetzung jedes Auftretens von $\alpha$ in $\tau$ 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. B. mit $\forall \beta .\beta$, dann erhält man einen unsyntaktischen Typ $\forall \beta .\beta \rightarrow \forall \beta .\beta$. 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. B. $string\rightarrow Set\ int$, 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 $\forall \beta .\beta \rightarrow \forall \beta .\beta$ muss in diesem Fall der speziellere Typ $\forall \beta .\beta \rightarrow \beta$ verwendet werden.

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

Spezialisierungsregel

$\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 '}}$

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 $\forall \alpha _{1}\dots \forall \alpha _{n}.\tau$ spezialisiert, indem man jede der quantifizierten Variablen $\alpha _{i}$ konsistent durch einen beliebigen Monotyp $\tau _{i}$ ersetzt, so dass man insgesamt einen Monotyp $\tau '$ 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. 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 $\forall \alpha .\alpha$ 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 $\sqsubseteq$ eine Halbordnung.

Die Deduktionsmaschinerie

Die Syntax der Regeln

${\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}}$

Die Syntax von HM wird durch die Syntax der Inferenzregeln fortgeführt, die den Körper des formalen Systems bilden, indem sie die Typungen als 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 $[{\mathtt {Namen}}]$ 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

Deklaratives Regelsystem

${\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}}$

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

Die ersten vier Regeln $[{\mathtt {Var}}]$, $[{\mathtt {App}}]$, $[{\mathtt {Abs}}]$ und $[{\mathtt {Let}}]$ 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 $[{\mathtt {Inst}}]$ and $[{\mathtt {Gen}}]$ gebildet, die die Spezialisierung und Generalisierung von Typen behandeln. Während die $[{\mathtt {Inst}}]$ Regel inhaltlich im Abschnitt über die Spezialisierung bereits beschrieben wurde, vervollständigt die Regel $[{\mathtt {Gen}}]$ diese durch die umgekehrter Richtung. Sie erlaubt eine Generalisierung, d. h. eine Quantifizierung einer nicht im Kontext gebundenen Monotypvariablen. Die Notwendigkeit für die Einschränkung $\alpha \not \in \mathrm {frei} (\ \Gamma \ )$ wurde im Abschnitt über die freien Typvariablen eingeführt.

Die folgenden beiden Beispiele exerzieren das Regelsystem in Aktion.

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

${\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}}$

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

${\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}}$

Haupttyp

Wie in der 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 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 $[{\mathtt {Abs}}]$ und $[{\mathtt {Let}}]$.

In der Regel $[{\mathtt {Abs}}]$ wird die Wertvariable des Parameters der Funktion $\lambda x.e$ dem Kontext als ein monomorpher Typ durch die Prämisse $\Gamma ,\ x:\tau \vdash e:\tau '$ hinzugefügt, während in der Regel $[{\mathtt {Let}}]$ die Variable die Umgebung in polymorpher Form $\Gamma ,\ x:\sigma \vdash e_{1}:\tau '$ 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 $\lambda$-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 $\lambda f.(f\,{\textrm {true}},f\,{\textrm {0}})$ erschlossen werden, da sich der Parameter $f$ in monomorpher Position befindet, während ${\textbf {let}}\ f=\lambda x.x\,{\textbf {in}}\,(f\,{\textrm {true}},f\,{\textrm {0}})$ den Typ $(bool,int)$ darum ergibt, weil $f$ in einem let-Ausdruck eingeführt und darum polymorph behandelt wird. Beachte, dass dieses Verhalten sich in starkem Gegensatz zu üblichen Definition ${\textbf {let}}\ x=e_{1}\ {\textbf {in}}\ e_{2}\ ::=(\lambda \ x.e_{2})\ e_{1}$ befindet, was der Grund dafür ist, die let-Variante überhaupt in die Syntax des Ausdrucks aufzunehmen. Diese Unterscheidung wird let-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 $[{\mathtt {Inst}}]$ and $[{\mathtt {Gen}}]$ 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 $[{\mathtt {Inst}}]$ und $[{\mathtt {Gen}}]$ 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

Syntaktisches Regelsystem

${\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}}$

Generalisierung

${\bar {\Gamma }}(\tau )=\forall \ {\hat {\alpha }}\ .\ \tau \quad \quad {\hat {\alpha }}={\textrm {frei}}(\tau )-{\textrm {frei}}(\Gamma )$

Eine zeitgenössische Behandlung des HM verwendet ein rein syntaxgesteuertes Regelsystem nach Clement als Zwischenschritt. In diesem System ist die Spezialisierung direkt hinter der ursprünglichen $[{\mathtt {Var}}]$ Regel platziert und nun in diese eingemischt, während die Generalisierung mit in die $[{\mathtt {Let}}]$ Regel aufgenommen wurde. Hierbei ist die Generalisierung zudem durch die Einführung der Funktion ${\bar {\Gamma }}(\tau )$ so bestimmt, dass sie immer den allgemeinsten Typ erzeugt, indem sie alle nicht in $\Gamma$ gebundenen Monotypvariablen quantifiziert.

Um zu überprüfen, dass dieses neue Regelsystem $\vdash _{S}$ zum Original $\vdash _{D}$ äquivalent ist, hat man zu zeigen, dass $\Gamma \vdash _{D}\ e:\sigma \Leftrightarrow \Gamma \vdash _{S}\ e:\sigma$, was in zwei Teilbeweise zerfällt:

• $\Gamma \vdash _{D}\ e:\sigma \Leftarrow \Gamma \vdash _{S}\ e:\sigma$ (Korrektheit)
• $\Gamma \vdash _{D}\ e:\sigma \Rightarrow \Gamma \vdash _{S}\ e:\sigma$ (Vollständigkeit)

Während man die Korrektheit durch Zerlegung der Regeln $[{\mathtt {Let}}]$ and $[{\mathtt {Var}}]$ von $\vdash _{S}$ zu Beweisen in $\vdash _{D}$ sehen kann, ist ebenso erkennbar, dass $\vdash _{S}$ unvollständig ist, da man z. B. nicht zeigen kann, dass $\vdash _{S}\ \lambda \ x.x:\forall \alpha .\alpha \rightarrow \alpha$gilt, sondern bestenfalls nur $\vdash _{S}\ \lambda \ x.x:\alpha \rightarrow \alpha$. Allerdings ist eine nur leicht schwächere Version der Vollständigkeit nachweisbar, nämlich:

• $\Gamma \vdash _{D}\ e:\sigma \Rightarrow \Gamma \vdash _{S}\ e:\tau \wedge {\bar {\Gamma }}(\tau )\sqsubseteq \sigma$

was besagt, dass man den Haupttyp für einen Ausdruck in $\vdash _{S}$ herleiten kann, wenn man erlaubt, den Beweis am Ende zu generalisieren.

Beachte, dass $\vdash _{S}$ im Vergleich zu $\vdash _{D}$ 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 $\tau$ in $[{\mathtt {Var}}]$ und $[{\mathtt {Abs}}]$ einschränken. Die Entscheidung für eine angemessene Auswahl kann nicht lokal erfolgen, aber deren Qualität wird in den Prämissen von $[{\mathtt {App}}]$ 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 ($\alpha \not \in \mathrm {frei} (\Gamma )$) für $\tau$ zu machen und diese sowie die in $[{\mathtt {Abs}}]$ zu treffende Wahl zu verfeinern, bis alle durch die $[{\mathtt {App}}]$ 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 nach Robinson in Verbindung mit dem sogenannten Union-Find-Algorithmus.

Um das Union-Find-Verfahren kurz zusammenzufassen, erlaubt es bei gegebener Menge aller Typen in einem Beweis, diese mittels der Prozedur ${\mathtt {union}}$ in Äquivalenzklassen zu teilen und mittels der Prozedur ${\mathtt {find}}$ einen Repräsentanten zu bestimmen. Das Wort Prozedur im Sinne von Nebenwirkung betonend, wird das Reich der Logik hier verlassen, um einen effektiven Algorithmus vorzubereiten. Der Repräsentant von ${\mathtt {union}}(a,b)$ ist hierbei so bestimmt, dass, falls sowohl $a$ und auch $b$ 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

Algorithmus W

${\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}}$

Die Präsentation des Algorithmus W wie er im Kasten an der Seite gezeigt wird, weicht nicht nur signifikant vom Original 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 $\vdash _{S}$ zu ermöglichen und zugleich eine effektive Implementierung anzugeben. Die Regeln spezifizieren nun eine Prozedur mit Parametern $\Gamma ,e$ und Resultat $\tau$ 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 Attributierung (mit denselben Anmerkungen bzgl. der Nebeneffekte) angesehen werden.

Die Prozedur '$inst(\sigma )$' spezialisiert den Polytyp $\sigma$, indem sie den Term kopiert und die darin enthaltenen gebundenen Variablen konsistent durch (global) neue Monotypvariablen ersetzt. '$newvar$' erzeugt eine neue Monotypvariable. In ähnlicher Weise hat ${\bar {\Gamma }}(\tau )$ 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 oben angemerkt, ist das Ergebnis $\tau$ am Ende noch einmal zu ${\bar {\Gamma }}(\tau )$ zu generalisieren, um den Haupttyp für einen gegebenen Ausdruck zu erhalten.

Da die im Algorithmus verwendeten Prozeduren Kosten nahe $O(1)$ 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 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 ${\bar {\Gamma }}(\tau )$ 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 $\lambda \ x.(x\ x)$, 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 wird der Algorithmus formaler in einem 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 Fixpunktkombinators ausgedrückt werden können. In der Originalpublikation wird angemerkt, dass Rekursion mit dem Typ $fix:\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha$ dieses Kombinators realisiert werden kann. Eine mögliche rekursive Definition kann damit als ${\mathtt {rec}}\ v=e_{1}\ {\mathtt {in}}\ e_{2}\ ::={\mathtt {let}}\ v=fix(\lambda v.e_{1})\ {\mathtt {in}}\ e_{2}$ formuliert werden.

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

$\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}}]$

mit

• $\Gamma '=v_{1}:\tau _{1},\ \dots ,\ v_{n}:\tau _{n}$
• $\Gamma ''=v_{1}:{\bar {\Gamma }}(\ \tau _{1}\ ),\ \dots ,\ v_{n}:{\bar {\Gamma }}(\ \tau _{n}\ )$

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