Eine Eigenschaft der Typentheorie und Familie von Systemen, in denen Typen von Werten (Termen) abhängen können, wodurch Typen präzise Spezifikationen ausdrücken, Daten und Beweise verbinden und Prophezeiungen als Typen internalisiert werden können.

Prinzip

Typen als Prädikate: Ein Typ kann nach einem Wert parametriert sein (z. B. Vector n A), sodass das Typsystem Invarianten auf Wertezusichern erzwingt; die Curry–Howard-Korrespondenz wird dabei mit größerer Ausdruckskraft realisiert.

Demonstration

Definition eines Listentyps mit Länge n als List A n und Schreiben einer Funktion append : ∀n m. List A n → List A m → List A (n + m); der Typ stellt zur Kompilierzeit sicher, dass die Länge des Ergebnisses der Summe der Eingabelängen entspricht.

Fehlanwendung

Indezidierbare oder zu aufwändige Eigenschaften direkt in Typen zu kodieren (z. B. beliebige Suche während der Typprüfung), ohne Vorsicht walten zu lassen, wodurch die Typprüfung nicht terminieren oder Programme unpraktisch werden können.

Konsequenz

Ermöglicht das Einbetten reichhaltiger Spezifikationen in Typen, sodass viele Korrektheitseigenschaften vom Typrüfer geprüft werden; es erleichtert die Programmextraktion aus konstruktiven Beweisen und die Entwicklung hochzuverlässiger Software bei guter Gestaltung.

Umkehrung

Einfache Typensysteme, in denen Typen unabhängig von Laufzeitwerten sind (z. B. einfach typisierte Systeme), die ausdrucksstarke Spezifikationen zugunsten entscheidbarer und effizienter Typprüfung aufgeben.

Abgrenzung

Gilt, wenn die Typprüfungsdisziplin wertebenen Berechnungen und Terminierungskontrollen unterstützt; abhängige Typen entscheiden nicht willkürlich über semantische Eigenschaften und erfordern oft Totalitäts-/Terminierungsbedingungen und Beweisverpflichtungen.

Semantische Spannung

Spannung zwischen ausdrucksstarken abhängigen Typen, die starke Invarianten formulieren können, und dem Wunsch nach entscheidbarer, effizienter Typprüfung und Automatisierung; außerdem Spannung zwischen Verwendung abhängiger Typen für Beweise und pragmatischer Programmierergonomie.

Synthese

Abhängige Typen erweitern das Typsystem so, dass Typen über Werte sprechen können, wodurch Typen zu präzisen Spezifikationen werden und Beweise über Programmverhalten neben dem Code leben können; sie erkaufen erhöhte Ausdruckskraft und Verifikationsfähigkeit mit größerer Komplexität bei Typprüfung und Entwicklung.