Théorie des types - Définition

La théorie des types est une branche de la logique mathématique qui a pour principales caractéristiques que tout objet (terme, fonction, ensemble) y a un type et que les entités ne peuvent se combiner qu'en respectant des règles de "typage".

Une première théorie des types (dite "ramifiée") a été créée par Bertrand Russell pour résoudre les paradoxes logiques, comme celui du menteur et ceux de la théorie des ensembles ; lourde d'emploi, elle a d'abord été simplifiée par Ramsey et ensuite supplantée par les théories de Zermelo-Frankel et NF de Quine (voir [1]), et aussi reconsidérée pour des objets plus élémentaires après la découverte du lambda-calcul et de la logique combinatoire. Bien que ces théories soient cohérentes dans leurs versions originelles, qui sont non typées, il est intéressant d'en étudier des formulations avec types.

Dans ces derniers cas, les entités mathématiques sont construites à l'aide de fonctions, 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 :

• les théories des ensembles qui, suivant l'intuition de Russell, classent les ensembles en différents types,
• 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,
• la linguistique, à travers le concept de catégorie syntaxique.