Wie werden Typen bewiesen — das TypeScript-Typsystem und die Curry–Howard-Korrespondenz

Zusammenfassung:

• Es wird eine Perspektive vorgestellt, die das Typsystem von TypeScript nicht nur als einfachen statischen Type Checker, sondern als Beweissystem der Logik interpretiert.
• Auf Basis der Curry–Howard-Korrespondenz (Type = Proposition, Program = Proof) wird konzeptionell erklärt, warum Typinferenz möglich ist.
• TypeScript-Funktionen wie Funktionstypen, Generics, bedingte Typen und Type Narrowing werden als Entsprechungen zu logischer Implikation, Allquantifizierung und Fallunterscheidung erläutert.
• Der Prozess des Type Checking wird nicht als Anwenden von Regeln, sondern als Überprüfung von Beziehungen zwischen Aussagen interpretiert.
• Der Fokus liegt weniger auf Implementierungsdetails als auf dem Designhintergrund und der mathematischen Struktur des TypeScript-Typsystems.

Detaillierte Zusammenfassung:

1. Hintergrund: Warum ist Typinferenz überhaupt möglich?
   In statisch typisierten Sprachen wird Typinferenz oft als Implementierungsfrage erklärt: „Wie probiert der Compiler aus, die Typen passend zu machen?“
   Dieser Artikel tritt einen Schritt zurück und fragt stattdessen, warum Typinferenz grundsätzlich möglich ist.
   Als Antwort wird die Perspektive vorgeschlagen, das Typsystem als Beweissystem der Logik zu betrachten.

2. Theoretische Grundlage: Curry–Howard-Korrespondenz
   Nach der Curry–Howard-Korrespondenz entspricht ein Typ (Type) einer Aussage (Proposition), und ein Programm (Program) entspricht dem Beweis (Proof) dieser Aussage.
   Aus dieser Sicht lässt sich Type Checking als der Prozess verstehen, zu verifizieren, ob ein Programm eine bestimmte Aussage erfüllt.

3. Entsprechung zwischen TypeScript-Funktionen und logischer Struktur
   Im Artikel werden die wichtigsten Funktionen von TypeScript wie folgt zugeordnet.

• Funktionstypen → logische Implikation (Implication)
• Generics → Allquantifizierung (Universal Quantification)
• Bedingte Typen / Type Narrowing → Fallunterscheidung (Case Analysis)
  So wird erklärt, warum bestimmte Typausdrücke natürlich wirken
  und warum manche Typen strukturell schwer auszudrücken sind.

4. Grenzen des Typsystems und Designentscheidungen
   Aus dieser Perspektive lassen sich die Einschränkungen und Grenzen von TypeScript nicht als „fehlende Funktionen“, sondern als Designentscheidungen zum Erhalt logischer Konsistenz verstehen.
   Der Artikel konzentriert sich eher darauf zu erklären, auf welcher Philosophie und welchem mathematischen Hintergrund das Typsystem aufbaut, als auf praktische Techniken oder Tricks.