Typableitung

Durch Typinferenz 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 (SML)

Gegeben sei der folgende SML-Code:

int a;
int b;
c = a+b;

Das SML-Typsystem kann nun mit Hilfe seines strikten Regelwerks automatisch herleiten, dass die Variable c den Typ int haben muss, da die Variable a bereits vom Typ int ist und der Operator + nicht mit zwei Werten die verschiedene Typen haben verwendet werden kann.

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.

Anmerkungen

1. ↑ Er hat wiederentdeckt, was schon schon von Hindley (1969), unter Rückgriff auf Ideen von Curry aus den 1950er Jahren, gefunden worden war. Pierce, TAPL, 336.

Referenzen

• 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