Type dépendant

En Informatique et en Logique, un type dépendant est un type qui peut dépendre d'une valeur définie dans le langage typé.

Les langages Agda et Gallina (de l'assistant de preuve Coq) sont des exemples de langages à type dépendant.

Exemples

Les types dépendants permettent par exemple de définir le type des listes à n éléments.

Voici un exemple en Coq.

Inductive Vect (A: Type): nat -> Type :=
| nil: Vect A 0
| cons (n: nat) (x: A) (t: Vect A n): Vect A (S n).

Ainsi, Vect A n définit les listes à n éléments de type A et nil est une liste à 0 élément, et cons n s t est une liste à n + 1 éléments si t est une liste à n éléments.

v · m Types de données
Non interprétée	Bit Byte Trit Tryte Mot
Numérique	Bignum Complexe (en) Décimal (en) Virgule fixe Virgule flottante Entier Non signé (en) Intervalle Rationnel (en)
Texte brut	Caractère Chaîne de caractères
Pointeur	Adressage mémoire Physique Virtuelle Référence
Composite (en)	Type algébrique de données Généralisé Tableau Tableau associatif Classe Dépendant Égalité (en) Inductive (en) Liste Objet Métaobjet Option (en) Produit Enregistrement Ensemble (set) Vecteur Union (en) Disjointe
Autres	Booléen Type vide Collection Conteneur Type énuméré Exception Fonction Opaque (en) Type récursif Sémaphore Flux Top (en) Type class (en) Type unité Void
Articles liés	Type abstrait Structure de données Généricité Kind (en) Métaclasse Parametric polymorphism (en) Primitive data type (en) Interface Subtyping (en) Type constructor (en) Conversion de type Type system (en)