Typinferenz nach Hindley-Milner

Diese Baustelle befindet sich fälschlicherweise im Artikelnamensraum. Bitte verschiebe die Seite oder entferne den Baustein {{Baustelle}}.

Dieser Artikel ist im Entstehen und noch nicht Bestandteil der freien Enzyklopädie Wikipedia.

Solltest du über eine Suchmaschine darauf gestoßen sein, bedenke, dass der Text noch unvollständig sein und Fehler oder ungeprüfte Aussagen enthalten kann. Wenn du Fragen zum Thema hast, nimm Kontakt mit den Autoren auf.

Typinferenz nach Hindley-Milner

Hindley-Milner (HM) ist eine klassische Methode zu 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 Beiweis 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 Typen eines gegeben Quelle ohne Hinzunahme von Annotationen oder sonstigen Hinweisen bestimmen zu können. HM ist ein effezienter Algorithmus, der den der Typisierung nahezu in linearer Zeit bzgl. des Größe der Quelle ermitteln kann, womit es praktisch zum Typen großer Programme anwendbar ist. HM wird bevorzugt funktionalen Sprachen eingesetzt. Es wurde erstmals als Teil des Sortenapparts der Programmiersprache ML implementiert. Seit dem wurde HM in verschiedenster Weise erweitert, insbesondere durch beschränkte Typen, wie sie in Haskell verwendet werden.

Einleitung

Damas und Milner trennen in der Gliederung ihrer Orginal-Veröffentlichung zwei sehr verscheidene Aufgaben. Die eine, zu beschreiben, welche Typen ein Ausdruck haben kann, die andere, eine Algorithmus anzugeben, der tatsächlich einen Typen ermitteln kann.

Beide Aspekte getrennt von einander 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 zueinder passen wird mit Hilfe eines Deduktionssystems beschrieben. Wie jedes Beweissystem erlaubt es auf verschiedene Wegen zu einem Schluss zu gelangen, sowie, da ein und der Ausdruck begründbar verschiedene Typen haben kann, auch zu durchaus unterschiedlichen Schlüssen über einen Ausdruck zu kommen. Im Gegensatz dazu ist die Typinferenz-Methode selbst (Algorithm W) ein Schritt-für-Schritt auszuführendes Verfahren, dass keine Wahl lässt, was als nächstes zu tun sein. 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 &{\texttt {let}}\ x=e\ {\texttt {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 "Type", deren Form durch die Syntax präzisiert wird.

Die zu typenden Ausdrücke sind die des Lambda-Kalküls, erweitert um einen let-Ausdruck.

Mit dem Lambda-Kalkül nicht vertraute Leser mögen nicht nur über dessen Syntax verwundert sein, was sich aber schnell durch eine Übersetzung beheben lässt. 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 ${\texttt {function}}\,(x)\ {\texttt {return}}\ e\ {\texttt {end}}$ ausgeschrieben.

Das Gesamt der Typen (Sorten) teilt sich in zwei Gruppe, 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$ or $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 keine weiteren Informationen besitzt. Entsprechend bildet eine Funktionen mit dem Typ $\alpha \rightarrow \alpha$ nur Werte des Type $\alpha$ auf sich selbst ab und kann nur auf Werte dieses Typen 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. Beachte, dass Quantoren nur auf oberster Ebene auftreten dürfen, 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 Vorraussetzungen 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 sich 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}}$

Betrachte $foo$ in Beispiel 1, mit Typ-Annotationen in eckigen Klammern. Offensichtlich wird der Parameter $y$ im Körper nicht verwendet, wohl aber die im der äußeren Kontext von $foo$ gebundene Variable $x$. Als Konsequenz akzeptiert $foo$ jeden Wert als Argument, während sie einen Wert liefert, der ausserhalb 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 Typen von $bar$. Die 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 i. allg. ohne Kenntnis des Kontexts nicht aussagekräftig.

Kontext und Typung

Syntax

${\begin{array}{llrl}{\text{Kontext}}&\Gamma &=&\epsilon \ {\texttt {(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 zusammen zu bringen 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 man nun schließlich eine sinnvoll Aussage über den den Typ von $foo$ in Beispiel 1 machen, 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 $frei(\ \Gamma \ )$ im Kasten an der Seiten präzisiert.

Anmerkungen zur Ausdruckskraft

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 ein Hinweis hilfreich, dass HM sich 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.

Z.B. 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 Berechnungskraft 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, dass 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 der Natur des Typ-Systems, 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 innenwohnende 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, dass muss sie ihre Form an den speziellen Typen dieses Wertes anpassen. Während dieser Anpassung ändert sie mithin auch ihren Typen, 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 passt. 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 Polytypen 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 Quantifierung 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 Typen in dem Parameter und Resultat der Funktion denselben Typen 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 {free}}(\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 durch einem 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 ersetzten, letztlich eine Umbenennung, oder durch eine Typkonstante (einschließlich des Funktionstypen), die 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. Eine Typanwendungen sind also da um zu bleiben. Nur wenn diese eine weitere quantifiziere Typvariable enthalten kann kann die Spezialisierung durch deren weitere Ersetzung fortgeführt werden.

Die Spezialisierung führt also keine weiteren Gleichheiten auf Polytypen ausser 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 Ordnung.

Die Deduktionsmaschinerie

Die Syntax der Regeln

${\begin{array}{lrl}\mathrm {Pr{\ddot {a}}dikat} &=&\sigma \sqsubseteq \sigma \\&\vert \ &\alpha \not \in 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 [{\texttt {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 Vorraussetzungen 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 $[{\texttt {Namen}}]$ der angewandten Regel und die Prämissen, entweder durch Verweis auf eine vorangehende Zeile(-nnummer) 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 }}&[{\texttt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash e_{0}:\tau \rightarrow \tau '\quad \quad \Gamma \vdash e_{1}:\tau }{\Gamma \vdash e_{0}\ e_{1}:\tau '}}&[{\texttt {App}}]\\\\\displaystyle {\frac {\Gamma ,\;x:\tau \vdash e:\tau '}{\Gamma \vdash \lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\texttt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash e_{0}:\sigma \quad \quad \Gamma ,\,x:\sigma \vdash e_{1}:\tau }{\Gamma \vdash {\texttt {let}}\ x=e_{0}\ {\texttt {in}}\ e_{1}:\tau }}&[{\texttt {Let}}]\\\\\\\displaystyle {\frac {\Gamma \vdash e:\sigma '\quad \sigma '\sqsubseteq \sigma }{\Gamma \vdash e:\sigma }}&[{\texttt {Inst}}]\\\\\displaystyle {\frac {\Gamma \vdash e:\sigma \quad \alpha \notin {\text{frei}}(\Gamma )}{\Gamma \vdash e:\forall \ \alpha \ .\ \sigma }}&[{\texttt {Gen}}]\\\\\end{array}}$

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

Die ersten vier Regeln $[{\texttt {Var}}]$, $[{\texttt {App}}]$, $[{\texttt {Abs}}]$ und $[{\texttt {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 $[{\texttt {Inst}}]$ and $[{\texttt {Gen}}]$ gebildet, die die Spezialisierung und Generalisierung von Typen behandeln. Während die $[{\texttt {Inst}}]$ Regel inhaltlich im Abschnitt über die Spezialisierung bereits beschrieben wurde, vervollständigt die Regel $[{\texttt {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 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 &[{\texttt {Var}}]&(id:\forall \alpha .\alpha \rightarrow \alpha \in \Gamma )\\2:&\Gamma \vdash id:int\rightarrow int&[{\texttt {Inst}}]&(1),\ (\forall \alpha .\alpha \rightarrow \alpha \sqsubseteq int\rightarrow int)\\3:&\Gamma \vdash n:int&[{\texttt {Var}}]&(n:int\in \Gamma )\\4:&\Gamma \vdash id(n):int&[{\texttt {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 &[{\texttt {Var}}]&(x:\alpha \in \left\{x:\alpha \right\})\\2:&\vdash \lambda x.x:\alpha \rightarrow \alpha &[{\texttt {Abs}}]&(1)\\3:&\vdash \lambda x.x:\forall \alpha .\alpha \rightarrow \alpha &[{\texttt {Gen}}]&(2),\ (\alpha \not \in frei(\epsilon ))\\4:&id:\lambda \alpha .\alpha \rightarrow \alpha \vdash id:\lambda \alpha .\alpha \rightarrow \alpha &[{\texttt {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 &[{\texttt {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 $[{\texttt {Abs}}]$ und $[{\texttt {Let}}]$.

In der Regel $[{\texttt {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 $[{\texttt {Let}}]$ die Variable die Umbegung 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 monomoph 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 Fokusierung 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 $[{\texttt {Inst}}]$ and $[{\texttt {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 $[{\texttt {Inst}}]$ und $[{\texttt {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 }}&[{\texttt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash e_{0}:\tau \rightarrow \tau '\quad \quad \Gamma \vdash e_{1}:\tau }{\Gamma \vdash e_{0}\ e_{1}:\tau '}}&[{\texttt {App}}]\\\\\displaystyle {\frac {\Gamma ,\;x:\tau \vdash e:\tau '}{\Gamma \vdash \lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\texttt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash e_{0}:\tau \quad \quad \Gamma ,\,x:{\bar {\Gamma }}(\tau )\vdash e_{1}:\tau '}{\Gamma \vdash {\texttt {let}}\ x=e_{0}\ {\texttt {in}}\ e_{1}:\tau '}}&[{\texttt {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 $[{\texttt {Var}}]$ Regel plaziert und nun in diese eingemischt, während die Generalisierung mit in die $[{\texttt {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 Orginal $\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 $[{\texttt {Let}}]$ and $[{\texttt {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 daraufhin, den Haupttyp zu zeigen, dann läßt sich die Wahl auf das Aussuchen geeigneter Typen für $\tau$ in $[{\texttt {Var}}]$ und $[{\texttt {Abs}}]$ einschränken. Die Entscheidung für eine angemessene Auswahl kann nicht lokal erfolgen, aber deren Qualität wird in den Prämissen von $[{\texttt {App}}]$ erkennbar, der einzigen Regel in der zwei unterschiedliche Typen, nämlich der des formalen und der des aktuelle 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 frei(\Gamma )$) für $\tau$ zu machen und diese sowie die in $[{\texttt {Abs}}]$ zu treffende Wahl zu verfeinern, bis alle durch die $[{\texttt {App}}]$ Regeln geforderten Randbedingungen endlich erfüllt sind. Glücklicherweise sind hierfür werder Versuch und Irrtum noch irgendwelche Iterationen erforderlich, da eine effektive Methode zur Berechnung aller notwendigen Entscheidung bekannt ist, die Unifikation (Logik) nach Robinson in Verbindung mit dem sogenannten Union-Find Algorithmus.

Um das Union-Find Verfahren kurz zusammen zu fassen, erlaubt es bei gegebener Menge aller Typen in einem Beweis, diese mittels der Prozedur ${\texttt {union}}$ in Äquivalenzklassen zu teilen und mittels der Prozedur ${\texttt {find}}$ einen Repräsentanten zu bestimmen. Das Wort Prozedur im Sinne von Seiteneffekt betonend, wird das Reich der Logik hier verlassen, um einen effektiven Algorithmus vorbereiten. Der Repräsentant von ${\texttt {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 Typevariable ist dann
    union(ta,tb)
  sonst
    fehler 'typen passen nicht zusammen'

Algorithmus W

Algorithmus W

${\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma \quad \tau =inst(\sigma )}{\Gamma \vdash x:\tau }}&[{\texttt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash e_{0}:\tau _{0}\quad \Gamma \vdash e_{1}:\tau _{1}\quad \tau '=newvar\quad unify(\tau _{0},\ \tau _{1}\rightarrow \tau ')}{\Gamma \vdash e_{0}\ e_{1}:\tau '}}&[{\texttt {App}}]\\\\\displaystyle {\frac {\tau =newvar\quad \Gamma ,\;x:\tau \vdash e:\tau '}{\Gamma \vdash \lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\texttt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash e_{0}:\tau \quad \quad \Gamma ,\,x:{\bar {\Gamma }}(\tau )\vdash e_{1}:\tau '}{\Gamma \vdash {\texttt {let}}\ x=e_{0}\ {\texttt {in}}\ e_{1}:\tau '}}&[{\texttt {Let}}]\end{array}}$

Die Präsentation des Algorithmus W wie er im Kasten an der Seite gezeigt wird, weicht nicht nur signifikant vom Orginal ab, sondern stellt auch einen erheblichen Fehlgebrauch der Notation logischer Regeln dar, da er Seiteneffekte 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 Seiteneffekte) angesehen werden.

Die Prozedur '$inst(\sigma )$' spezialisiert den Polytypen $\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 Typen 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 Gesamtkonsten 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 unentscheibar 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.

HIER

The efficiency is slightly lowered for two reasons. First, the binding of type variables in the context has to be maintained to allow computation of ${\bar {\Gamma }}(\tau )$ and an occurs check has to made to prevent recursive types to be build during $union(\alpha ,\tau )$. An example of such a case is $\lambda \ x.(x\ x)$, for which no type can be derived using HM. Because practically types are only small terms and do not build up expanding structures, one can treat them in complexity analysis as being smaller as some constant, retaining O(1) costs.

Der Algorithmus W im Orginal

In the original paper, the algorithm is presented more formally using a substitution style instead of side effects in the method above. In the later form, the side effect invisibly takes care of all places where a type variable is used. Explicitly using substitutions does not only makes the algorithm hard to read, because the side effect occurs virtually everywhere, but also gives the false impression that the method might be costly. When implemented using purely functional means or for the purpose to prove the algorithm to be basically equivalent to the deduction system, full explicitness is of cause needed and the original formulation a necessary refinement.

Weitere Themen

Rekursive Definitionen

Ein zentrale Eigenschaft des Lambda-Kalküls ist, dass rekursive Definitionen nicht elementar sind, sondern mit Hilfe des Fixpunktkomibators ausgedrückt werden können. In der Orginalpublikation 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 ${\texttt {rec}}\ v=e_{1}\ {\texttt {in}}\ e_{2}\ ::={\texttt {let}}\ v=fix(\lambda v.e_{1})\ {\texttt {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 \ {\texttt {rec}}\ v_{1}=e_{1}\ {\texttt {and}}\ \dots \ {\texttt {and}}\ v_{n}=e_{n}\ {\texttt {in}}\ e:\tau }}\quad [{\texttt {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 $[{\texttt {Abs}}]$ und $[{\texttt {Let}}]$ zusammengemischt, wobei die rekursiv definierten Variablen monomorph behandelt werden, wenn sind links vom ${\texttt {in}}$ auftreten, aber polymorph rechts davon. Diese Formulierung fasst die Essenz des let-Polymorphismus vielleicht am besten zusammen.

Siehe auch

• HM(X)
• ...

Einzelnachweise

{{DEFAULTSORT:Type Inference}} [[Category:Type systems]] [[Category:Type theory]] [[Category:Inference]] [[Category:Lambda calculus| ]] [[Category:Theoretical computer science]] [[Category:Formal methods]]