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 Rocq) 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 Rocq. 

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.

  • Portail de la logique
  • Portail de l'informatique théorique
Cet article est issu de Wikipédia. Sauf mention contraire, le texte est disponible sous licence Creative Commons Attribution-Share Alike 4.0. Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.