Typinferenz
Durch Typinferenz (englisch Type inference mit type „(Daten-)Art“ oder „Datentyp“ und inference „Schlussfolgerung“), auch Typableitung genannt, 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[Anm 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.
Sprachen die Typinferenz verwenden, sind zum Beispiel: C++11, C#, Clean, Crystal, D, Dart F#, FreeBASIC, Go, Haskell, Java, Julia, Kotlin, ML, Nim, OCaml, Opa, R, Python, Rust, Scala, Swift, Vala, und Visual Basic.
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 – wegen 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
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[1] beschrieben und später von Robin Milner[2] wiederentdeckt. Luis Damas trug eine genaue formale Analyse und einen Beweis der Methode in seiner Doktorarbeit[3] bei, weshalb das Verfahren auch als Damas-Milner[4] bezeichnet wird. Unter den herausragenden Eigenschaften des HM sind Vollständigkeit und die Fähigkeit, den allgemeinsten Typen einer gegebenen Quelle ohne Notwendigkeit von Annotationen oder sonstigen Hinweisen zu bestimmen. HM ist ein effizientes Verfahren, das die Typisierung nahezu in linearer Zeit bzgl. der Größe der Quelle ermitteln kann, womit es praktisch für die Erstellung großer Programme ist. HM wird bevorzugt in funktionalen Sprachen eingesetzt. Es wurde erstmals als Teil der Programmiersprache ML implementiert. Seither wurde HM in verschiedenster Weise erweitert, insbesondere durch beschränkte Typen, wie sie in Haskell verwendet werden.
Siehe auch
Literatur
- Luca Cardelli: Basic polymorphic type checking. In: 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. MIT Press, Cambridge MA 2002, ISBN 978-0-262-16209-8
Anmerkungen
- 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.
Einzelnachweise
- R. Hindley: The Principal Type-Scheme of an Object in Combinatory Logic. In: Transactions of the American Mathematical Society, Vol. 146, 1969, S. 29–60 jstor.org
- Milner: A Theory of Type Polymorphism in Programming. In: Journal of Computer and System Science (JCSS), 17, 1978, S. 348–374, citeseerx.ist.psu.edu (PDF)
- Luis Damas: Type Assignment in Programming Languages. PhD thesis, University of Edinburgh, 1985 (CST-33-85)
- Damas, Milner: Principal type-schemes for functional programs. Abgerufen am 21. Mai 2020. (PDF) 9th Symposium on Principles of programming languages (POPL’82), ACM, 1982, S. 207–212.