Begriff
Dependent Types
Warum wichtig?
Dieser Begriff ist ein Knoten im SengakujiWorks-Wissensnetz. Nutze Level 0 für die erste Einordnung, Level 1 für Praxis, Level 2 für technische Struktur und Level 3 für Grenzen, Fallstricke und Expertenkontext.
In Java hast du List.
Der Typ weiß nicht, wie lang die Liste ist.
list.get(10) -> Laufzeitfehler (IndexOutOfBounds).
Dependent Types erlauben Typen, die von Werten abhängen.
List <int, 5> (Eine Liste von Integers mit Länge 5).
Funktion append:
Nimmt List<n> und List<m>.
Gibt zurück List<n+m>.
Wenn du versuchst, get(10) auf einer List<5> aufzurufen, gibt es einen Compiler-Fehler.
"5 ist nicht größer als 10".
Die Logik wandert in das Typ-System.
Merksatz: Ein Typensystem, in dem Typen von Werten abhängen können (z. B. "Array der Länge n"), was es ermöglicht, komplexe Invarianten und Korrektheitseigenschaften zur Kompilierzeit zu prüfen.
Sprachen wie Idris, Agda, Lean.
Code sieht aus wie Haskell, aber mit Mathe im Typ.
vadd : Vect n a -> Vect n a -> Vect n a.
(Addiere zwei Vektoren, aber nur, wenn sie exakt gleich lang n sind).
Compiliert nicht, wenn Längen unterschiedlich sein könnten.
1. Proofs are First Class
Mit Dependent Types ist 2 + 2 = 4 ein Typ.
Der Wert Refl (Reflexivity) ist der Beweis.
Man kann Funktionen schreiben, die Beweise als Argumente nehmen.
safeDiv : (x : Int) -> (y : Int) -> (Not (y = 0)) -> Int.
Du kannst erst dividieren, wenn du einen Beweis lieferst, dass y nicht Null ist.
2. Termination
Damit der Compiler Typen prüfen kann ("Ist n+m das Gleiche wie m+n?"), muss er Rechnungen ausführen. Wenn diese Rechnungen in eine Endlosschleife gehen, hängt der Compiler. Deshalb verlangen Dependent Type Sprachen meistens, dass alle Funktionen terminieren (keine Endlosschleifen).
1. П-Types & Σ-Types
Mathematisch basieren Dependent Types auf zwei Säulen:
- Π-Types (Dependent Product): Verallgemeinerung von Funktionen. Der Ergebnistyp
Bhängt vom Wert des Argumentsxab. Notation:(x : A) -> B(x). Beispiel: Eine Funktion, die eine Zahlnnimmt und einen Vektor der Längenzurückgibt. - Σ-Types (Dependent Sum): Verallgemeinerung von Paaren. Der Typ des zweiten Elements hängt vom Wert des ersten Elements ab. Notation:
(x : A) ** B(x). Beispiel: Ein Paar bestehend aus einer Zahlnund einem Vektor der Längen. Das ist die Basis für "Existenz-Beweise" (Es existiert ein n, sodass...).
2. The Universe Hierarchy
Da Typen nun Werte sind, stellt sich die Frage: "Welchen Typ hat ein Typ?".
In der naiven Mengenlehre führt das zur Russellschen Antinomie.
Dependent-Type-Systeme nutzen daher eine Hierarchie von Universen (Type 0 : Type 1 : Type 2 ...).
Das verhindert Paradoxien, macht aber das Programmieren komplexer (Universe Polymorphism), da man manchmal Funktionen schreiben muss, die über "alle Universen hinweg" funktionieren. In der Produktion (Idris) versteckt der Compiler dies oft hinter dem Keyword Type, prüft aber im Hintergrund die Konsistenz.
3. Elaborator & Unification
Das Herz eines Dependent-Type-Compilers ist der Elaborator.
Da der User oft nicht alle Typ-Details explizit hinschreiben will (zu viel Rauschen), nutzt der Compiler Unifikation. Er versucht zu "raten", welcher Wert für ein Loch (_) eingesetzt werden muss, damit die Gleichungen im Typ-System aufgehen.
Production-Challenge: Wenn die Unifikation fehlschlägt, bekommt man Fehlermeldungen, die oft hunderte Zeilen lang sind und mathematische Terme enthalten, die der User nie geschrieben hat. Das "Zähmen" des Elaborators ist die größte Hürde für die Benutzerfreundlichkeit dieser Sprachen.
Quick-Check
Warum hat Java das nicht?
Zu komplex. Typ-Prüfung wird unentscheidbar (außer man schränkt die Sprache ein). Und Fehlermeldungen sind gruselig ("Cannot unify (n+1) with m").Zukunft?
Haskell bekommt langsam Features (Liquid Haskell). Rust hat Const Generics ([T; N]). Wir bewegen uns langsam darauf zu.Vorteil?
"If it compiles, it works." Wirklich. Bugs wie Buffer Overflows sind mathematisch unmöglich.