Une première théorie des types a été créée par Bertrand Russell pour résoudre les paradoxes de la théorie des ensembles ; lourde d'emploi, elle a été supplantée par la théorie de Zermelo-Frankel avant d'être reconsidérée après la découverte du lambda-calcul.
En théorie des types, les entités mathématiques sont construites à l'aide de fonctionss, où chaque fonction a un type qui décrit le type de ses arguments et le type de la valeur retournée. Les entités sont bien formées lorsque les fonctions sont appliquées à des entités ayant le type que la fonction attend.
Le concept de type a plusieurs domaines d'applications :
- la logique pour laquelle on cherche à donner un contenu calculatoire aux propositions et aux démonstrations par la correspondance de Curry Howard,
- les langages de programmation, surtout les langages fonctionnels typés,
- les systèmes de démonstration sur ordinateur.
Voir aussi
