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 HindleyR. Hindley, (1969) The Principal Type-Scheme of an Object in Combinatory Logic, Transactions of the American Mathematical Society, Vol. 146, S. 29–60 beschrieben und später von Robin MilnerMilner, (1978) A Theory of Type Polymorphism in Programming. Journal of Computer and System Science (JCSS) 17, S. 348–374 online wiederentdeckt. Luis Damas trug eine genaue formale Analyse und einen Beweis der Methode in seiner DoktorarbeitLuis Damas (1985): Type Assignment in Programming Languages. PhD thesis, University of Edinburg (CST-33-85) bei, weshalb das Verfahren auch als Damas-MilnerDamas, Milner (1982), Principal type-schemes for functional programs. 9th Symposium on Principles of programming languages (POPL'82) S. 207–212, ACM: 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 Typen

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 stellt die auch oft als geschriebene Funktionsanwendung dar, während die Abstraktion die anonyme Funktion bzw. das Funktionsliteral meint, die inzwischen in vielen zeitgenössischen Programmiersprachen verfügbar ist, dort vielleicht nur wortreicher etwa als ausgeschrieben.

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

Monotypen , 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 oder . Typen können parametrisch sein, wie z. B. . All diese Typen sind Beispiele von Anwendungen von Typfunktionen , z. B. in den vorangegangenen Beispielen, wobei die hochgestellte Ziffer die Zahl der Typparameter angibt. Während die Wahl von grundsätzlich beliebig ist, muss sie im Zusammenhang des HM wenigstens den bequemerweise infix geschriebenen Funktionstyp enthalten. Beispielsweise hat eine Funktion, die ganze Zahlen auf Zeichenketten abbildet, den Typ .Die parametrischen Typen 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 auf, der zwei polymorphe Parameter hat und hier nur als spezieller Fall behandelt wird.

Vielleicht etwas irritierenderweise sind Typvariablen ebenfalls Monotypen. Eine allein stehende Typvariable bezeichnet einen Typ, der genau so konkret ist wie etwa oder 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 nur Werte des Typs 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 jeden Wert auf einen Wert gleichen Typs abbilden. Die identische Funktion ist ein Wert für diesen Typ. Als weiteres Beispiel ist 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 beispielsweise ist durch die Syntax ausgeschlossen. Ferner sind Monotypen eine Teilmenge der Polytypen, so dass Typen insgesamt die allgemeine Form haben.

Freie Typvariablen Freie Typvariablen

In einem Typ ist das Symbol der die Typvariablen im Monotyp bindende Quantor. Die Variablen heißen quantifiziert. Jedes Auftreten einer quantifizierten Variablen in 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 hier . Da Typen wie , 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. , d. h. eine Mischung von gebundenen und ungebundenen Typvariablen, enthalten und was bedeutet eine freie Typvariable darin?

Beispiel 1

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

Im Gegensatz dazu hat den Typ , in dem alle Typvariablen gebunden auftreten. Wertet man z. B. aus, erhält man als Ergebnis eine Funktion vom Typ , was perfekt wiedergibt, dass der Monotyp von in durch den Aufruf verfeinert wurde.

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

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 , Belegung (s. a. Belegung, Zuordnung, Zuweisung) genannt, die jeder Wertvariablen im Kontext einen Typ zuordnet. Alle drei Teile zusammen ergeben eine Typung der Form , die aussagt, dass unter der Annahme der Ausdruck den Typ hat.

Da nun die vollständige Syntax zur Verfügung steht, kann schließlich eine sinnvolle Aussage über den Typ von in Beispiel 1 gemacht werden, nämlich . Im Gegensatz zu den vorangehenden Formulierungen ist die Monotypvariable nicht länger frei, d. h. bedeutungslos, sondern im Kontext als Typ der Wertvariablen 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 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 transformiert werden nach . 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.