Daten-abhängige Typen

(dependent types) - Typ ist anhängig von Daten,

in Agda (http://wiki.portal.chalmers.se/agda/)

data Nat : Set where 
    zero : Nat ; suc  : Nat -> Nat
Vec : Nat -> Set -> Set
vHead : {X : Set}->(n : Nat)->Vec (suc n) X -> X
transpose : {m n : Nat}{X : Set} 
   -> Vec m (Vec n X) -> Vec n (Vec m X)

• höhere statische Sicherheit
• Typkorrektheit nicht entscheidbar (Halteproblem!)
• Programmierer muß Typ v. Bezeichnern beweisen
• ähnlich in Coq http://coq.inria.fr/