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.
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
