Kapitel 6: Typprüfung

Stand: 30.11.2000

© 2001 François Bry
Dieses Lehrmaterial wird ausschließlich zur privaten Verwendung angeboten. Eine nichtprivate Nutzung (z.B. im Unterricht oder eine Veröffentlichung von Kopien oder Übersetzungen) dieses Lehrmaterials bedarf der Erlaubnis des Autors.

Zeitplan: Das Kapitel 6 kann in den 12. und 13. Sitzungen sowie im ersten Teil der 14. Sitzung behandelt werden.

Überblick:

Moderne Programmiersprachen ermöglichen die Festlegung von Typen für Variablen oder Programmausdrücke, die dann automatisch überprüft werden. Dieses Kapitel führt in die diese Technik, "Typprüfung" genannt, ein. Zunächst wird zwischen statische und dynamische Typprüfung unterschieden. Dann wird der Begriff Polymorphie erläutert. Die Sprachkonstrukte von SML zur Spezifikation von Typen und Typ-Constraints werden ferner eingeführt. Schlussregeln für die Typinferenz für vereinfachte SML-Programme werden gegeben und der Unifikationsalgorithmus wird eingeführt. Letztlich wird das Prinzip eines Verfahrens zur automatischen Typinferenz erläutert.

Inhalt:

• 6.1 Die Typprüfung: Eine nützliche Abstraktion für die Entwicklung von korrekten Programmen
• 6.2 Statische contra dynamische Typprüfung
• 6.3 Die Polymorphie: Eine wünschenswerte Abstraktion
• 6.4 Polymorphie contra Überladung
• 6.5 Typvariablen, Typkonstanten, Typkonstruktoren und Typausdrücke in SML
• 6.6 Typkonstruktor contra Wertkonstruktor
• 6.7 Schlussregeln für die Typinferenz
• 6.8 Der Unifikationsalgorithmus
• 6.9 Ein Verfahren zur automatischen Typinferenz

6.1 Die Typprüfung: Eine nützliche Abstraktion für die Entwicklung von korrekten Programmen

Die Typprüfung (type checking) umfasst zwei komplementäre Aufgaben:

1. Die Ermittlung der Typen von Ausdrücken eines Programms aus den Typ-Constraints, die in diesem Programm vorkommen, z.B. die Emittlung der Typen der Namen x (int) und zweimal (int -> int) im folgenden Programm:

        - fun zweimal(x) = 2 * x;

2. Die Überprüfung der Typen, die die Typ-Constraints eines Programms angeben, z.B. die Überprüfung der Korrektheit der angegebene Typen im folgen Programm (die Typ-Constraints des Parameters x und der Typ der Konstante 2.0 (real) sind nicht kompatibel, so dass das Programm ein Typfehler nachweist):

        - fun zweimal'(x:int):real = 2.0 * x;

Typen stellen eine Abstraktion dar, die zur Entwicklung von Algorithmen und Programme äußerst nutzlich ist. Sie ermöglichen zu überprüfen, bevor ein Programm aufgeführt wird oder während einer Ausführung eines Programmes, dass die Parameter, die an Prozeduren "weitergegeben" werden, nicht verwechselt worden sind.

6.2 Dynamische contra statische Typprüfung

Eine Typprüfung kann zur Laufzeit durchgeführt werden, d.h. wenn das Programm aufgeführt wird und Ausdrücke ausgewertet werden. Man spricht dann von einer "dynamischen Typprüfung". Die Programmiersprachen Lisp, Pascal und Smalltalk führen eine dynamische Typprüfung durch. Die Programmierprache Java ermöglicht die dynamische Typprüfung. Die meisten stark (oder streng) typisierten Programmiersprachen führen eine dynamische Typprüfung durch.

Eine Typprüfung kann aber auch zur Übersetzungszeit durchgeführt werden, d.h. wenn das Program auf syntaktische Korrektheit überprüft wird und wenn es in ein Programm in der Maschinensprache umgewandelt wird, also bevor das Programm ausgeführt wird. Man spricht dann von einer "statischen Typprüfung". Die Programmiersprachen SML, Miranda, C++ und auch Java führen eine statische Typprüfung durch. Eine Besonderheit von SML liegt darin, dass diese Programmiersprache ausschließlich eine statische Typprüfung durchführt. Die statische Typprüfung wurde für SML konzipiert und mit SML eingeführt -- siehe:

R. Milner. A theory of type polymorphism in programming languages, Journal of Computer and System Science, vol. 17, pp. 348-375, 1978

Eine Programmiersprache, die eine dynamische Typprüfung durchführt, heißt "dynamisch typisiert". Eine Programmiersprache, die eine statische Typprüfung und keine dynamische Typprüfung durchführt, heißt "statisch typisiert". Eine Programmiersprache, die überhaupt keine Typprüfung durchführt, heißt "nicht typisiert".

Es ist zu betonen, dass manche moderne Programmiersprachen wie C nicht typisiert sind. Solche Programmiersprache führen häufig zu Programmierfehler -- in C oft, wenn Zeiger verwendet werden.

Im Gegensatz zu anderen Programmiersprachen wie C++ und Java führt SML überhaupt keine dynamische Typprüfung durch. Keine dynamische Typprüfung, sondern eine ausschließlich statische Typprüfung durchzuführen hat die folgenden Vorteile:

1. Zum einen trägt die statische Typprüfung zur frühen Erkennung von Programmier- oder konzeptionsfehler schon während der Programmentweicklung bei.
2. Zum zweiten entlastet eine ausschließlich statische Typprüfung die Laufzeit von einer zeitaufwendigen Aufgabe und trägt zur Einfachheit des Übersetzers (bzw. des Auswerters) bei.
3. Zum dritten können bei statisch typisierten Programmiersprachen keine "Laufzeitfehler" vorkommen, d.h. Fehler im Programm in der Maschinensprache, in das das ursprüngliche Programm übersetzt wird. (Selbstverständlich gilt dies nur insofern, dass der Übersetzer selbst fehlerfrei ist.)

Die Programmierpraxis hat gezeigt, dass die statische Typrüfung eine sehr große Hilfe zur Entwicklung von fehlerfreien Programmen ist. Es ist zu erwarten, dass die statische Typrüfung sich unter den zukünftigen industriellen Programmiersprachen verbreiten wird.

Was auch die Programmiersprache und ihr Berechnungsmodell -- wie etwa das funktionale, das imperative oder das logische Modell -- sind, die Typprüfung beruht immer auf die selben Techniken. Es ist günstig, diese Techniken in Zusammenhang mit SML zu lernen, weil die Typprüfung dieser Programmiersprache besonders ausgereift ist.

SML ist eine sogeannte "polymorphe" Programmiersprache. Im nächsten Absatz wird diesen Begriff eingeführt. Die Polymorphie hat Folgen, was die Typprüfung angeht: Sie macht fortgeschritene Techniken zur Typprüfung, wie die Unifikation, notwendig.

6.3 Die Polymorphie: Eine wünschenswerte Abstraktion

6.3.1 Polymorphe Funktionen, Konstanten und Typen

Der Algorithmus zum Aneinanderhängen zweier Listen ist derselbe ganz egal, ob es sich um Listen von ganzen Zahlen, um Listen von Zeichen, um Listen von Boole'schen Werte oder um Listen von Objekte eines weiteren Typs handelt.

Dieser Algorithmus kann in SML wie folgt durch die Funktion append implementiert (siehe Absatz 5.4.7):

     - fun append(nil, l) = l
         | append(h :: t, l) = h :: append(t, l); 
     val append = fn : 'a list * 'a list -> 'a list

Die SML-Funktion append ist tatsächlich für Listen von allen möglichen Objekten anwendbar:

     - append([1,2,3,4],[5,6]);
     val it = [1,2,3,4,5,6] : int list

     - append([#"a",#"b",#"c"],[#"d",#"e"]);
     val it = [#"a",#"b",#"c",#"d",#"e"] : char list

     - append([10e~1,20e~1],[30e~1]);
     val it = [1.0,2.0,3.0] : real list  

     - append([[1,2]],[[1,3],[1,4]]);
     val it = [[1,2],[1,3],[1,4]] : int list list  

Eine Funktion oder Prozedur, die wie die oben definierte SML-Funktion append auf aktuellen Parametern unterschiedlicher Typen anwendbar ist, heißt "polymorph". Diese Bezeichnung bezieht sich auf die Parametern, die unterschielicher (Griechisch "poly") Gestalten (Griechisch "morph") sein können. Der Typ einer polymorphen Funktion nennt man einen "polymorphen Typ" oder kurz ein "Polytyp". Beispiele von polymorphen Typen sind in der SML-Syntax:

Polymorph können nicht nur Funktionen und Typen sein, sondern auch beliebige Ausdrücke. In SML ist z.B. die leere Liste nil (auch [] notiert)eine polymorphe Konstante.

Eine Programmiersprache, die wie SML polymorphe Funktionen und Prozeduren ermöglicht, wird "polymorph" genannt. Man sagt auch, dass sie die "Polymorphie" anbietet.

6.3.2 Typen von Vorkommen eines polymorphen Ausdrucks

Ist ein Ausdruck polymorph, so dürfen unterschiedlichen Vorkommen dieses Ausdrucks im selben Programm unterschiedlichen Typen erhalten. Wenn z.B. die polymorphe Funktion append auf Listen von ganzen Zahlen angewendet wird, so erhält die polymorphe Konstante nil im Rumpf von append den Typ int list. Wird aber nun die selbe polymorphe Funktion append auf Listen von Zeichen angewendet, so erhält die polymorphe Konstante nil im Rumpf von append den Typ char list.

Ein weiteres Beispiel einer polymorphe Funktion ist die Identitätsfunktion:

     - val id = fn x => x;
     val id = fn : 'a -> 'a  

Im Ausdruck id(id)(2) erhält das innere Vorkommen von id den Typ int -> int, das äußere den Typ ('a -> 'a) -> ('a -> 'a):

     - id(id)(2);
     val it = 2 : int    

6.3.3 Vorteile der Polymorphie

Nicht alle Programmiersprachen sind polymorph. Viele Programmiersprachen wie z.B. Pascal und Basic verlangen, dass für jede Art von Listen eine append-Funktion speziell für diese Art von Listen programmiert wird. Nichtpolymorphe Programmiersprachen haben die folgenden Nachteile:

1. Die Nichtpolymorphie vergrößert unnötig die Programme und trägt dazu bei, sie unübersichtlich zu machen.
2. Die Nichtpolymorphie erschwert die Wartung von Programmen, weil derselbe Algorithmus in verschiedenen Prozeduren verbessert werden muss.

Die Polymorphie stellt also eine Abstraktion dar, die in Programmiersprachen äußerst wünschenswert ist.

Die Polymorphie ist eine Verbesserung von Programmiersprachen, die erst in den 80er Jahren vorgeschlagen wurde. Dabei war SML sowohl Vorreiterin als auch Untersuchungsfeld. Der immer noch aktuelle Artikel

L. Cardelli and P. Wegner: On understanding types, data abstraction, and polymorphism, ACM Computing Surveys, 17, pp. 471--522, 1985

bespricht das Thema und beschreibt verschiedene Ansätze zur Polymorphie.

6.4 Polymorphie contra Überladung

Wie die Funktion append können einigen vordefinierten Funktionen von SML wie z.B. die Addition auf aktuelle Parameter von unterschiedlichen Typen angewant werden:

     - 2 + 5;
     val it = 7 : int  

     - 2.1 + 4.2;
     val it = 6.3 : real 

Diese Eigenschaft der Addition wurde im Kapitel 2 (Absatz 2) als "Überladung" geannt. Die Frage stellt sich also, ob Überladung und Polymorphie unterschieden werden sollten.

Bei der Addtion handelt es sich um die Verwendung des selben Namens (Bezeichner) zum Aufruf von verschiedenen (System-)Prozeduren: der Prozedur zur Addition von ganzen Zahlen einerseits, der Prozedur zur Addition von Gleitkommazahlen andererseits.

Bei der Funktion append handelt es sdich um die Verwendung der selben Prozedur, folglich auch des selben Namens, mit Aufrufparametern mit unterschiedlichen Typen.

Polymorphie und Überladung sind völlig unterschiedlich:

Die Polymorphie bezeichnet die Verwendung der selben Prozedur mit Aufrufparametern mit unterschiedlichen Typen.

Die Überladung bezeichnet die Verwendung des selben Namens zur Bezeichnung von verschiedenen Prozeduren.

Die Überladung war schon in FORTRAN, einer der ältesten Programmiersprachen, vorhanden. Die Polymorphie ist viel später erschienen, erst nachdem stark typisierte Programmiersprachen entwickelt wurden. Untypisierten Programmiersprachen bedürfen keine Polymorphie. Die automatische Typanpassung von schwach typisierten Programmiersprachen ermöglicht in den vielen praktischen Fälle die Polymorphie.

Die Überladung wird auch "ad hoc Polymorphie" genannt. Wird die Überladung so bezeichnet, so spricht man von "parametrische Polymorphie" dafür, was hier "Polymorphie" genannt wird.

Die Bezeichnungen "ad hoc Polymorphie" und "parametrische Polymorphie" gehen laut Peter Hancock auf C. Strachey zurück -- siehe Kapitel

Peter Hancock. Polymorphic type-checking, pp. 139-162 in: Simon L. Peyton Jones. The Implementation of functional programming languages, Prentice Hall, ISBN 0-13-453333-X ISBN 0-13-453325 Paperback, 1987

6.5 Typvariablen, Typkonstanten, Typkonstruktoren und Typausdrücke in SML

6.5.1 Typvariablen

Der Typ der polymorphen Funktion append vom Absatz 6.1 lautet:

'a list * 'a list -> 'a list

wie das SML-System nach der Auswertung der Deklaration von append mitteilt:

     - fun append(nil, l) = l
         | append(h :: t, l) = h :: append(t, l); 
     val append = fn : 'a list * 'a list -> 'a list

Dabei ist 'a (oft alpha gesprochen) eine "Typvariable". Die Polymorphie der Funktion append macht es nötig, dass eine Variable im Typ dieser Funktion vorkommt. Wird die Funktion append auf aktuelle Parameter eines Typs t angewandt, so wird die Typvariable 'a an t gebunden. Daraus läßt sich der aktuelle Typ der polymorphen Funktion append in der gegebene Funktionsanwendung bestimmen. Eine solche Ermittlung eines Typs wird "Typinferenz" genannt.

Typvariable werden auch "schematische Typvariablen" und "generische Typvariablen" (letzteres u.a. in der Programmiersprache Miranda) genannt.

6.5.2 Typinferenz

Die Typinferenz ist die Schlussfolgerung, durch die der Typ eines Ausdrucks ermittelt wird oder die Korrektheit der Typ-Constraints eines Programm überprüft werden. Betrachten wir die folgende Funktionsdeklaration:

     - fun zweimal(x) = 2 * x;

Der Typ der Funktion zweimal kann wie folgt ermittelt werden. Da 2 eine ganze Zahl ist, steht der überladene Name * für die Multiplikation zweier ganzen Zahlen. Folglich hat x den Typ int. Daraus folgt den Typ int -> int der Funktion zweimal.

     - append([1,2,3,4],[5,6]);
     val it = [1,2,3,4,5,6] : int list

Die aktuelle Parameter der Funktionsanwendung haben den Typ int list. Aus dem polymorphen Typ 'a list * 'a list -> 'a list von append und dem Typ int list der aktuellen Parametern der Funktionsanwendung folgt der aktuelle Typ von append in der Funktionsanwendung:

int list * int list -> int list.

     - append([#"a",#"b",#"c"],[#"d",#"e"]);
     val it = [#"a",#"b",#"c",#"d",#"e"] : char list

In diesem Fall wird 'a an char gebunden, so dass aus dem polymorphen Typ 'a list * 'a list -> 'a list der aktuelle Typ

char list * char list -> char list

von append in der Funktionsanwendung folgt.

     - append([[1,2]],[[1,3],[1,4]]);
     val it = [[1,2],[1,3],[1,4]] : int list list  

Dieser Fall ist nur scheinbar komplizierter. Hier wird die Typvariable 'a an den Typ int list gebunden, so dass der aktueller Typ von append in der Funktionsanwendung

int list list * int list list -> int list list

ist. Wir erinnern daran, dass der Postfix-Operator list linksassoziativ ist und dass der Operator * (Karthesisches Produkt) stärker bindet als der Operator ->, so dass der obige Typausdruck für den folgenden steht:

((int list) list * (int list) list) -> ((int list) list)

6.5.3 Typausdrücke

In den vorangehenden Beispiele kommen "Typausdrücke" vor. In diesem Absatz wird der Formalismus näher erläutert, mit dem in einem SML-Programm die Typen von Ausdrücken festgelegt werden können.

Typvariablen sind herkömmlichen Variablen ähnlich. Sie werden an Typausdrücke gebunden.

Ein Typausdruck ist entweder atomar, wie z.B. int und char, oder zusammengesetzt, wie z.B. int list oder (int list) list.

6.5.4 Typkonstanten

Atomare Typausdrücke, die keine Typvariaben sind, werden "Typkonstante" genannt. Beispiele von Typkonstanten sind: int, real, bool, string, char und unit. Typkonstanten bezeichnen Typen, die nicht zusammengesetzt sind. Im Kapitel 8 wird gezeigt, wie solche Typen definiert werden können.

6.5.5 Typ-Constraints

Ein Typ-Constraint (siehe Kapitel 2, Absatz 2.4 Namen, Bindungen und Deklarationen) ist ein Ausdruck der Gestalt:

Ausdruck : Typausdruck

wie z.B.:

x : int
l : char list
(fn x => x * x) : int -> int

Typ-Constraints werden auch Typisierungsausdrücke genannt.

6.5.6 Zusammengesetzte Typausdrücke und Typkonstruktoren

Zusammengesetzte Typausdrücke werden ähnlich wie Funktionsanwendungen, oft mit Postfix- oder Infix-Operatoren, gebildet. Z.B.:

'a * 'a

int list

int -> int

int list * int list -> int list

{Vorname:string, Nachname:string}

Die Operatoren, die dabei verwendet werden, werden "Typkonstruktoren" genannt.

Typkonstruktoren unterscheiden sich syntaktisch von Funktionsnamen nicht. Typkonstruktoren werden aber anders als Funktionsnamen verwendet:

• Wird eine Funktion wie append auf die Listen [1,2] und [3] angewandt, so geshieht dies, damit die Funktionsanwendung append([1,2],[3]) ausgewertet wird, d.h. damit der Wert [1,2,3] berechnet wird.
• Wird der Typkonstruktor * auf die Typausdrücke int und 'a list angewandt, so geschieht dies lediglich, damit der Typausdruck (int * 'a list) gebildet wird.

Bei der Anwendung eines Typkonstruktors auf "Parametern" findet keine Auswertung statt. Eine solche Auswertung könnte in der Regel nicht berechnet werden. Die Anwendung des Typkonstruktors * (Karthesisches Produkt) auf die beiden Typkonstanten int und real bezeichnet z.B. die Menge aller Paare (n, w), so dass n eine ganze Zahl ist und w ein Boole'scher Wert ist. Mathematisch gesehen bildet die Anwendung des Typkonstruktors * (Karthesisches Produkt) die Typen int und real, d.h. die Mengen Z und {true, false}, auf die folgende Menge:

{(n, w) | n in Z und w in {true, false}}

Diese Menge kann nicht berechnet werden, weil sie unendlich ist. In einem Fall wie etwa bool * bool, wäre die Berechnung des zusammengesetzten Typs möglich, weil er endlich ist. Die Berechnung eines (endlichen) Typs wäre aber sinnlos. Typen werden lediglich verwendet, um Programmierfehler zu vermeiden, nicht um allen möglichen Werte zu berechnen.

6.5.7 Die ''-Typvariablen zur Polymorphie mit Typen mit Gleichheit

Die Gleichheitsfunktion = ist überladen, weil das selbe Symbol = für viele verschiedenen Typen wie etwa bool, int, die polymorphen Typen List, Vektor und Verbund.

Viele Algorithmen, für die eine Implementierung als polymorphe Funktion, beziehen sich auf die Gleichheit.

Damit die Spezifikation in SML von solchen Funktionen möglich ist, bietet SML die ''-Typvariablen. Eine ''-Typvariable wird ''Name geschrieben. ''-Typvariablen stehen immer für Typen mit Gleichheit.

Ein Beispiel der Verwendung von ''-Typvariablen ist der polymorphe Prädikat member zum testen, ob ein Element in einer Liste vorkommt (wir erinnern daran, dass ein Prädikat eine Funktion ist, deren Anwendung Boole'sche Werte liefert):

     - fun member(x, nil)         = false
          | member(x, head::tail) = if x = head 
                                    then true 
                                    else member(x, tail);
     val member = fn : ''a * ''a list -> bool 

     - member(3,[1,2,3,4]);
     val it = true : bool

     - member(#"c",[#"a",#"b",#"c",#"d"]);
     val it = true : bool

     - member([1,2],[[1,2,3],[1,2],[1,2,3,4]]);
     val it = true : bool   

''-Typvariablen können nur an Typausdrücke gebunden werden, die Typen mit Gleichheit bezeichnen:

    - member((fn x => x), [(fn x => x)]);
    Error: operator and operand don't agree [equality type required]
       operator domain: ''Z * ''Z list
       operand:         ('Y -> 'Y) * ('X -> 'X) list
       in expression:
         member ((fn x => x),(fn  => ) :: nil) 

6.6 Typkonstruktor contra Wertkonstruktor

Ein Typkonstruktor soll nicht mit dem (Wert-)Konstruktor dieses Typs verwechselt werden. Der Typkonstruktor list und der Listenkonstruktor cons (::) sollen z.B. nicht verwechselt werden:

• Mit list und einem Typausdruck wie z.B. 'a oder int * bool w werden der polymorphe Listentyp 'a list und der Listentyp (int * bool) list gebildet. list und * sind in diesen Beispielen Typkonstruktor.
• Mit cons (::) und einem (herkömmlichen) Ausdrucken wie z.B. 1, "abc" oder (3, false) werden wie folgt Listen gebildet:

       - 1 :: [];
       val it = [1] : int list

       - "abc" :: [];
       val it = ["abc"] : string list

       - (3, false) :: [];
       val it = [(3,false)] : (int * bool) list  

cons ist ein (Wert-)Konstruktor.

Die Unterscheidung gilt für alle zusammengesetzten Typen. In der folgenden Tabelle werden die Argumente der Typkonstruktoren und der Konstruktoren der jeweiligen Typen mit . dargestellt:

Der allgemeine Fall ist, dass es zu *einem* Typkonstruktor *mehrere*, aber endlich viele (Wert-)Konstruktoren des Typs geben kann. Z. B. sind cons (::) und nil die beiden (Wert-)Konstruktoren eines Listentyps. nil ist ein 0-stellige (Wert-)Konstruktor, d.h. eine Konstante. Im Kapitel 8 werden Typen eingeführt, die mehrere (Wert-)Konstruktoren einer Stelligkeit größer-gleich 1 haben.

6.7 Schlussregeln für die Typinferenz

Im Absatz 6.5 wurde die Typinferenz informell eingeführt. Wir wollen sie nun formal und als Algorithmus für eine Vereinfachung von SML definieren. Ist die Typinferenz so definiert, so läßt sie sich formal untersuchen, z.B. auf Korrekheit prüfen, und auch als Programm implementieren.

6.7.1 Eine Vereinfachung von SML: SMalL_1

Die Programmiersprache SMalL_1 ist eine Vereinfachung von SML. SMalL_1 enthält die val-Deklarationen, die vordefinierten Typen bool, int, real, die Listen und Vektoren mit ihren vordefinierten Funktionen, das fn-Konstrukt zur Funktionsbildung, die Fallunterscheidung mit if-then-else und natürlich die Typ-Constraints.

SMalL_1 läßt keinen Musterangleich (pattern matching), keine Verbunde, weder let- noch local-Ausdrücke zu. Zudem hat SMalL_1 keine der Konstrukten von SML (zur Spezifikationen von u.a. Ausnahmen und Modulen), die bisher nicht eingeführt wurden.

Der Einfachheit halber und ohne Beschränkung der Allgemenheit wird angenommen, dass alle Funktionen in SMalL präfix notiert werden.

Wir erinnern daran, dass eine n-stellige SML- oder SMalL-Funktion als eine 1-stellige Funktion angesehen werden kann, deren (einzigen) Parameter ein n-Vektor ist (siehe Absatz 5.3.1). So ist es möglich, jede Funktionsanwendung F(P1, ..., Pn) als Objekt der Gestalt F P anzusehen.

6.7.2 Logischer Kalkül

Zur Spezifikation eines Algorithmus für die Typinferenz in SMalL-Programmen bedienen wir uns den Ansatz eines "logischen Kalküls". Ein logischer Kalkül besteht aus:

1. einer (formalen) Sprache, in dem Aussagen über die zu bewiesenen Eigenschaften ausgedruckt werden;
2. Schlussregeln, womit weitere Aussagen aus bereits festgestellten Aussagen geschlossen werden können;
3. Axiome und Annahmen, d.h. Aussagen, deren Gültigkeit nicht bewiesen werden müssen, weil sie immer gelten (Axiome) oder weil sie angenommen werden (Annahme).

Im Fall des (logischen) Kalküls für die Typinferenz gilt:

• die (formale) Sprache ist der Formalismus, in der die Typ-Constraints (oder Typisierungsaussagen) wie etwa (fn x => x) : 'a -> 'a ausgedrückt werden
• die Axiome sind die Typ-Constraints für die vordefinierten Typen wie etwa 34 : int, ~98.67e4 : real, false : bool, nil : 'a list, und @ : ('a list * 'a list) -> 'a list (@ ist die vordefinierte Infixfunktion append von SML)
• die Annahmen sind die Typ-Constraints aus dem Programm -- wie etwa: x : int oder (fn x => a*x + b*x**2) : real -> real -- sowie für jeden Ausdruck oder Teilausdruck A aus dem Programm, für den das Programm kein Typ-Constraint enthält, ein Typ-Constraint A : V mit V Typvariable, sodass für jedes Paar solchen verschiedenen Ausdrücke A die Typvariablen V paarweise verschieden sind.

Die Axiome werden "Typsierungsaxiome", die Annahmen "Typsierungsannahmen" genannt.

6.7.3 Gestalt der Schlussregeln eines logischen Kalküls

Eine Schlussregl hat die folgende Gestalt

wobei n >= 1, Pr1, ..., Prn und Sch Ausdrücke in der zugrunden liegenden formalen Sprache, also in der formalen Sprache des logischen Kalküls, sind. Pr1, ..., Prn sind die "Pämisse", Sch der "Schluss". Eine solche Regel bedeutet: Aus Pr1 und ... und Prn folgt logisch Sch.

Verlangt eine Schlussregel eine Annahme A, so hat sie die Gestalt (Die Annahme (A) kann über jeder Prämise stehen):

Mögliche Schlussregeln wären z.B.:

    append:('a list * 'a list) -> 'a list   [1,2]:int list  [3,4]:int list
R1: ----------------------------------------------------------------------
                   append([1,2], [3,4]):int list

        1 : int    2 : int
  R2:   ------------------
         [1,2] : int list 

        0 : int      [1,2]: int list  
  R3:   ---------------------------- 
            [0,1,2] : int list 

Obwohl sinnvoll und korrekt gebildet sind diese Schlussregeln keine Schlussregel des logischen Kalküls für die Typinferenz, weil sie zu speziell sind. Schlussregeln werden bevorzugt, die weder für eine besondere Prozedur, noch für besondere aktuelle Parameter definiert sind.

Eine bekannte Schlussregel ist der "modus ponens" für Formeln der Aussagenlogik:

     a    a => b
     -----------
          b

Eine andere bekannte Schlussregel ist die "Kontraposition", ebenfalls für Formeln der Aussagenlogik:

          a => b
     -----------------
     (not b) => (not a)

In den Schlussregeln "modus ponens" und "Kontraposition" stehen a und b für aussagenlogischen Formlen. a und b sind also Variablen der Metasprache, die zur Definition der Schlussregeln verwendet wird, aber keine aussagenlogischen Variablen.

6.7.4 Beweisbegriff bezüglich eines logischen Kalküls

Ist ein logischer Kalkül durch eine formale Sprache, Schlussregeln und Axiome sowie möglichen Annahmen definiert, so werden Beweise als Bäume (im Sinne der Graphentheorie) definiert, deren Blätter (im Sinne der Graphentheorie) Axiome und Annahmen sind und wie folgt von den Blätter her aufgebaut werden können:

1. Axiome und Annahmen sind Beweise.

2. Sind B1, ..., Bn Beweise mit Wurzel P1, ... bzw. Pn und ist

eine Schlussregel, so ist der Baum

ein Beweis.

Oft werden zusätzliche Bedingungen gestellt, dass so gebildeten Bäume erfüllen müssen, um Beweise des logischen Kalküls zu sein.

Die Bäume, die aus den Axiomen und Annahmen unter Verwendung der Schlussregeln gebildet werden, haben ein paar bemerkenswerte Merkmale, die charakteristisch für die Beweise eines logischen Kalküls sind:

1. Ihre Kanten sind waagerechte Linien;
2. Ihre Wurzel befindet sich unten, ihre Blätter befinden sich oben.

Die Beweise eines logischen Kalküls sind also besondere Bäume: Ihre Wurzeln stehen unten, ihre Blätter oben.

Beispiel:

Mit den vorangehenden Schlussregeln R2 und R3 und den Axiomen 0:int, 1:int und 2:int läßt sich der folgende Beweis bilden:

                                1:int       2:int 
                            R2: -----------------
                   0:int        [1,2]:int list
               R3: ---------------------------
                         [0,1,2]:int list

Verlangt eine Schlussregel eine Annahme A, so kann sie nur dann auf Beweise B1, ..., Bn zur Bildung eines Beweises B angewandt werden, wenn ein der Beweise B1, ..., Bn diese Annahme A als Blatt besitzt.

6.7.5 Die Schlussregeln für die Typinferenz oder "Typsierungsregeln"

Im Folgenden stehen T, Ti für Typausdrücke, V für Typvariabeln, F, B, P, A, Ai für Ausdrücke.

T3 (Funktionsbildung oder Lambda-Abstraktion):

                                      (P : T1)
                                       A : T2  
                               ----------------------
                               (fn P => A) : T1 -> T2 

wobei V eine Typvariable und T ein Typausdruck sind.

T4 setzt zudem dvoraus, dass die Typvariable V im Typausdruck T nicht vorkommt.

Die Bedingung der Schlussregel T4 ist notwendig: Was wäre wohl der Typ 'a, der gleich mit dem Typ 'a list wäre?

Die Definition der Beweise verlangt, dass eine Bindung einer Typvariablen V an einem Typausdruck T unter Verwendung der Schlussregel T4 nicht nur für *ein*, sondern für *alle* Vorkommen von V, die gemäß der Blockstruktur das selbe Objekt bezeichnen, im Beweis gilt.

T5 (Einführung von Konstruktoren):

                              A1 : T      A2 : T list   
                     T5-list: ------------------------
                               (A1 :: A2) : T list   

                                  A1 : T  ... An : T
                 T5-n-Vektor: ---------------------------
                              (A1, ..., An) : T * ... * T   (n mal)

Für jeden n >= 1 gibt es eine Regel T5-n-Vektor. Da ein Programm endlich ist, kann man sich für jedes gegebene Programm auf eine endliche Anzahl von Schlussregeln beschränken, nämlich alle Schlussregeln T1 bis T4 und nur die Schlussregeln T5-n-Vektor für n-Vektoren einer Steligkeit n, die im Programm vorkommen.

6.7.6 Typiesierungsbeweise

Typsierungsbeweise werden wie folgt definiert:

1. Typsierungsaxiome und -annahmen sind Typieiserungsbeweise.

         P1 ... Pn
2. Ist --------- eine Typsierungsregel und sind B1, ..., Bn
           S                                           B1 ... Bn 
   Typsierungsbeweise von P1, ... bzw. Pn, so ist  C = ---------
                                                           S
   ein Typsierungsbeweis, wenn in C für alle Ausdrücke A, die gemäß
   der Blocksytruktur das selbe Objekt bezeichnen, alle Anwendungen der
   Instanziierungsregel T4 mit Prämisse A : V den selben Schluss A : T
   (also mit dem selben Typausdruck T) haben. 

6.7.7 Beispiele von Typiesierungsbeweisen

Seien die folgende SMalL-Funktion:

     val f = fn x => +(*(a, x), 2.0)   (*   a*x + 2.0   *)

und die folgende Typsierungsannahme:

a : real

Der Typ real -> real von f läßt sich durch den folgenden Typsierungsbeweis feststellen:

                                    Annahme  x : 'x
                                          T4 --------
                       Annahme a : real      x : real
                   T5-2-Vektor ----------------------
Axiom * : (real * real) -> real  (a, x): real * real
       T1 ------------------------------------------
        +: (real * real) --> real     *(a, x) : real     Axiom 2.0 : real
     T1 -----------------------------------------------------------------
                              +(*(a, x), 2.0) : real
                  T3 ----------------------------------------
                     (fn x => +(*(a, x), 2.0)) : real -> real

Wäre nun die Funktion f wie folgt definiert:

     val f = fn (x:int) => +(*(a, x), b)   (*   a*x + 2.0   *)

Der vorangehender Beweis läßt sich nicht mehr aufbauen, weil mit der TYpisierungsannahme x : int sich kein Beweis von *(a, x) : real bilden läßt.

Es ist bemerkenswert, dass der Beweis vom ersten Beispiel genau die Struktur des Ausdrucks (fn x => +(*(a, x), 2.0)) widerspriegelt: Wird der Beweis von seiner Wurzel zu seinen Blätter, d.h. Annahmen oder Axiome durchlaufen, so zerlegt der Beweis den Ausdruck in seinen Teilausdrücke. So konnte der Beweis wie folgt aufgebaut werden:

(*) (fn x => +(*(a, x), 2.0)) : 'p1 -> 'p2 weil es sich um ein fn-Ausdruck handelt +(*(a, x), 2.0) : 'p2 'p1 = 'p2 weil + : ('p1 * 'p1) -> 'p1 2.0 : real Axiom

Folglich:

'p1 = 'p2 = real

Also:

(fn x => +(*(a, x), 2.0)) : real -> real

Das Prinzip, das sich hier anhand eines Beispiels erkennen läßt, gilt im Allgemeinen. Darauf beruht die Automatisierung der Typprüfung.

Der Beweis vom ersten Beispiel beinhaltet einen "Eureka-Schritt", der schwer zu automatisieren wäre: die Anwendung der Instanziierungsschlussregel T4 auf x : 'x, um x : real zu erhalten. Da es unendlich viele Typen gibt, die Kandidaten zur bindung von 'x sind, läßt sich daraus nur schwer einen brauchbaren Algorithmen entwickeln. Die Lösung zu diesem Problem liegt darin, Typvariablen nur soweit wie nötig an Typausdrücke zu binden -- wie bereit im Beweis (*) angewendet wurde.

Für die Bindung von Typvariablen "nur soweit wie nötig" wird der sogeannte Unifikationsalgorithmus verwendet.

6.8 Der Unifikationsalgorithmus

Im Folgenden bezeichnen V, Vi Typvariablen, T, Ti Typausdrücke, K, Ki Typkonstanten.

Zur Unifikation zweier Typausdrücken TA1 und TA2 gehe wie folgt vor:

Beispiel einer Anwendung des Unifkiationsalgorithmus:

6.9 Ein Verfahren zur automatischen Typinferenz

6.9.1 Prinzip des Verfahrens

Das Verfahren besteht aus zwei Phasen, deren Ausführengen beliebig ineinander verzahnt werden dürfen.

Das Verfahren erhält als Parameter

• einen Ausdruck A (mitoder ohne Typ-Constraint), dessen Typisierung überprüft oder festgestellt werden soll, und
• eine Menge M von Typ-Constraints. Beim ersten Aufruf des Verfahrens ist M leer.

6.9.2 Behandlung der Überschattung

Obwohl Deklarationen von lokalen Variablen mit let- oder local-Ausdrücke in SMalL nicht möglich ist, können die formalen Parametern einer Funktionsdefinition, d.h. in einem fn-Ausdruck (fn . => .) Namen überschatten.

Zur Behandlung der Überschatung wird eine Namenliste oder "Typisierungsumgebung" verwendet, die wie eine Umgebung verwaltet wird:

• Wird während der Phase 1 auf einen Ausdruck gestossen, der eine val-Deklaration oder ein fn-Ausdruck ist, dann wird der im val-Ausdruck deklarierten Namen oder die formalen Parametern des fn-Ausdrucks am Anfang der "Typisierungsumgebung" eingefügt.
• Wird während der Phase 1 eine val-Deklaration oder ein fn-Ausdruck verlassen, so werden alle Namen von der Typsierungsumgebung entfernt, die beim Eintritt in diese val-Deklaration oder diesen fn-Ausdruck in die Typsierungsumgebung eingefügt wurden.
• Die Typ-Constraints, die während der Phase 2 einem Ausdruck zugeordnet werden, werden dem zutreffenden Ausdruck der Typsierungsumgebung zugeordnet. Dazu wird die Typsierungsumgebung von Anfang her durchsucht.

Da zur typinferenz keine Auswertung stattfindet, werden auch keine Werte an Namen gebunden. Folglich reicht es aus, Namen statt Gleichungen der Gestalt Namen = Wert in die Typsisierunfsumgebung aufzunemhen und werden keine lokale Umgebungen benötigt.

6.9.3 Beispiele

1. Sei der Ausdruck A:

   val f = fn x => +(*(a, x), 2.0) (* d.h. a*x + 2.0 *)

   Zerlegung des Ausdrucks:	Typsierungsumgebung (Anfang: unten)
   val f = fn x => +(*(a, x), 2.0)	f	: 'f
   	fn x => +(*(a, x), 2.0)	: 'f
   fn x => +(*(a, x), 2.0)	f	: 'f
   	fn x => +(*(a, x), 2.0)	: 'f 'x->'v1
   	x	: 'x
   +(*(a, x), 2.0)	f	: 'f
   	fn x => +(*(a, x), 2.0)	: 'f 'x->'v1
   	x	: 'x
   	+(*(a, x), 2.0))	: 'v1
   	Unifikation: 'f = 'x->'v1
   +	f	: 'x->'v1
   	fn x => +(*(a, x), 2.0)	: 'x->'v1
   	x	: 'x
   	+(*(a, x), 2.0)	: 'v1
   	+	: 'v1*'v1->'v1
   *(a, x)	f	: 'x->'v1
   	fn x => +(*(a, x), 2.0)	: 'x->'v1
   	x	: 'x
   	+	: 'v1*'v1->'v1
   	*(a, x)	: 'v1
   *	f	: 'x->'v1
   	fn x => +(*(a, x), 2.0)	: 'x->'v1
   	x	: 'x
   	+	: 'v1*'v1->'v1
   	*(a, x)	: 'v1
   	*	: 'v2*'v2->'v2
   	Unifikation: 'v2 = 'v1
   a	f	: 'f
   	fn x => +(*(a, x), 2.0)	: 'x->'f
   	x	: 'x
   	+	: 'v1*'v1->'v1
   	*(a, x)	: 'v1
   	*	: 'v1*'v1->'v1
   	a	: 'v1
   	Unifikation: 'v2 = 'v1
   x	f	: 'x->'v1
   	fn x => +(*(a, x), 2.0)	: 'x->'v1
   	x	: 'x 'v1
   	+	: 'v1*'v1->'v1
   	*(a, x)	: 'v1
   	*	: 'v1*'v1->'v1
   	a	: 'v1
   	Unifikation: 'x = v1
   2.0	f	: 'v1->'v1
   	fn x => +(*(a, x), 2.0)	: 'v1->'v1
   	x	: 'v1
   	+	: 'v1*'v1->'v1
   	*(a, x)	: 'v1
   	*(a, x)	: 'v1
   	*	: 'v1*'v1->'v1
   	a	: 'v1
   	2.0	: 'v1 real
   	Unifikation: 'v1 = real Nun ist die Typsierungsumgebung wie folgt:
   	f	: real->real
   	fn x => +(*(a, x), 2.0)	: real->real
   	x	: real
   	+	: real*real->real
   	*(a, x)	: real
   	*(a, x)	: real
   	*	: real*real->real
   	a	: real
   	2.0	: real

2. Sei der Ausdruck A:

   val not = fn x => if x = true than false else true;

   val not = fn x => if x = true than false else true;

   not	: 'a
   fn x => if x = true than false else true	: 'a
   not	: 'a
   fn x => if x = true than false else true	: 'a 'b->'c
   x	: 'b
   if x = true than false else true	: 'c
   Unifiziere 'a und 'b->'c	'a = 'b -> 'c
   not	: 'b -> 'c
   fn x => if x = true than false else true	: 'b -> 'c
   x	: 'b
   if x = true than false else true	: 'c 'd
   x = true	: bool
   false	: 'd bool
   true	: 'd bool
   Unifiziere: 'c und 'd: 'd und bool:	'c = 'd 'd = bool
   not	: 'b -> bool
   fn x => if x = true than false else true	: 'b -> bool
   x	: 'b 'e
   if x = true than false else true	: bool
   x = true	: bool
   false	: bool
   true	: bool
   =	: 'e * 'e -> bool
   true	: 'e bool
   Unifiziere: 'b und 'e: 'e und bool:	'b = 'e 'e = bool
   not	: bool -> bool
   fn x => if x = true than false else true	: bool -> bool
   x	: bool
   if x = true than false else true	: bool
   x = true	: bool
   false	: bool
   true	: bool
   =	: bool * bool -> bool
   true	: bool