Une caractéristique en théorie des types et une famille de systèmes où les types peuvent dépendre de valeurs (termes), permettant aux types d'exprimer des spécifications précises, de relier données et preuves, et d'internaliser propositions comme types.

Principe

Types-comme-prédicats : un type peut être paramétré par une valeur (par ex. Vector n A) de sorte que le typage impose des invariants au niveau des valeurs ; la correspondance propositions‑types (Curry–Howard) est réalisée avec une expressivité accrue.

Démonstration

Définir un type de listes de longueur n comme List A n et écrire une fonction append : ∀n m. List A n → List A m → List A (n + m) ; le type garantit à la compilation que la longueur du résultat est la somme des longueurs des entrées.

Mauvaise application

Encoder directement dans les types des propriétés indécidables ou trop coûteuses (par ex. recours arbitraire à la recherche pendant le typage) sans précaution, ce qui peut rendre la vérification de types non terminante ou les programmes impraticables à écrire et maintenir.

Conséquence

Permet d'intégrer des spécifications riches dans les types de sorte que de nombreuses propriétés de correction sont vérifiées par le vérificateur de types, facilitant l'extraction de programmes à partir de preuves constructives et le développement de logiciels à haute assurance lorsqu'elles sont bien conçues.

Inversion

Des systèmes de types simples où les types sont indépendants des valeurs d'exécution (par ex. système simplement typé), qui renoncent à des spécifications expressives au profit d'un typage décidable et efficace.

Limite

S'applique quand la discipline de vérification des types supporte le calcul au niveau des valeurs et des contraintes de terminaison ; les types dépendants ne décident pas magiquement des propriétés sémantiques arbitraires et exigent souvent totalité/contrôles de terminaison et obligations de preuve.

Tension sémantique

Tension entre des types dépendants expressifs pouvant énoncer des invariants forts et le désir d'un typage décidable et efficace avec automatisation ; tension aussi entre l'usage des types dépendants pour des preuves et l'ergonomie pragmatique de la programmation.

Synthèse

Les types dépendants étendent le système de types pour que les types puissent parler des valeurs, transformant les types en spécifications précises et permettant aux preuves sur le comportement du programme de coexister avec le code ; ils échangent puissance expressive et capacité de vérification contre une complexité accrue dans le typage et le développement.