Typsysteme

Typsysteme sind formale Disziplinen, die Programmausdrücke nach den Arten von Werten klassifizieren, die sie berechnen, wodurch breite Fehlerklassen ausgeschlossen werden, bevor ein Programm ausgeführt wird.

Definition

Ein Typsystem ist eine handhabbare syntaktische Methode zum Nachweis der Abwesenheit bestimmter Programmverhaltensweisen, indem Ausdrücke gemäß den Arten von Werten klassifiziert werden, die sie berechnen.

Scope

Dieser Bereich umfasst die Theorie und das Design von Typsystemen: statische versus dynamische Typisierung, parametrischen und Ad-hoc-Polymorphismus, Subtyping, Typinferenz und fortgeschrittene Systeme wie abhängige und substrukturelle Typen. Er behandelt die Typsicherheit (type soundness), die Beziehung zwischen Typen und Logik über die Curry-Howard-Korrespondenz und wie Typisierungsdisziplinen Ausdrucksstärke gegen Garantien und Entscheidbarkeit abwägen.

Sub-topics

• dependent and substructural types
• polymorphism and generics
• static and dynamic typing
• type inference

Core questions

• Welche Garantien bietet ein Typsystem, und was ist Typsicherheit (type soundness)?
• Wie erhöhen Polymorphismus und Subtyping die Ausdrucksstärke, ohne die Sicherheit zu opfern?
• Können Typen automatisch inferiert werden, und wann ist die Inferenz entscheidbar?
• Wie weit können Typen reichhaltige Programmeigenschaften bis hin zu vollständigen Spezifikationen kodieren?

Key theories

Typsicherheit (type soundness) durch Progress und Preservation

Wrights und Felleisens syntaktischer Ansatz beweist die Typsicherheit eines Typsystems, indem er feststellt, dass wohltypisierte Programme nicht stecken bleiben: Typen bleiben während der Auswertung erhalten, und wohltypisierte Terme können immer Fortschritte machen.

Typologie von Polymorphismus und Abstraktion

Cardelli und Wegner organisieren den Raum der Typisierungskonzepte und unterscheiden parametrischen und Ad-hoc-Polymorphismus, Inklusion (Subtyping) und Datenabstraktion innerhalb eines einheitlichen Rahmens.

Typentheorie als Grundlage der Programmiersprache

Harper entwickelt eine einheitliche Statik-und-Dynamik-Methodologie, in der Sprachmerkmale durch Typisierungs- und Auswertungsregeln definiert werden, wobei die Typentheorie als organisierende Grundlage für das Sprachdesign behandelt wird.

Clinical relevance

Typsysteme gehören zu den am weitesten verbreiteten formalen Methoden: Sie fangen Fehler zur Kompilierzeit ab, dokumentieren Schnittstellen, ermöglichen sicheres Refactoring und treiben Editor-Tools an. Fortschritte wie Generika, graduelle Typisierung und Ownership-Typen sind direkt in gängige Industriesprachen eingeflossen.

History

Typisierte Sprachen entstanden mit frühen Systemen wie Algol und dem einfach typisierten Lambda-Kalkül. Milners polymorphe Typinferenz (1978) bildete die Grundlage für ML; Girard und Reynolds entwickelten unabhängig voneinander System F für parametrischen Polymorphismus. Die Übersicht von Cardelli und Wegner aus dem Jahr 1985 systematisierte das Feld, und die Progress-and-Preservation-Methode (1994) wurde zur Standardtechnik für die Typsicherheit, die Pierce und Harper später in Lehrbüchern kanonisierten.

Debates

Statische versus dynamische Typisierung

Eine langjährige Debatte wägt die frühe Fehlererkennung und Dokumentation der statischen Typisierung gegen die Flexibilität und schnelle Iteration der dynamischen Typisierung ab, wobei die graduelle Typisierung als Versöhnung angeboten wird.

Key figures

• Benjamin Pierce
• Robert Harper
• Luca Cardelli
• Robin Milner
• Matthias Felleisen

Seminal works

• pierce2002
• harper2016
• cardelli1985
• wright1994

Frequently asked questions

Was bedeutet es, dass ein Typsystem sicher (sound) ist?

Typsicherheit (soundness) bedeutet, dass wohltypisierte Programme die Fehler, die das Typsystem verhindern soll, nicht aufweisen können. Dies wird in der Regel dadurch bewiesen, dass gezeigt wird, dass Typen während der Auswertung erhalten bleiben und dass wohltypisierte Programme niemals stecken bleiben.

Haben dynamisch typisierte Sprachen Typsysteme?

Sie verfügen über Typen und führen Laufzeit-Typüberprüfungen durch, aber es fehlt ihnen ein statisches Typsystem, das fehlerhaft typisierte Programme vor der Ausführung ablehnt; Typfehler treten stattdessen als Laufzeitfehler auf.