(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)