vignette|Représentation schématique de la transmission des méthodes d'une classe abstraite à une classe dérivée. 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 propositionQui peut être énoncée dans le langage de la théorie et possiblement démontrée dans le système de la théorie.. 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' ou de Rocq 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 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 , à 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 ou Idris. Le calcul des constructions de Thierry Coquand et ses extensions sont utilisés notamment par Rocq et . 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 FoundationsLa notion de type reste latente dans ZF, via la hiérarchie cumulative, et dans NF, via la notion de stratification.), 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

Fondements mathématiques Le premier assistant de preuve informatique, appelé Automath, utilisait la théorie des types pour encoder les mathématiques dans un ordinateur. Martin-Löf a développé spécifiquement la théorie intuitionniste des types afin d'encoder l'ensemble des mathématiques et d'en faire un nouveau fondement pour la discipline. Des recherches sont encore en cours concernant les fondements mathématiques basés sur la théorie homotopique des types.

Les mathématiciens travaillant en théorie des catégories éprouvaient déjà des difficultés à utiliser le fondement largement accepté de la théorie des ensembles de Zermelo–Fraenkel. Cela a conduit à des propositions telles que la théorie élémentaire de la catégorie des ensembles (ETCS) de Lawvere. La théorie homotopique des types s’inscrit dans cette continuité en s'appuyant sur la théorie des types. Les chercheurs explorent les liens entre les types dépendants (en particulier le type identité) et la topologie algébrique (notamment l’homotopie).

Assistants de preuve Article principal : Assistant de preuve

Une grande partie de la recherche actuelle sur la théorie des types est motivée par les assistants de preuve interactifs et les démonstrateurs automatiques de théorèmes. La plupart de ces systèmes utilisent une théorie des types comme fondement mathématique pour représenter les preuves, ce qui n’a rien de surprenant compte tenu du lien étroit entre la théorie des types et les langages de programmation :

LF est utilisé par Twelf, souvent pour définir d’autres théories des types ; de nombreuses théories des types relevant de la logique d'ordre supérieur sont utilisées par la famille de démonstrateurs HOL ainsi que par PVS ; la théorie computationnelle des types est utilisée par NuPRL ; le calcul des constructions et ses dérivés sont utilisés par Rocq (anciennement connu sous le nom Coq), Matita, et Lean ; UTT (Unified Theory of dependent Types de Luo) est utilisé par Agda, qui est à la fois un langage de programmation et un assistant de preuve.

De nombreuses théories des types sont prises en charge par LEGO et Isabelle. Isabelle prend également en charge d’autres fondements que les théories des types, tels que ZFC. Mizar est un exemple de système de preuve qui repose uniquement sur la théorie des ensembles.

Langages de programmation Toute analyse statique de programmes, comme les algorithmes de vérification de types utilisés lors de l’analyse sémantique d’un compilateur, entretient un lien avec la théorie des types. Un exemple emblématique est Agda, un langage de programmation qui utilise UTT (Unified Theory of dependent Types de Luo) pour son système de types.

Le langage de programmation ML a été développé pour manipuler des théories des types (voir LCF) et son propre système de types en a été fortement influencé.

Linguistique La théorie des types est également largement utilisée en sémantique formelle des langages naturels, en particulier dans la grammaire de Montague et ses prolongements. Les grammaires catégorielles et les grammaires de prégroupe utilisent notamment de manière extensive des constructeurs de types pour définir les types grammaticaux (nom, verbe, etc.) des mots.

La construction la plus courante considère les types de base (pour les individus) et (pour les valeurs de vérité), et définit l’ensemble des types de manière récursive comme suit :

si et sont des types, alors en est également un ; rien n’est un type en dehors des types de base et de ce qui peut être construit à partir d’eux selon la règle précédente.

Un type complexe est le type des fonctions qui associent à des entités de type des entités de type . On obtient ainsi des types tels que , interprétés comme des éléments de l’ensemble des fonctions des entités vers les valeurs de vérité, c’est-à-dire des fonctions indicatrices d’ensembles d’entités.

Une expression de type est une fonction d’ensembles d’entités vers des valeurs de vérité, c’est-à-dire une fonction indicatrice d’un ensemble d’ensembles. Ce dernier type est couramment considéré comme le type des quantificateurs du langage naturel, tels que tout le monde ou personne (Montague 1973 ; Barwise et Cooper 1981).

La théorie des types avec enregistrements (type theory with records) est un cadre de représentation de sémantique formelle qui utilise des enregistrements pour exprimer les types de la théorie des types. Elle a été utilisée en traitement automatique des langues, notamment en sémantique computationnelle et dans les systèmes de dialogue.

Sciences sociales Gregory Bateson a introduit une théorie des types logiques dans les sciences sociales ; ses notions de double contrainte (double bind) et de niveaux logiques sont fondées sur la théorie des types de Russell.

Logique Une théorie des types est une logique mathématique, c’est-à-dire un ensemble de règles d’inférence produisant des jugements. La plupart des logiques comportent des jugements affirmant « la proposition est vraie » ou « la formule est bien formée ». Une théorie des types, quant à elle, comporte des jugements qui définissent des types et les attribuent à un ensemble d’objets formels appelés termes. Un terme et son type sont souvent écrits ensemble sous la forme .

Termes En logique, un terme est défini récursivement comme un symbole constant, une variable, ou une application de fonction, c’est-à-dire un terme appliqué à un autre terme. Les symboles constants peuvent par exemple inclure le nombre naturel , la valeur booléenne ainsi que des fonctions comme la fonction successeur ou l’opérateur conditionnel . Ainsi, certains termes possibles sont et .

Jugements La plupart des théories des types comportent quatre jugements fondamentaux :

« est un type » « est un terme de type » « Le type est égal au type » « Les termes et , tous deux de type , sont égaux »

Les jugements peuvent découler d’hypothèses. Par exemple, on peut dire « en supposant que est un terme de type et que est un terme de type , il s’ensuit que est un terme de type ». De tels jugements sont formellement notés à l’aide du symbole taquet .

S’il n’y a aucune hypothèse, rien n’apparaît à gauche du symbole de tournant.

La liste des hypothèses figurant à gauche constitue le contexte du jugement. Les lettres grecques majuscules, telles que et , sont des notations couramment employées pour représenter une partie ou la totalité des hypothèses.

Les quatre types de jugements s’écrivent donc généralement de la manière suivante. +Notation formelle pour les jugementsDescription est un type (sous les hypothèses ) est un terme de type (sous les hypothèses )Le type est égal au type (sous les hypothèses )Les termes et , tous deux de type , sont égaux (sous les hypothèses ). Certains manuels utilisent un triple signe égal afin de souligner qu’il s’agit d’une égalité de jugements et donc d’une notion d’égalité extrinsèque. Les jugements garantissent que chaque terme possède un type. Le type détermine quelles règles peuvent être appliquées à un terme.

Règles d'inférence