Typinferenz
... [ Seminar "Programmierkonzepte und Programmiersprachen"]
... [ Inhaltsübersicht ]
... [ zurück ]
... [ weiter ]
Übersicht: Typinferenz
Beschreibung Typinferenz
Der Ausdruck Inferenz stammt von dem englischen Wort "inference" ab, welches man als Schlussfolgerung
oder Rückschluss übersetzen kann. Typinferenz bedeutet demnach Typrückschluss. In der Informatik versteht
man unter Typinferenz das Folgern eines bestimmten Typs für einen gegebenen Ausdruck, obwohl der Typ nicht
explizit angegeben wurde. Stattdessen wird unter Zuhilfenahme eines Algorithmus auf den richtigen Typen
rückgeschlossen. Da Typinferenz jedoch sehr stark von dem jeweiligen Typsystem abhängig ist, kann ein
passender Algorithmus zum Teil auch nur schwer oder gar nicht gefunden werden. ML und Haskell verwenden beide
das sogenannte Hindley-Milner Typsystem, mit welchem sich die Typinferenz gut realisieren lässt.
Hindley-Milner
Typüberprüfung
Um die Besonderheiten der Hindley-Milner Typüberprüfung zu
verdeutlichen, soll als erstes das Vorgehen einer konventionellen
Typüberprüfung an einem Beispiel gezeigt werden.
Beispiel: Konventionelle Typüberprüfung an einen Codestück in C Syntax
a[i] + i
Damit dieses Beispiel bei einer konventionellen Typüberprüfung funktioniert, müssen sowohl a als auch
i deklariert sein. Die Variable a in diesen Fall als array of Integer und i als Integer.
Als Syntax Baum dargestellt, präsentiert sich das Beispiel der Typüberprüfung folgendermassen:
In einen ersten Schritt werden nun die Typnamen der Deklarationen in den Blattknoten übernommen.
Nun wird als erstes der "[]"-Unterknoten überprüft. Der linke Operand muss ein array sein und
der rechte Operand ein Integer. Da dies der Fall ist, wird diese Überprüfung ohne Fehler bestanden.
Davon ausgehend wird nun auf den Typ des Unterknotens geschlossen. Dieser erhält den Basistypen des arrays,
in diesen Fall Integer.
Als letztes wird der "+"-Knoten untersucht. Unterstellt man, dass die Sprache, in der die Prüfung
stattfindet,keine impliziten Konversionen erlaubt, folgt aus den "+"-Operator, dass beide Operanden
den selben Typ haben müssen. Des weiteren muss für diesen Typ die "+"-Operation definiert
sein. Da beide Operanden den Typ Integer haben, werden beide Vorraussetzungen erfüllt und der Ausdruck ist
somit korrekt. Das Resultat bei der "+"-Operation ist der Typ der Operanden, also Integer in diesen Fall.
Beispiel: Typüberprüfung an den gleichen Codestück bei Typinferenz
a[i] + i
Bei diesem Beispiel wird nochmals das gleiche Codestück überprüft, nur wird diesmal davon
ausgegangen, dass kein Typ für a und i deklariert wurde. Wie das Beispiel zeigen wird, kommt die
Typüberprüfung trotzdem zur selben Lösung wie beim ersten Beispiel.
In einen ersten Schritt ordnet die Typüberprüfung allen Variablen ohne Typ einen internen Typnamen zu.
Der "[]"-Unterknoten wird wiederum als erstes analysiert. Damit der Ausdruck korrekt ist, muss der
Typ von a ein array sein. Auf den Basistyp des arrays kann jedoch noch nicht geschlossen werden.
Die Typüberprüfung schliesst des weiteren darauf, dass i vom Typ Integer ist.Dies geschieht wiederum
in der Annahme, dass in der Programmiersprache nur der Typ Integer als Index eines arrays zugelassen wird.
Die Typüberprüfung schliesst aus den Erkenntnissen über die beiden Typen, dass der gesamte
"[]"-Unterknoten fehlerlos ist und das Resultat des Unterknotens somit der Basistyp von a ist.
Als letztes wird der "+"-Knoten ausgewertet. Die Typüberprüfung schliesst hier darauf, dass der
Basistyp des arrays Integer sein muss, da beide Operanden den selben Typ haben müssen damit der Ausdruck
korrekt ist. Das Ergebnis ist damit der gleiche Syntaxbaum wie im oberen Beispiel.
Instantiierung
Wird eine Typvariable durch einen wirklichen Typ ersetzt oder ein Typ durch einen spezielleren Untertypen,
dann werden alle Instanzen dieser Variablen sofort durch den neuen Typen ersetzt. Dieser Vorgang des
Ersetzten nennt man Instantiierung. Das Ersetzen wird oft durch Tabellen von Typausdrücken erreicht, die
mehrere Indirektstufen besitzen und Symboltabellen ähneln.
Unifikation
Im Laufe des Ersetzens von Typvariablen durch echte Typen kann sich herausstellen das 2 Typvariablen den selben
Typ besitzen. Dies geschah zum Beispiel im obigen Beispiel, wo sich im Laufe der Typüberprüfung
herausstellte, dass alpha und gamma beide vom Typ Integer sind.
Es kann sich allerdings auch schon rausstellen, dass 2 Typvariablen gleich sein müssen damit ein Ausdruck
korrekt ist, obwohl noch nicht der wirkliche Typ bekannt ist. Ein Beispiel wären 2 arrays alpha und beta,
die den selben Typ haben müssen, damit der Ausdruck korrekt arbeitet. In diesen Fall muss dann beta durch alpha
in allen Ausdrücken ersetzt werden. Dieser Vorgang wird Unifikation genannt.
Im Rahmen der Unifikation gibt es drei grundlegende Fälle die auftreten können:
1) Jede Typvariable vereint sich mit jeden Typausdruck und wird mit dem Ausdruck instantiiert.
(Bsp.: Eine Variable beta vereint sich mit den Ausdruck array of alpha und beta wird mit den Ausdruck array of alpha
instantiert.)
2) Zwei Typkonstanten(wirkliche Typen wie Integer,boolean...) vereinen sich nur, wenn sie vom selben Typ sind.
(Bsp.: Vereinigung von Integer und Integer)
3) Zwei Typkonstruktoren(wie array oder struct) vereinen sich nur, wenn sie durch Anwendung des selben Typkonstruktors
entstehen und alle ihre Komponententypen sich auch vereinigen lassen.
... [ Seminar "Programmierkonzepte und Programmiersprachen"]
... [ Inhaltsübersicht ]
... [ zurück ] ... [ Seitenanfang ]
... [ weiter ]