Abhängiger Typ

Ein abhängiger Typ (engl. dependent type) ist ein Typ, der von einem Wert (und nicht nur von einem anderen Typ wie bei den generischen Typen) abhängt. Ein Beispiel ist z.B. der Typ der reellen Vektoren mit 4 Elementen. Dieser hängt vom konkreten Wert 4 ab.

Bei Funktionen können kompliziertere Abhängigkeiten genutzt werden, um Programmierfehler zu vermeiden. Beispielsweise kann die Funktion zum Ermitteln des n-ten Elements einer Liste den folgenden Typ erhalten:

Integer[0..n-1] ✕ List<α, n> → α,

wobei Integer[0..n-1] die ganzen Zahlen zwischen 0 und n-1 einschließlich bezeichnet und List<α, n> die Listen mit dem Elementtyp α und der Länge n. Dann kann im Rahmen der Typprüfung sichergestellt werden, dass die angegebene Position zur Länge der Liste passt.


Quellen

http://en.wikipedia.org/wiki/Dependent_type
http://de.wikipedia.org/wiki/Generischer_Typ
http://www.informatik.uni-ulm.de/ki/Edu/Vorlesungen/Inferenzsysteme/WS0405/r06a.pdf