imported>Hoo man: Änderung 234067567 von Clavismax rückgängig gemacht; per Kommentar: Das ist keine vollständige Liste und wir haben hier genug Beispiele

2023-05-27T11:06:35Z

Änderung 234067567 von Clavismax rückgängig gemacht; per Kommentar: Das ist keine vollständige Liste und wir haben hier genug Beispiele

Neue Seite

Durch '''Typinferenz''' ({{enS|''Type inference ''}} mit {{lang|en|''type''}} „(Daten-)Art“ oder „[[Datentyp]]“ und {{lang|en|''inference''}} „Schlussfolgerung“), auch '''Typableitung''' genannt, kann in manchen (stark typisierten) [[Programmiersprache]]n 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 (Logik)|Unifikation]] den allgemeinsten Typ (Haupttyp, ''principal type'') eines Terms.

Die Entwicklung der Typinferenz (für [[ML (Programmiersprache)|ML]]) durch [[Robin Milner|Milner]]<ref group="Anm">Er hat wiederentdeckt, was schon von Hindley (1969), unter Rückgriff auf Ideen von [[Haskell Curry|Curry]] aus den 1950er Jahren, gefunden worden war. ''Pierce, TAPL, 336.''</ref> war ein Meilenstein in der Entwicklung der Programmiersprachen. Sie bedingte, ermöglichte aber zugleich auch anspruchsvollere [[Typsystem]]e, die damit erheblich an Bedeutung gewannen. Gewisse Spracheigenschaften wie [[Typumwandlung|Typanpassung]]en und manchmal [[Überladen]] wurden zurückgedrängt, weil sie mit der Typinferenz kollidieren.

Viele Programmiersprachen unterstützen Typinferenz, zum Beispiel: [[Python (Programmiersprache)|Python]], [[Java (Programmiersprache)|Java]], [[C++11]], [[C-Sharp|C#]] und [[Visual Basic .NET#2005–2007: Visual Basic 8 und 9|Visual Basic]].

== Beispiel ==
Gegeben sei der folgende Code:

<syntaxhighlight lang="c++">
int a = 1;
int b = 2;
auto c = a + b;
</syntaxhighlight>

Hierbei kann das ''Typsystem'' der jeweiligen Programmiersprache (wenn sie ein entsprechendes Typsystem samt striktem Regelwerk besitzt) nun automatisch herleiten, dass die Variable ''c'' vom Typ ''int'' ([[Integer (Datentyp)|Integer]]) sein muss, 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 (Programmiersprache)|SML]] ist es zum Beispiel nicht möglich, ganze Zahlen mit [[Boolesche Variable|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:

<syntaxhighlight lang="ocaml">
fun f(a, b, c) = if b then a(b) else c + 1
</syntaxhighlight>

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 ''<code>c + 1</code>'' 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:

<syntaxhighlight lang="ocaml">
f : ((bool->int) * bool * int) -> int
</syntaxhighlight>

'''Anmerkung:''' Beim obigen Beispiel wurden explizit die Typisierungsregeln der Sprache [[Standard ML|SML]] verwendet. Andere Sprachen wie [[C++]] oder [[Java (Programmiersprache)|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 [[Polymorphie (Programmierung)#Parametrische Polymorphie|parametrischem Polymorphismus]] für den [[Lambda-Kalkül]]. Es wurde erstmals von [[J. Roger Hindley]]<ref>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 [http://www.jstor.org/stable/1995158 jstor.org]</ref> beschrieben und später von [[Robin Milner]]<ref>Milner: ''A Theory of Type Polymorphism in Programming''. In: ''Journal of Computer and System Science'' (JCSS), 17, 1978, S. 348–374, [https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/milner-type-polymorphism.pdf online] (PDF; 1,6 MB)</ref> wiederentdeckt.
[[Luis Damas]] trug eine genaue formale Analyse und einen Beweis der Methode in seiner Doktorarbeit<ref>Luis Damas: ''Type Assignment in Programming Languages''. PhD thesis, University of Edinburgh, 1985 (CST-33-85)</ref> bei, weshalb das Verfahren auch als [[Damas-Milner]]<ref name="Damas">Damas, Milner: {{Internetquelle | url=https://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_types.pdf | abruf=2020-05-21 | titel=''Principal type-schemes for functional programs''. }} (PDF) 9th Symposium on Principles of programming languages (POPL’82), ACM, 1982, S. 207–212.</ref> bezeichnet wird. Unter den herausragenden Eigenschaften des HM sind Vollständigkeit und die Fähigkeit, den allgemeinsten Typen einer gegebenen Quelle ohne Notwendigkeit von [[Typisierung (Informatik)#Typsystem|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 [[Funktionale Programmierung|funktionalen Sprachen]] eingesetzt. Es wurde erstmals als Teil  der Programmiersprache [[ML (Programmiersprache)|ML]] implementiert. Seither wurde HM in verschiedenster Weise erweitert, insbesondere durch beschränkte Typen, wie sie in [[Haskell (Programmiersprache)|Haskell]] verwendet werden.

== Siehe auch ==
* [[Typisierung (Informatik)|Typisierung]]
* [[Typsicherheit]]

== Literatur ==
* Luca Cardelli: [http://lucacardelli.name/Papers/BasicTypechecking.pdf ''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 ==
<references group="Anm" />

== Einzelnachweise ==
<references />

[[Kategorie:Typentheorie]]
[[Kategorie:Datentyp]]

Typinferenz - Versionsgeschichte

imported>Hoo man: Änderung 234067567 von Clavismax rückgängig gemacht; per Kommentar: Das ist keine vollständige Liste und wir haben hier genug Beispiele