Théorie des types

En mathématiques, logique et informatique, une théorie des types est une classe de systèmes formels, dont certains peuvent servir d'alternatives à la théorie des ensembles comme fondation des mathématiques. Ils ont été historiquement introduits pour résoudre le paradoxe d'un axiome de compréhension non restreint.

En théorie des types, il existe des types de base et des constructeurs (comme celui des fonctions ou encore celui du produit cartésien) qui permettent de créer de nouveaux types à partir de types préexistant. Une différence notable avec la théorie des ensembles est que chaque terme possède un type, ce qui est un jugement subjectif et non pas une proposition . En d'autres termes la question de savoir si un terme appartient ou non à un type n'est pas réputée objective.

Des types sont utilisés dans certains langages de programmation, ce qui permet d'éviter des bugs.

Toutefois, la théorie des types fait plus souvent références à l'étude des systèmes de types qui servent de fondation alternative aux mathématiques. Le λ-calcul typé d'Alonzo Church et ses extensions permettent de faire de la logique à différents ordres ; ainsi elles servent à formaliser le système F. Dans la même ligne, la théorie des types intuitionniste de Per Martin-Löf ainsi que le calcul des constructions inductif offrent d'autres perspectives. Ceux-ci sont notamment à la base d'Agda (en) ou de Coq qui sont des assistants de preuve.

Histoire

D'un point de vue de la théorie mathématique : les types ont été pour la première fois théorisés par Bertrand Russell comme réponse à sa découverte du paradoxe ébranlant la théorie naïve des ensembles de Gottlob Frege. Cette théorie des types est développée dans l'ouvrage Principia Mathematica de Russell et Whitehead. Elle permet de contourner le paradoxe de Russell en introduisant tout d'abord une hiérarchie de types, puis en assignant un type à chaque entité mathématique. Les objets d'un certain type ne peuvent être construits qu'à partir d'objets leur préexistant (situés plus bas dans la hiérarchie), empêchant ainsi les boucles infinies et les paradoxes de surgir et de casser la théorie.

Pour ce qui concerne le sous-domaine des mathématiques nommé la logique mathématique — mais c'est aussi très utile dans le domaine de l'informatique, dans des sous-domaines nommés théorie des grammaires, théorie de la compilation, et système de réécriture, voire plus récemment dans le domaine de la transcompilation — on utilise les types dans le cadre de la théorie des types.

Dans le langage courant, « théorie des types » est à comprendre dans le contexte des systèmes de réécriture. L'exemple le plus connu est le lambda calcul d'Alonzo Church. Sa Theory of Types a permis de passer du calcul non-typé originel, incohérent du fait du paradoxe de Kleene-Rosser (en), à un calcul correct. Church a démontré que ce système pouvait servir de fondement des mathématiques ; on le décrit comme une logique d'ordre supérieur.

D'autres théories des types marquantes sont la théorie des types intuitionniste de Per Martin-Löf qui est utilisée comme fondement dans certaines branches des mathématiques constructivistes et pour des assistants de preuve tels que Agda (en) ou Idris. Le calcul des constructions de Thierry Coquand et ses extensions sont utilisés notamment par Coq et Matita (en). Il s'agit d'une recherche active, comme le démontrent les récents développements en théorie homotopique des types.

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 puis supplantée par la théorie de Zermelo-Frankel en 1922 (socle axiomatique utilisé par tous les mathématiciens, l'autre théorie NF conçue par Quine en 1937 et perfectionnée en NFU en 1969 par Ronald Jensen n'étant pas utilisée par les mathématiciens malgré les possibilités simplificatrices qu'elle offre, voir New Foundations), 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.

Applications

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 ;
• la théorie des modèles, où un type est un ensemble de formules particulier ;
• 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.

Voir aussi

Articles connexes

• Type (informatique)
• Format de données
• Caml, Haskell
• Agda (en), Coq, Idris, Matita (en)
• Analyse dimensionnelle