Typsysteme

Typsysteme bezeichnen in der Informatik formale Systeme, die jedem Ausdruck oder jeder Variable einen Typ zuweisen. Ziel ist es, die Korrektheit von Operationen sicherzustellen, Laufzeitfehler zu verhindern und Programme besser überprüfbar zu machen. Typen dokumentieren Absichten und ermöglichen Compile-Time- oder Run-Time-Checks sowie Optimierungen.

Man unterscheidet statische Typisierung, bei der Typinformationen bereits vor der Ausführung bekannt sind, von dynamischer Typisierung, bei der Typprüfungen zur Laufzeit erfolgen. Ebenso spricht man von starker Typisierung, die implizite Typumwandlungen tendenziell reduziert, und von schwacher Typisierung, bei der solche Umwandlungen häufiger stattfinden.

Type Checking (Typprüfung) kann explizit erfolgen, oder Typen können durch den Compiler automatisch abgeleitet werden (Typinferenz). Typing-Disziplinen umfassen nominale Typisierung (basierend auf Namensbeziehungen wie Vererbung) und strukturelle Typisierung (basierend auf der Struktur der Typen).

Wichtige Konzepte umfassen Polymorphismus, Generics bzw. parametrisierte Typen, Subtypisierung und Vererbung, Typkonstruktoren sowie hochrangige Typen. Fortgeschrittene Systeme schließen abhängige Typen ein, die Typen und Werte enger verknüpfen.

Praktische Beispiele sind Sprachen wie Haskell mit einem starken statischen Typsystem und Typinferenz, Java mit statischer, nominaler Typisierung und Generics, sowie Python mit dynamischer Typisierung und optionalen Typannotationen. Theoretisch bildet die Typtheorie die Grundlage der Typsysteme und erforscht formale Eigenschaften von Typen und deren Zuordnung zu Ausdrücken.