Typinferenz

Durch Typinferenz (auch Typableitung) kann in manchen (stark typisierten) Programmiersprachen viel Schreibarbeit eingespart werden, indem auf die Niederschrift von Typangaben verzichtet wird, die aus den restlichen Angaben und den Typisierungsregeln hergeleitet (rekonstruiert) werden können; dazu bedient man sich derselben Regeln, die auch zur Typprüfung dienen, als deren Fortentwicklung die Typinferenz in gewisser Weise anzusehen ist. Bei der Durchführung bestimmt man durch Unifikation den allgemeinsten Typ (Haupttyp, principal type) eines Terms.

Die Entwicklung der Typinferenz (für ML) durch Milner^[1] war ein Meilenstein in der Entwicklung der Programmiersprachen. Sie bedingte, ermöglichte aber zugleich auch anspruchsvollere Typsysteme, die damit erheblich an Bedeutung gewannen. Gewisse Spracheigenschaften wie Typanpassungen und manchmal Überladen wurden zurückgedrängt, weil sie mit der Typinferenz kollidieren.

Beispiel

Gegeben sei der folgende Code:

int a;
c = a+b;

Hierbei kann das Typsystem der jeweiligen Programmiersprache (wenn sie ein entsprechendes Typsystem samt striktem Regelwerk besitzt) nun automatisch herleiten, dass die Variable b den Typ int haben muss, da die Variable a bereits vom Typ int ist, und der Operator + nicht mit zwei Werten unterschiedlichen Typs verwendet werden kann. Außerdem muss auch die Variable c vom Typ int sein, da das Ergebnis einer int-Addition ebenfalls vom Typ int ist.

Typinferenz ist wichtig, um dem Programmierer zu helfen, Flüchtigkeitsfehler schnell zu entdecken. In einer streng typisierten Sprache wie SML ist es zum Beispiel nicht möglich, ganze Zahlen mit booleschen Werten zu vergleichen; um genau solche Fehler zu vermeiden und zu finden, werden mittels Typinferenz für alle Ausdrücke Typen hergeleitet, und es wird geprüft, ob alle auf den Ausdrücken ausgeführten Operationen typkonform sind (wenn z. B. wie oben angenommen Additionen nur zwischen zwei Zahlen gleichen Typs erlaubt sind).

Ein etwas komplexeres Beispiel für die Typinferenz ist die Herleitung des Typs der Funktion f im folgenden SML-Code:

fun f (a, b, c) = if b then a(b) else c+1

Zunächst muss die Variable b vom Typ bool (Wahrheitswert) sein, da sie im if-then-else statement nach dem if steht. Als zweites kann man sagen, dass die gesamte Funktion ein int zurückgeben muss, da sowohl der then- als auch der else-Teil denselben Typ haben müssen, und c + 1 vom Typ int sein muss, da 1 vom Typ int ist, und somit auch – aufgrund des Plus-Operators – c vom Typ int sein muss. Nun kann man noch sagen, dass a eine Funktion sein muss, da im then-Teil a auf b angewendet wird. Da then- und else-Teil jedoch denselben Rückgabetyp haben müssen, muss das Ergebnis von der Funktion a angewendet auf b ebenfalls vom Typ int sein. Somit ergibt sich für die Funktion f folgender Typ:

f : ((bool->int) * bool * int) -> int

Anmerkung: Beim obigen Beispiel wurden explizit die Typisierungsregeln der Sprache SML verwendet. Andere Sprachen wie C++ oder Java haben andere Typisierungsregeln, sodass die Typherleitung dort anders aussehen kann oder eventuell aufgrund der schwachen Typisierung der Sprache (es sind an vielen Stellen mehrere verschiedene Typen erlaubt) gar nicht möglich ist.

Hindley-Milner

(Hauptartikel: Typinferenz nach Hindley-Milner)

Hindley-Milner (HM) ist ein klassisches Verfahren der Typinferenz mit parametrischem Polymorphismus für den Lambda-Kalkül. Es wurde erstmals von J. Roger Hindley^[2] beschrieben und später von Robin Milner^[3] wiederentdeckt. Luis Damas trug eine genaue formale Analyse und einen Beweis der Methode in seiner Doktorarbeit^[4] bei, weshalb das Verfahren auch als Damas-Milner^[5] 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 effizientes Verfahren, das die 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 in 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.

Literatur

• Luca Cardelli: Basic polymorphic type checking. Science of Computer Programming, 8(2), 1987.
• Ralf Hartmut Güting, Martin Erwig: Übersetzerbau. Springer, Berlin Heidelberg 1999, ISBN 3-540-65389-9
• Benjamin C. Pierce: Types and programming languages. – Cambridge, Mass.: MIT Press, 2002 ISBN 978-0-262-16209-8

Siehe auch

• Typisierung
• Typprüfung
• Typsystem

Einzelnachweise und Anmerkungen

1. ↑ Er hat wiederentdeckt, was schon von Hindley (1969), unter Rückgriff auf Ideen von Curry aus den 1950er Jahren, gefunden worden war. Pierce, TAPL, 336.
2. ↑ R. Hindley, (1969) The Principal Type-Scheme of an Object in Combinatory Logic, Transactions of the American Mathematical Society, Vol. 146, pp. 29-60 [1]
3. ↑ Milner, (1978) A Theory of Type Polymorphism in Programming. Journal of Computer and System Science (JCSS) 17, pp. 348-374[2]
4. ↑ Luis Damas (1985): Type Assignment in Programming Languages. PhD thesis, University of Edinburg (CST-33-85)
5. ↑ Damas,Milner (1982), Principal type-schemes for functional programs. 9th Symposium on Principles of programming languages (POPL'82) pp. 207–212, ACM: [3]