Théorie des types

Mathématiques constructives

Per Martin-Löf a proposé sa théorie des types intuitionniste comme fondement pour les mathématiques constructives. Les mathématiques constructives exigent que, pour démontrer « il existe un ${\displaystyle x}$ ayant la propriété ${\displaystyle P(x)}$ », on construise explicitement un certain ${\displaystyle x}$ ainsi qu’une preuve qu’il possède la propriété ${\displaystyle P}$. En théorie des types, l’existence est formulée au moyen du type somme dépendante, et une preuve de cette existence correspond à un terme de ce type.

Un exemple de démonstration non constructive est la preuve par contradiction. La première étape consiste à supposer que ${\displaystyle x}$ n’existe pas et à réfuter cette hypothèse par contradiction. On en déduit alors : « il n’est pas vrai que ${\displaystyle x}$ n’existe pas ». Dans une démarche classique, la dernière étape utilise la double négation pour conclure que ${\displaystyle x}$ existe. Les mathématiques constructives n’autorisent pas cette étape finale consistant à éliminer la double négation pour conclure à l’existence de ${\displaystyle x}$.

La plupart des théories des types proposées comme fondements sont constructives, y compris la majorité de celles utilisées par les assistants de preuve. Il est possible d’ajouter des éléments non constructifs à une théorie des types, que ce soit sous forme de règle ou d’hypothèse. Cela inclut notamment certains opérateurs sur les continuations, tels que call with current continuation. Toutefois, ces opérateurs ont tendance à rompre des propriétés souhaitables telles que la canonicité et la paramétricité.

Inférence de types

Article principal : Inférence de types

De nombreux programmes qui reposent sur la théorie des types (par exemple les assistants de preuve interactifs) réalisent également de l’inférence de types. Cela leur permet de sélectionner automatiquement les règles que l’utilisateur souhaite appliquer, tout en réduisant le nombre d’actions nécessaires de sa part.

Théorie des catégories

Bien que la motivation initiale de la théorie des catégories ait été très éloignée du fondationalisme, les deux domaines se sont révélés profondément liés. Comme l’écrit John Lane Bell :

« En réalité, les catégories peuvent elles-mêmes être considérées comme des théories des types d’un certain genre ; ce fait seul montre que la théorie des types est beaucoup plus étroitement liée à la théorie des catégories qu’à la théorie des ensembles. »

En bref, une catégorie peut être vue comme une théorie des types en considérant ses objets comme des types (ou sortes), c’est-à-dire : « En gros, une catégorie peut être vue comme une théorie des types dépouillée de sa syntaxe. » Plusieurs résultats importants s’ensuivent :

• les catégories cartésiennes fermées correspondent au λ-calcul typé (Lambek, 1970) ;
• les C-monoïdes (catégories munies de produits, d’exponentielles et d’un objet non terminal) correspondent au λ-calcul non typé (observation indépendante de Lambek et Dana Scott vers 1980) ;
• les catégories localement cartésiennes fermées correspondent aux théories des types de Martin-Löf (Seely, 1984).

Cette interaction, connue sous le nom de logique catégorique, fait l’objet de recherches actives depuis lors ; on peut citer, par exemple, la monographie de Jacobs (1999).

Théorie homotopique des types

La théorie homotopique des types cherche à combiner la théorie des types et la théorie des catégories. Elle met l’accent sur les notions d’égalité, en particulier les égalités entre types. Elle se distingue principalement de la théorie des types intuitionniste par sa manière de traiter le type d’égalité.

En 2016, la théorie des types cubiques (cubical type theory) a été proposée ; il s’agit d’une version de la théorie homotopique des types qui admet une normalisation.

Termes atomiques

Les types les plus fondamentaux sont appelés atomes, et un terme dont le type est un atome est appelé terme atomique. Parmi les termes atomiques courants en théorie des types, on trouve :

• les nombres naturels, notés avec le type ${\displaystyle nat}$;
• les valeurs booléennes ( ${\displaystyle true/false}$ ), notées avec le type ${\displaystyle bool}$ ;
• les variables formelles, dont le type peut varier.

Par exemple, les éléments suivants peuvent être des termes atomiques :

• ${\displaystyle 42:nat}$
• ${\displaystyle true:bool}$
• ${\displaystyle x:nat}$
• ${\displaystyle y:bool}$

Termes fonctionnels

En plus des termes atomiques, la plupart des théories des types modernes permettent également des fonctions. Les types fonctionnels introduisent un symbole de flèche et sont définis inductivement : si ${\displaystyle \sigma }$ et ${\displaystyle \tau }$ sont des types, alors la notation ${\displaystyle \sigma \to \tau }$ désigne le type d’une fonction qui prend un paramètre de type ${\displaystyle \sigma }$ et renvoie un terme de type ${\displaystyle \tau }$. Les types de cette forme sont appelés types simples.

Certains termes peuvent être déclarés directement comme ayant un type simple, comme le terme ${\displaystyle add}$, qui prend deux nombres naturels en séquence et renvoie un nombre naturel :

${\displaystyle \mathrm {add}$ :{\mathsf {nat}}\to ({\mathsf {nat}}\to {\mathsf {nat}})}

Strictement parlant, un type simple n’autorise qu’une seule entrée et une seule sortie. Une lecture plus correcte du type ci-dessus est donc que ${\displaystyle add}$ est une fonction qui prend un nombre naturel et renvoie une fonction du type ${\displaystyle nat\to nat}$. Les parenthèses indiquent que ${\displaystyle add}$ n’a pas le type ${\displaystyle (nat\to nat)\to nat}$ qui correspondrait à une fonction prenant en entrée une fonction sur les naturels et renvoyant un naturel.

La convention veut que la flèche soit associative à droite, de sorte que les parenthèses peuvent être omises dans le type de ${\displaystyle add}$.

Lambda termes

De nouveaux termes fonctionnels peuvent être construits à l’aide d’expressions lambda, et sont appelés lambda termes. Ces termes sont également définis inductivement : un terme lambda a la forme ${\displaystyle (\lambda v.t)}$, où ${\displaystyle v}$ est une variable formelle et ${\displaystyle t}$ est un terme. Son type s’écrit ${\displaystyle \sigma \to \tau }$, où ${\displaystyle \sigma }$ est le type de ${\displaystyle v}$ et ${\displaystyle \tau }$ est le type de ${\displaystyle t}$[.

Le lambda terme suivant représente une fonction qui double un nombre naturel donné :

${\displaystyle (\lambda x.add{\text{ }}x{\text{ }}x):nat\to nat}$

La variable est ${\displaystyle x}$, et (comme l’indique implicitement le type du lambda terme) elle doit être de type ${\displaystyle nat}$. Le terme ${\displaystyle add{\text{ }}x{\text{ }}x}$ est de type ${\displaystyle nat}$, ce que l’on obtient en appliquant deux fois la règle d’inférence pour l’application de fonctions. Ainsi, le lambda terme est de type ${\displaystyle nat\to nat}$ ce qui signifie qu’il s’agit d’une fonction prenant en argument un nombre naturel et renvoyant un nombre naturel.

Un lambda terme est souvent appelé fonction anonyme, car il ne possède pas de nom. Cette notion de fonction anonyme apparaît dans de nombreux langages de programmation.

Application de fonction

La puissance des théories des types réside dans la spécification de comment les termes peuvent être combinés entre eux par des règles d'inférence. Les théories des types qui ont des fonctions ont également des règles d'inférence pour l'application de fonction : si ${\displaystyle t}$ est un terme de type ${\displaystyle \sigma \rightarrow \tau }$, et ${\displaystyle s}$ est un terme de type ${\displaystyle \sigma }$, alors l'application de ${\displaystyle t}$ à ${\displaystyle s}$, souvent notée ${\displaystyle (t\ s)}$, est de type ${\displaystyle \tau }$. Par exemple, si on sait que ${\displaystyle 0:nat,\ 1:nat}$ et ${\displaystyle 2:nat}$, alors on peut déduire le type des fonctions suivantes grâce à la règle d'application :

• ${\displaystyle (add\ 1):nat\rightarrow nat}$
• ${\displaystyle ((add\ 2)\ 0):nat}$

• ${\displaystyle ((add\ 1)((add\ 2)\ 0)):nat}$

Les parenthèses indiquent l'ordre des opérations. Cependant, par convention, l'application de fonction est associative à gauche : on peut donc retirer des parenthèses lorsque c'est approprié. Dans les exemples ci-dessus, on pourrait retirer les parenthèses des deux premiers, et simplifier le troisième en ${\displaystyle add\ 1(add\ 2\ 0):nat}$.

Réduction

Les théories des types autorisant les lambda termes sont également munies de règles d'inférence appelées ${\displaystyle \beta }$-réduction et ${\displaystyle \eta }$-réduction. Elles généralisent la notion d'application de fonction aux lambda termes. On les écris symboliquement:

• ${\displaystyle (\lambda v.t)\ s\rightarrow t[v:=\ s]}$ (${\displaystyle \beta }$-réduction).
• ${\displaystyle (\lambda v.tv)\rightarrow t}$, si ${\displaystyle v}$ n'est pas une variable libre dans ${\displaystyle t}$ (${\displaystyle \eta }$-réduction).

La première réduction décris comment évaluer un lambda terme : si une lambda expression ${\displaystyle (\lambda v.t)}$ est appliquée à un terme ${\displaystyle s}$, on remplace toutes les occurrences de ${\displaystyle v}$ dans ${\displaystyle t}$ par ${\displaystyle s}$. La seconde réduction rend explicite la relation entre lambda expression et types de fonction : si ${\displaystyle (\lambda v.tv)}$ est un lambda terme, alors nécessairement, t est une fonction car elle est appliquée à ${\displaystyle v}$. Ainsi, la lambda expression est équivalente à t, car les deux prennent un unique argument, et applique à ${\displaystyle t}$.

par exemple, let terme suivant peut être ${\displaystyle \beta }$-réduit.

${\displaystyle (\lambda x.add\ x\ x)\ 2\rightarrow add\ 2\ 2}$

Dans les théories des types qui définissent la notion d'égalité pour les types et les termes, il y des règles d'inférence qui leur sont associées : ${\displaystyle \beta }$-égalité et ${\displaystyle \eta }$-égalité.

Le type vide

Le type vide n'a pas de terme. On le note souvent ${\displaystyle \perp }$ ou ${\displaystyle 0}$. Il peut être utilisé pour démontrer qu'un type est habité, c'est-à-dire qu'il existe un terme ayant ce type : si pour un type ${\displaystyle a}$, il est consistent de dériver un fonction de type ${\displaystyle a\rightarrow \bot }$, alors ${\displaystyle a}$ n'est pas habité, c'est-à-dire qu'aucun terme n'a le type ${\displaystyle a}$.

Le type unit

Le type unité a exactement 1 terme canonique. On le note souvent ${\displaystyle \top }$ ou ${\displaystyle 1}$, et ${\displaystyle *}$ le terme canonique. Il est également utilisé pour démontrer qu'un type est habité : si pour un type ${\displaystyle a}$, il est consistent de dériver un fonction de type ${\displaystyle \top \rightarrow a}$, alors ${\displaystyle a}$ est habité.

Le type booléen

Le type booléen a exactement 2 termes canoniques. Il est souvent noté ${\displaystyle bool}$ ou ${\displaystyle \mathbb {B} }$ ou ${\displaystyle 2}$. Les termes canoniques sont ${\displaystyle true}$ et ${\displaystyle false}$.

Entiers naturels

Les entiers naturels sont généralement implémentés dans le style de l'arithmétique de Peano : il y un terme canonique ${\displaystyle 0:nat}$ pour zéro, et les entiers strictement positifs sont une succession d'application de la fonction successeur ${\displaystyle S:nat\rightarrow nat}$.

Type produit

Le type produit, noté ${\displaystyle \times }$, dépend de deux types, et ses termes sont souvent écris comme des couple ${\displaystyle (s,t)}$. Le couple ${\displaystyle (s,t)}$ est de type ${\displaystyle \sigma \times \tau }$, où ${\displaystyle \sigma }$ est le type de ${\displaystyle s}$ et ${\displaystyle \tau }$ celui de ${\displaystyle t}$. Chaque type produit est généralement définis avec des fonctions de destruction ${\displaystyle first:\sigma \times \tau \rightarrow \sigma }$ et ${\displaystyle second:\sigma \times \tau \rightarrow \tau }$.

• ${\displaystyle first\ (s,t)}$ renvoie ${\displaystyle s}$
• ${\displaystyle second\ (s,t)}$ renvoie ${\displaystyle t}$

Le type produit est également utilisé pour les concepts de conjonction logique et d'intersection.

Type somme

Le type somme, noté ${\displaystyle +}$ ou ${\displaystyle \sqcup }$. Dans les langages de programmation, les types sommes peuvent être associés aux types algébriques. Chaque type ${\displaystyle \sigma \sqcup \tau }$ est généralement défini avec des constructeurs ${\displaystyle left:\sigma \rightarrow (\sigma \sqcup \tau )}$ et ${\displaystyle right:\tau \rightarrow (\sigma \sqcup \tau )}$, qui sont injectives, et une fonction de destruction ${\displaystyle match:(\sigma \rightarrow \rho )\rightarrow (\tau \rightarrow \rho )\rightarrow \rho }$

• ${\displaystyle match\ f\ g\ (left\ x)}$ renvoie ${\displaystyle f\ x}$

• ${\displaystyle match\ f\ g\ (right\ y)}$ renvoie ${\displaystyle g\ y}$

Le type somme est utilisé pour les concept de disjonction logique et d'union.

Produits et sommes

Avec le polymorphisme, les fonctions d'éliminations peuvent être définies génériquement pour tous les types produits comme ${\displaystyle first:\forall \sigma \tau .\sigma \times \tau \rightarrow \sigma }$ et ${\displaystyle second:\forall \sigma \tau .\sigma \times \tau \rightarrow \sigma }$.

• ${\displaystyle first\ (s,t)}$ renvoie ${\displaystyle s}$
• ${\displaystyle second\ (s,t)}$ renvoie ${\displaystyle t}$

De même, les constructeurs des types sommes peuvent être définies pour tous les types des éléments d'un type somme comme ${\displaystyle left:\forall \sigma \tau .\sigma \rightarrow (\sigma \sqcup \tau )}$ et ${\displaystyle right:\forall \sigma \tau .\tau \rightarrow (\sigma \sqcup \tau )}$, qui sont injectives, et la fonction d'élimination peut être défini comme ${\displaystyle match:\forall \sigma \tau \rho .(\sigma \rightarrow \rho )\rightarrow (\tau \rightarrow \rho )\rightarrow \rho }$ tel que

• ${\displaystyle match\ f\ g\ (left\ x)}$ renvoie ${\displaystyle f\ x}$

• ${\displaystyle match\ f\ g\ (right\ y)}$ renvoie ${\displaystyle g\ y}$

Produits et somme dépendantes

Deux types dépendants courant, les types produits et sommes dépendantes, permettent à la théorie d'encoder la logique intuitioniste BHK en agissant comme des équivalents des quantificateurs universels et existentiels; ceci est formalisé par la correspondance de Curry-Howard. Comme ils relient les produits et les sommes de la théorie des ensemble, ils sont souvent notés avec les symboles ${\displaystyle \Pi }$ et ${\displaystyle \Sigma }$, respectivement.

Les types sommes sont utilisés pour les paires dépendantes, où le deuxième type dépend de la valeur du premier terme. Ceci intervient naturellement en informatique lorsque des fonctions renvoient différents sortes de résultat en fonction de l'entrée. Par exemple, le type booléen est souvent défini avec une fonction d'élimination ${\displaystyle if}$, qui prend trois arguments et ce comporte comme suit :

• ${\displaystyle if\ true\ x\ y}$ renvoie ${\displaystyle x}$
• ${\displaystyle if\ false\ x\ y}$ renvoie ${\displaystyle y}$

Les définitions ordinaires du ${\displaystyle if}$ demandent que ${\displaystyle x}$ et ${\displaystyle y}$ est le même type. Si la théorie autorisent les types dépendant, alors il est possible de définir un type dépendant ${\displaystyle x:bool\vdash TF\ x:U\rightarrow U\rightarrow U}$ tel que

• ${\displaystyle TF\ true\ \sigma \ \tau }$ renvoie ${\displaystyle \sigma }$
• ${\displaystyle TF\ false\ \sigma \ \tau }$ renvoie ${\displaystyle \tau }$

Le type de ${\displaystyle if}$ peut alors être écrit comme ${\displaystyle \forall \sigma \tau .\Pi _{x:bool}.\sigma \rightarrow \tau \rightarrow TF\ x\ \sigma \ \tau }$

Le type identité

En poursuivant la notion de correspondance de Curry-Howard, le type identité est un type introduit pour refléter l'équivalence propositionnelle, s'opposant à l'équivalence syntaxique des assertions que la théorie des types donne déjà.

Un type identité nécessite deux termes du même type et s'écrit avec le symbole ${\displaystyle =}$. Par exemple, si ${\displaystyle x+1}$ et ${\displaystyle 1+x}$ sont des termes, alors ${\displaystyle x+1=1+x}$ est un type possible. Les termes canoniques sont créés avec une fonction de ${\displaystyle {\text{refl}}}$. Pour un terme ${\displaystyle t}$, ${\displaystyle {\text{refl}}\ t}$ retourne le terme canonique qui habite type ${\displaystyle t=t}$.

Les complexités de l'égalité dans la théorie des types en font un sujet de recherche actifs; la théorie des types homotopiques est un domaine de recherche notable qui traite principalement de l'égalité dans la théorie des types.

Les types inductifs

Les types inductifs constituent un modèle général permettant de créer une grande variété de types. En fait, tous les types décrits précédemment, et bien d'autres, peuvent être définis à l'aide des règles des types inductifs. Deux méthodes pour générer des types sont l'induction-récursion et l'induction-induction. Une méthode qui utilise uniquement des termes lambda est le codage de Scott.

Certains assistants de preuve, tels que Rocq (précédemment connu sous le nom de Coq) et Lean, sont basés sur le calcul des constructions inductives, qui est un calcul des constructions enrichi de types inductifs