Système F

Les types du système F (notés ${\displaystyle A}$, ${\displaystyle B}$, ${\displaystyle C}$, etc.) sont formés à partir d'un ensemble de variables de types (notées ${\displaystyle \alpha }$, ${\displaystyle \beta }$, ${\displaystyle \gamma }$, etc.) à l'aide des trois règles de construction suivantes :

• (Variable de type) Si ${\displaystyle \alpha }$ est une variable de type, alors ${\displaystyle \alpha }$ est un type ;
• (Type flèche) Si ${\displaystyle A}$ et ${\displaystyle B}$ sont des types, alors ${\displaystyle A\to B}$ est un type ;
• (Type universel) Si ${\displaystyle \alpha }$ est une variable de type et ${\displaystyle B}$ un type, alors ${\displaystyle \forall \alpha ~B}$ est un type.

En résumé, les types du système F sont donnés par la grammaire BNF :

${\displaystyle A,B~~::=~~\alpha ~~|~~A\to B~~|~~\forall \alpha ~B.}$

Comme en lambda-calcul ou en calcul des prédicats, la présence d'un symbole mutificateur ${\displaystyle \forall }$ nécessite de distinguer les notions de variable libre et de variable liée, et d'introduire les mécanismes usuels de renommage permettant de travailler à ${\displaystyle \alpha }$-conversion près. Enfin, l'algèbre de types du système F est munie d'une opération de substitution similaire à celle du lambda-calcul, et l'on note ${\displaystyle B\{\alpha$ :=A\}} le type obtenu en remplaçant dans le type ${\displaystyle B}$ toutes les occurrences libres de la variable de type ${\displaystyle \alpha }$ par le type ${\displaystyle A}$.

Les termes (bruts) du système F (notés ${\displaystyle M}$, ${\displaystyle N}$, etc.) sont formés à partir d'un ensemble de variables de termes (notées ${\displaystyle x}$, ${\displaystyle y}$, ${\displaystyle z}$, etc.) à l'aide des cinq règles de construction suivantes :

• (Variable) Si ${\displaystyle x}$ est une variable de terme, alors ${\displaystyle x}$ est un terme ;
• (Abstraction) Si ${\displaystyle x}$ est une variable de terme, ${\displaystyle A}$ un type et ${\displaystyle M}$ un terme, alors ${\displaystyle \lambda x:A.M}$ est un terme ;
• (Application) Si ${\displaystyle M}$ et ${\displaystyle N}$ sont des termes, alors ${\displaystyle MN}$ est un terme ;
• (Abstraction de type) Si ${\displaystyle \alpha }$ est une variable de type et ${\displaystyle M}$ un terme, alors ${\displaystyle \Lambda \alpha .M}$ est un terme ;
• (Application de type) Si ${\displaystyle M}$ est un terme et ${\displaystyle A}$ un type, alors ${\displaystyle MA}$ est un terme.

En résumé, les termes (bruts) du système F sont donnés par la grammaire BNF :

${\displaystyle M,N~~::=~~x~~|~~\lambda x\,{:}\,A\,.\,M~~|~~MN~~|~~\Lambda \alpha \,.\,M~~|~~MA.}$

Les termes du système F incorporent deux mécanismes de liaison de variable : un mécanisme de liaison de variables de termes (par la construction ${\displaystyle \lambda x\,{:}\,A\,.\,M}$) et un mécanisme de liaison de variables de types (par la construction ${\displaystyle \Lambda \alpha \,.\,M}$), qui sont tous les deux pris en compte au niveau de la relation d'${\displaystyle \alpha }$-conversion. Ce double mécanisme donne naturellement lieu à deux opérations de substitution : une substitution de terme notée ${\displaystyle M\{x:=N\}}$, et une substitution de type notée ${\displaystyle M\{\alpha$ :=A\}} .

La présence d'un double mécanisme d'abstraction et d'application (abstraction/application de terme et abstraction/application de type) donne lieu à deux règles de ${\displaystyle \beta }$-réduction, dont l'union engendre par passage au contexte la relation de ${\displaystyle \beta }$-réduction en une étape du système F :

• ${\displaystyle (\lambda x\,{:}\,A\,.\,M)N\longrightarrow M\{x:=N\}}$ ;
• ${\displaystyle (\Lambda \alpha \,.\,M)A\longrightarrow M\{\alpha$ :=A\}} .

Comme pour le lambda-calcul pur, la ${\displaystyle \beta }$-réduction du système F est confluente (sur les termes bruts) et vérifie la propriété de Church-Rosser :

• (Confluence de la ${\displaystyle \beta }$-réduction) Si ${\displaystyle M\longrightarrow ^{*}M_{1}}$ et ${\displaystyle M\longrightarrow ^{*}M_{2}}$, alors il existe un terme ${\displaystyle M'}$ tel que ${\displaystyle M_{1}\longrightarrow ^{*}M'}$ et ${\displaystyle M_{2}\longrightarrow ^{*}M'}$ ;
• (Propriété de Church-Rosser) Pour que deux termes ${\displaystyle M_{1}}$ et ${\displaystyle M_{2}}$ soient ${\displaystyle \beta }$-convertibles, il faut et il suffit qu'il existe un terme ${\displaystyle M'}$ tel que ${\displaystyle M_{1}\longrightarrow ^{*}M'}$ et ${\displaystyle M_{2}\longrightarrow ^{*}M'}$.

On appelle contexte de typage (notation : ${\displaystyle \Gamma }$, ${\displaystyle \Gamma '}$, etc.) toute liste finie de déclarations de la forme ${\displaystyle x:A}$ (où ${\displaystyle x}$ est une variable de terme et ${\displaystyle A}$ un type) dans laquelle une variable de terme est déclarée au plus une fois.

Le système de types du système F est construit autour d'un jugement de typage de la forme ${\displaystyle \Gamma \vdash M:A}$ (« dans le contexte ${\displaystyle \Gamma }$, le terme ${\displaystyle M}$ a pour type ${\displaystyle A}$ »), qui est défini à partir des règles d'inférence suivantes :

• (Axiome) ${\displaystyle {\frac {}{\Gamma \vdash x:A}}}$ si ${\displaystyle (x:A)\in \Gamma }$ ;
• (${\displaystyle \to }$-intro) ${\displaystyle {\frac {\Gamma ,x:A\vdash M:B}{\Gamma \vdash \lambda x\,{:}\,A\,.\,M:A\to B}}}$ ;
• (${\displaystyle \to }$-élim) ${\displaystyle {\frac {\Gamma \vdash M:A\to B\quad \Gamma \vdash N:A}{\Gamma \vdash MN:B}}}$ ;
• (${\displaystyle \forall }$-intro) ${\displaystyle {\frac {\Gamma \vdash M:B}{\Gamma \vdash \Lambda \alpha \,.\,M:\forall \alpha ~B}}}$ si ${\displaystyle \alpha }$ n'a pas d'occurrence libre dans ${\displaystyle \Gamma }$ ;
• (${\displaystyle \forall }$-élim) ${\displaystyle {\frac {\Gamma \vdash M:\forall \alpha ~B}{\Gamma \vdash MA:B\{\alpha$ :=A\}}}} .

Les deux propriétés principales de ce système de types sont la propriété de préservation du type par ${\displaystyle \beta }$-réduction et la propriété de normalisation forte :

• (Préservation du type par réduction) Si ${\displaystyle \Gamma \vdash M:A}$ et si ${\displaystyle M\longrightarrow ^{*}M'}$, alors ${\displaystyle \Gamma \vdash M':A}$ ;
• (Normalisation forte) Si ${\displaystyle \Gamma \vdash M:A}$, alors ${\displaystyle M}$ est fortement normalisable.

La première de ces deux propriétés est une propriété purement combinatoire qui se démontre par une induction directe sur la dérivation de typage. En revanche, la propriété de normalisation forte du système F est une propriété dont la démonstration repose fondamentalement sur des méthodes non combinatoires, basées sur la notion de candidat de réductibilité.

Le système de type présenté dans la section précédente est explicite, ce qui veut dire de les informations sur le type des termes sont données à chaque étape. On dit aussi que c'est un système « à la Church ». Dans un tel système, vérifier qu'un terme est bien typé est très simple.

En 1994, Joe B. Wells a résolu une conjecture ancienne, qui répond à un problème plus général, à savoir que la vérification de type pour un variant « à la Curry » du système F (un système de type où les informations de type ne sont pas données) est indécidable[1]. Le résultat de Wells signifie que la reconstruction du type pour le système F n'est pas possible. Autrement dit, en système F, on ne peut pas avoir un mécanisme logiciel qui, comme en OCaml ou en Haskell, assigne un type à une fonction que le programmeur a entrée. Cependant dans ces langages, pour aller vers des systèmes de type qui englobent le système F, le programmeur doit fournir, ici ou là, des informations de type pour aider le logiciel à reconstruire le type du terme entier. Dans des langages comme Gallina (de Coq) ou Agda (en) qui contiennent une large extension du système F, la contribution du programmeur au typage est déterminante.

Le type des booléens est défini dans le système F par

• ${\displaystyle {\textbf {Bool}}~\equiv ~\forall \gamma \,(\gamma \to \gamma \to \gamma )}$

et les constantes ${\displaystyle {\textbf {true}}}$ et ${\displaystyle {\textbf {false}}}$ par :

• ${\displaystyle {\textbf {true}}~\equiv ~\Lambda \gamma \,.\,\lambda x,y\,{:}\,\gamma \,.\,x~:~{\textbf {Bool}}}$ ;
• ${\displaystyle {\textbf {false}}~\equiv ~\Lambda \gamma \,.\,\lambda x,y\,{:}\,\gamma \,.\,y~:~{\textbf {Bool}}}$.

On peut démontrer que les deux termes ci-dessus sont les deux seuls termes clos en forme normale de type ${\displaystyle {\textbf {Bool}}}$. Ainsi, le type de données ${\displaystyle {\textbf {Bool}}}$ capture effectivement la notion de booléen.

La construction 'if … then … else …' est définie par

• ${\displaystyle {\texttt {if}}_{C}~M~{\texttt {then}}~N_{1}~{\texttt {else}}~N_{2}~\equiv ~MCN_{1}N_{2}}$

où ${\displaystyle C}$ désigne le type d'élimination de la construction 'if ...', c'est-à-dire le type commun aux deux branches de la conditionnelle. Cette définition est correcte du point de vue du typage comme du point de vue calculatoire dans la mesure où :

• Dans tout contexte où le terme ${\displaystyle M}$ a le type ${\displaystyle {\textbf {Bool}}}$ et où les termes ${\displaystyle N_{1}}$ et ${\displaystyle N_{2}}$ ont le type ${\displaystyle C}$, la construction ${\displaystyle {\texttt {if}}_{C}~M~{\texttt {then}}~N_{1}~{\texttt {else}}~N_{2}}$ est bien typée et a pour type le type ${\displaystyle C}$ ;
• Si le terme ${\displaystyle M\,\!}$ se réduit sur ${\displaystyle {\textbf {true}}}$, alors la construction ${\displaystyle {\texttt {if}}_{C}~M~{\texttt {then}}~N_{1}~{\texttt {else}}~N_{2}}$ se réduit sur ${\displaystyle N_{1}\,\!}$ ;
• Si le terme ${\displaystyle M\,\!}$ se réduit sur ${\displaystyle {\textbf {false}}}$, alors la construction ${\displaystyle {\texttt {if}}_{C}~M~{\texttt {then}}~N_{1}~{\texttt {else}}~N_{2}}$ se réduit sur ${\displaystyle N_{2}\,\!}$.

Plus généralement, on peut définir un type fini ${\displaystyle E_{n}}$ à ${\displaystyle n}$ valeurs ${\displaystyle e_{1},\ldots ,e_{n}}$ en posant :

• ${\displaystyle E_{n}~\equiv ~\forall \gamma \,(\underbrace {\gamma \to \cdots \to \gamma } _{n}\to \gamma )}$ ;
• ${\displaystyle e_{i}~\equiv ~\Lambda \gamma \,.\,\lambda x_{1},\ldots ,x_{n}\,{:}\,\gamma \,.\,x_{i}}$ (pour tout ${\displaystyle 1\leq i\leq n}$).

Là encore, on peut démontrer que les termes ${\displaystyle e_{1},\ldots ,e_{n}}$ sont les seuls termes clos en forme normale de type ${\displaystyle E_{n}}$. L'opération de filtrage correspondant est définie par :

• ${\displaystyle {\texttt {match}}_{C}~M~{\texttt {with}}~e_{1}\mapsto N_{1}|\cdots |e_{n}\mapsto N_{n}~\equiv ~M\,C\,N_{1}\cdots N_{n}}$

(où ${\displaystyle C}$ désigne le type des branches de filtrage).

En particulier :

• ${\displaystyle E_{2}~\equiv ~\forall \gamma \,(\gamma \to \gamma \to \gamma )~\equiv ~{\textbf {Bool}}}$ (type des booléens) ;
• ${\displaystyle E_{1}~\equiv ~\forall \gamma \,(\gamma \to \gamma )~\equiv ~{\textbf {Unit}}}$ (type singleton) ;
• ${\displaystyle E_{0}~\equiv ~\forall \gamma \,\gamma ~\equiv ~{\textbf {Empty}}}$ (type vide).

Le type ${\displaystyle E_{0}}$ n'est habité par aucun terme clos en forme normale, et, d'après le théorème de normalisation forte, il n'est habité par aucun terme clos.

Soit ${\displaystyle A}$ et ${\displaystyle B}$ deux types. Le produit cartésien ${\displaystyle A\times B}$ est défini dans le système F par

• ${\displaystyle A\times B~\equiv ~\forall \gamma \,((A\to B\to \gamma )\to \gamma )}$

et la construction de couple par

• ${\displaystyle \langle M;N\rangle ~\equiv ~\Lambda \gamma \,.\,\lambda f\,{:}\,(A\to B\to \gamma )\,.\,f\,M\,N~:~A\times B}$ (si ${\displaystyle M:A\,\!}$ et ${\displaystyle N:B\,\!}$)

Comme pour les types énumérés, on peut démontrer que les seuls termes clos en forme normale de type ${\displaystyle A\times B}$ sont de la forme ${\displaystyle \langle M;N\rangle }$, où ${\displaystyle M}$ et ${\displaystyle N}$ sont des termes clos en forme normale de type ${\displaystyle A}$ et ${\displaystyle B}$, respectivement. Les fonctions de projection correspondantes sont données par

• ${\displaystyle {\textbf {fst}}~\equiv ~\Lambda \alpha ,\beta \,.\,\lambda p\,{:}\,(\alpha \times \beta )\,.\,p\,\alpha \,(\lambda x\,{:}\,\alpha \,.\,\lambda y\,{:}\,\beta \,.\,x)~:~\forall \alpha ,\beta \,(\alpha \times \beta \to \alpha )}$
• ${\displaystyle {\textbf {snd}}~\equiv ~\Lambda \alpha ,\beta \,.\,\lambda p\,{:}\,(\alpha \times \beta )\,.\,p\,\beta \,(\lambda x\,{:}\,\alpha \,.\,\lambda y\,{:}\,\beta \,.\,y)~:~\forall \alpha ,\beta \,(\alpha \times \beta \to \beta )}$

Ces fonctions vérifient naturellement les égalités ${\displaystyle {\textbf {fst}}\,A\,B\,\langle M;N\rangle =M}$ et ${\displaystyle {\textbf {snd}}\,A\,B\,\langle M;N\rangle =N}$.

La somme directe ${\displaystyle A+B}$ est définie par

• ${\displaystyle A+B~\equiv ~\forall \gamma \,((A\to \gamma )\to (B\to \gamma )\to \gamma )}$

Les habitants des types ${\displaystyle A}$ et ${\displaystyle B}$ sont plongés dans le type ${\displaystyle A+B}$ à l'aide des constructions

• ${\displaystyle {\textbf {inl}}(M)~\equiv ~\Lambda \gamma \,.\,\lambda f\,{:}\,(A\to \gamma )\,.\,\lambda g\,{:}\,(B\to \gamma )\,.\,f\,M~:~A+B}$ (si ${\displaystyle M:A\,\!}$)
• ${\displaystyle {\textbf {inr}}(M)~\equiv ~\Lambda \gamma \,.\,\lambda f\,{:}\,(A\to \gamma )\,.\,\lambda g\,{:}\,(B\to \gamma )\,.\,g\,M~:~A+B}$ (si ${\displaystyle M:B\,\!}$)

tandis que le filtrage des éléments de type ${\displaystyle A+B}$ est assuré par la construction

• ${\displaystyle {\texttt {match}}~N~{\texttt {with}}~{\textbf {inl}}(x)\mapsto M_{1}~|~{\textbf {inr}}(y)\mapsto M_{2}~\equiv ~N\,C\,(\lambda x\,{:}\,A\,.\,M_{1})\,(\lambda y\,{:}\,B\,.\,M_{2})}$

qui satisfait les égalités définitionnelles attendues.

Contrairement au produit cartésien, l'encodage de la somme directe dans le système F ne capture pas toujours la notion d'union disjointe, dans la mesure où il est possible, dans certains cas, de construire des termes clos en forme normale de type ${\displaystyle A+B}$ qui ne sont ni de la forme ${\displaystyle {\textbf {inl}}(M)}$ (avec ${\displaystyle M:A}$) ni de la forme ${\displaystyle {\textbf {inr}}(M)}$ (avec ${\displaystyle M:B}$).

Le type des entiers de Church est défini dans le système F par

• ${\displaystyle \mathbf {Nat} ~\equiv ~\forall \gamma \,(\gamma \to (\gamma \to \gamma )\to \gamma )}$

Chaque entier naturel ${\displaystyle n}$ est représenté par le terme

• ${\displaystyle {\bar {n}}~\equiv ~\Lambda \gamma \,\lambda x\,{:}\,\gamma \,.\,\lambda f\,{:}\,(\gamma \to \gamma )\,.\,\underbrace {f(\cdots (f} _{n}\,x)\cdots )~:~\mathbf {Nat} }$

Comme pour les booléens, le type ${\displaystyle \mathbf {Nat} }$ capture la notion d'entier naturel puisque tout terme clos de type ${\displaystyle \mathbf {Nat} }$ en forme normale est de la forme ${\displaystyle {\bar {n}}}$ pour un certain entier naturel ${\displaystyle n}$.

• ${\displaystyle |x|=x}$
• ${\displaystyle |\lambda x:A.M|=\lambda x.|M|}$
• ${\displaystyle |MN|=|M||N|}$
• ${\displaystyle |\Lambda \alpha .M|=|M|}$
• ${\displaystyle |MA|=|M|}$

• (Axiome) ${\displaystyle {\frac {}{\Gamma \vdash x:A}}}$ si ${\displaystyle (x:A)\in \Gamma }$
• (${\displaystyle \to }$-intro) ${\displaystyle {\frac {\Gamma ,x:A\vdash M:B}{\Gamma \vdash \lambda x.M:A\to B}}}$
• (${\displaystyle \to }$-élim) ${\displaystyle {\frac {\Gamma \vdash M:A\to B\quad \Gamma \vdash N:A}{\Gamma \vdash MN:B}}}$
• (${\displaystyle \forall }$-intro) ${\displaystyle {\frac {\Gamma \vdash M:B}{\Gamma \vdash M:\forall \alpha ~B}}}$ si ${\displaystyle \alpha }$ n'a pas d'occurrence libre dans ${\displaystyle \Gamma }$
• (${\displaystyle \forall }$-élim) ${\displaystyle {\frac {\Gamma \vdash M:\forall \alpha ~B}{\Gamma \vdash M:B\{\alpha$ :=A\}}}} .