Type Theory

Bertrand Russell fand einen Fehler in der Mathematik (Russell's Paradox): "Enthält die Menge aller Mengen, die sich nicht selbst enthalten, sich selbst?" -> BOOM. Logik kaputt. Seine Lösung: Typen. Man darf nicht alles in einen Topf werfen. Es gibt "Zahlen". Es gibt "Mengen von Zahlen". Es gibt "Mengen von Mengen". Man darf die Ebenen nicht mischen. In der Informatik schützt uns das vor Abstürzen: "Du kannst nicht 'Hallo' durch 5 teilen." Type Theory ist der Beweis, dass ein Programm sinnvoll ist, bevor es läuft.

Merksatz: Ein Zweig der mathematischen Logik und Informatik, der Systeme klassifiziert, indem er Ausdrücken Typen zuweist, um logische Fehler (und Laufzeitfehler) zu verhindern.

Statische Typisierung: (Java, Rust, TypeScript). Der Compiler prüft die Typentheorie. String x = 5 -> roter Kringel.
Dynamische Typisierung: (Python, JS). Keine Typentheorie zur Compilezeit. Fehler passieren erst, wenn der User klickt ("undefined is not a function").

1. Curry-Howard-Isomorphismus

Der mind-blowing Moment für Informatiker. "Ein Programm ist ein Beweis." "Ein Typ ist eine logische Aussage (Theorem)." Wenn du eine Funktion f: A -> B schreiben kannst, hast du mathematisch bewiesen, dass aus Aussage A Aussage B folgt. Programme schreiben und Mathe beweisen ist exakt das Gleiche.

2. Dependent Types (Idris / Agda)

Die Zukunft. Typen, die von Werten abhängen. Array<Int, 5> (Ein Array mit genau 5 Zahlen). Wenn du versuchst, das 6. Element zu lesen, kompiliert das Programm nicht. Der Compiler verhindert "Index Out of Bounds" Fehler mathematisch.

1. Per-Martin-Löf und Intuitionistische Typentheorie

In der klassischen Mathematik gilt das "Gesetz vom ausgeschlossenen Dritten" ($A \lor \neg A$). Etwas ist entweder wahr oder falsch. Die Intuitionistische Typentheorie (MLTT) sagt: Eine Aussage ist nur wahr, wenn wir einen Beweis (ein Programm) dafür konstruieren können. Das ist die Basis für Sprachen wie Coq oder Lean, in denen Computerprogramme mathematische Theoreme beweisen. Microsoft hat z. B. Teile seines Kernels oder spezielle Krypto-Bibliotheken mathematisch verifiziert, indem sie diese in einer Typentheorie geschrieben haben, die keine logischen Fehler zulässt.

2. Hindley-Milner Algorithmus (HM)

Warum kann der Compiler in Haskell oder Rust Typen raten, während Java das oft nicht kann? Dank des Hindley-Milner-Algorithmus. Er findet den "allgemeinsten Typ" (Principal Type) eines Ausdrucks, ohne dass er explizit deklariert werden muss. Er löst im Grunde ein Gleichungssystem: "Wenn Funktion $f$ einen String zurückgibt und $x$ das Ergebnis von $f$ ist, dann MUSS $x$ ein String sein." HM ist der Goldstandard für Typ-Inferenz, stößt aber an seine Grenzen, sobald man extrem komplexe Dinge wie "Generics mit Constraints" oder "Subtyping" (OOP) hinzufügt.

3. Linear Types (Rust-Inspiration)

Eine neuere Entwicklung sind Linear Types. Normale Typentheorie erlaubt es, eine Variable beliebig oft zu nutzen (Copy). Linear Types erzwingen, dass ein Wert genau einmal benutzt werden muss. Das klingt nach einer Einschränkung, erlaubt aber geniale Optimierungen: Der Compiler weiß, dass eine Variable nach der Nutzung "tot" ist. Er kann den Speicher sofort freigeben, ohne einen Garbage Collector zu brauchen. Das "Ownership-Modell" von Rust ist eine direkte Anwendung dieser typentheoretischen Konzepte auf die Systemprogrammierung.