Einleitung

Definition

Wir wollen nun zunächst die folgende Definition von Benjamin C. Pierce betrachten und auseinander nehmen, um eine grundsätzliche Idee zu bekommen, was ein Typsystem ist:

A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.

Es geht bei unserer Betrachtung um program behaviors, also um die Semantik von Computer-Programmen. Historisch gesehen sind Typsysteme ein Bestandteil der Mathematik, der unabhängig von Programmen und Programmiersprachen ist. Diesen Ansatz werden wir hier aber nicht verfolgen. Wir konzentrieren uns auf Anwendungen von Typsystemen in der Informatik.

Typsysteme klassifizieren Terme statisch (d.h. zur Übersetzungszeit) anhand ihrer Struktur. Die Programme werden bei der Typprüfung noch nicht ausgeführt. Aufgrund der statischen Auswertung können Typsysteme nur die Abwesenheit bestimmter ungewünschter Programmverhalten (z.B. Multiplikationen von Booleans mit Strings) garantieren, sie können aber nicht nachweisen, dass ein Fehlverhalten tatsächlich zu Laufzeit auftreten kann:

String s = true ? "Ho Ho Ho" : 2;

Im Falle der oben genannten Java-Anweisung würde es zur Laufzeit nie zu einem Typfehler kommen, da der bedingte Ausdruck immer zu "Ho Ho Ho" vom Typ java.lang.String ausgewertet werden würde. Trotzdem wird er bei der Typprüfung zurückgewiesen, da er seiner Struktur nach einen Typfehler enthält.

Es werden nur bestimmten Arten von unerwünschtem Programmverhalten ausgeschlossen (wie zum Beispiel der Aufruf einer Funktion mit zu wenigen Argumenten). Es gibt aber immer noch Raum für Laufzeitfehler wie Array-Zugriffe mit ungültigen Indizes oder Division durch Null. Welche Fehlverhalten erst zur Laufzeit und welche bereits zur Übersetzungszeit ausgeschlossen werden ist abhängig von der Wahl der Programmiersprache und dem konkreten Programmentwurf.

Schlussendlich muß die Typprüfung ein mechanisch nachvollziehbarer Prozess/Algorithmus sein (tractable), der effizient umgesetzt werden kann.

Motivation

Kurz zusammengefasst gibt es die folgenden Motivationen Typen zur Übersetzungszeit zu prüfen:

• Frühzeitiges Erkennen von Fehlern: Wie bereits gezeigt können bestimmte Arten von Fehlern bereits zur Übersetzungszeit erkannt werden. Dies ist besonders dann hilfreich, wenn sich die fehlerhafte Anweisung in einem selten durchlaufenden Programmteil befindet und sie somit zur Laufzeit möglicherweise erst sehr spät erkannt werden könnte.
• Abstraktionen schützen: So können zum Beispiel in Java Variablen vom Typ boolean nur die Werte true oder false annehmen, selbst wenn ihre technische Repräsentation auch die Werte 12, 15 oder 27 annehmen könnte.
• Dokumentation die zwangsläufig aktuell ist: In großen Programmen können explizite Typangaben helfen, Funktionen oder Datenstrukturen zu verstehen. Im Gegensatz zu Kommentaren werden die Typangaben vom Compiler überprüft und sind somit für jedes übersetzbare Programm aktuell.
• Effizienz: Da bestimmte fehlerhafte Programmkonstruktionen mit Hilfe von Typsystemen bereits zur Übersetzungszeit ausgeschlossen werden können, werden Laufzeitprüfungen eingespart.

Sichere und unsichere Sprachen, statische und dynamische Typprüfung

Man kann Sprachen in sichere und unsichere Sprachen und Sprachen mit statischer und dynamischer Typprüfung einteilen. Als "sicher" bezeichnet man eine Sprache, die ihre Abstraktionen immer schützt. So kann man zum Beispiel in Java einem boolean nie den Wert 27 zuweisen, egal wie man sich bemüht. C ist eine unsichere Sprache, weil die Sprachdefinition weisse Flecken hat. Bestimmte C-Programme lösen undefiniertes Verhalten aus. So ist zum Beispiel nach einem Zugriff auf ein Element hinter dem Ende eines Arrays jedes beliebige Programmverhalten möglich. Sicherheit ist in der Regel nicht absolut, so ist es zum Beispiel möglich in Java mittels des sogenannten Java Native Interface (JNI) beliebige C-Funktionen auszuführen, und auf diese Weise undefiniertes Verhalten innerhalb eines Java-Programms zu erzeugen. Von dynamischer Typprüfung im Gegensatz zu statischer Typprüfung ist bei sogenannten Skriptsprachen die Rede. Hier werden Operanden erst beim Ausführen einer Operation auf ihren Typ getestet. Wir werden im folgenden nur noch Sprachen mit statischer Typprüfung betrachten.

Explizit und implizit getypte Sprachen

Als explizit getypt bezeichen wir Sprachen in denen der Programmierer Programmelementen eplizit Typangaben zuordnet. Implizit getypte Sprachen sind in der Lage Typen von Ausdrücken und Funktionen durch Typinferenzmechanismen zu bestimmen. Hierbei wird nach den allgemeinsten Typen gesucht, mit denen ein Programm noch wohlgetypt ist. Java zwingt den Programmieren beispielsweise an sehr vielen Stellen zu expliziten Typangaben, wohingegen zum Beispiel in Haskell an fast allen Stellen auf Typangaben verzichtet werden kann. Trotzdem können Typangaben auch in Haskell helfen, bei komplexeren Programmen den Überblick zu bewahren.

Nominelle und strukturelle Typsysteme

Ein nominelles Typsystem liegt genau dann vor, wenn jedem Typ eindeutig ein einfacher Name zugeordnet werden kann. So kann man beispielsweise in Java an eine Methode die ein Argument vom Typ java.util.Map erwartet, nur Objekte von Typ java.util.Map (oder einem Subtyp) übergeben. Es ist nicht möglich ihr ein Objekt eines anderen Typs mitzugeben, auch wenn dieser exakt die gleiche Struktur (öffentliche Methoden und Attribute) wie java.util.Map hat. Nominelle Typsysteme werden in den meisten Programmiersprachen eingesetzt, weil sie einfache und effiziente Typprüfungen (insbesondere Laufzeittypprüfungen) möglich machen. In mathematischen Kalkülen wird hingegen fast ausschliesslich mit strukturellen Typsystemen gearbeitet. In einem solchen System ist der Name eines Typen (, falls er überhaupt einen hat) vollkommen belanglos. Es interessiert lediglich ob ein Typ die geforderte Struktur hat. Ab einer bestimmten Mächtigkeit können Typsystem nicht mehr rein nominell arbeiten. In der Regel ist hier bei parametriesierten Typen Schluss. So läßt sich beispielweise der Typ "java.util.Map <java.lang.String , java.util.ArrayList <java.lang.String>>" in einem rein-nominellen Typsystem nicht mehr darstellen. Wir werden uns im folgenden nur noch mit strukturellen Typsystemen befassen.