Système F - System F

Le système F , également connu sous le nom de ( Girard-Reynolds ) calcul lambda polymorphe ou calcul lambda de second ordre , est un calcul lambda typé qui diffère du calcul lambda simplement typé par l'introduction d'un mécanisme de quantification universelle sur les types. Le système F formalise ainsi la notion de polymorphisme paramétrique dans les langages de programmation , et forme une base théorique pour des langages tels que Haskell et ML . Le système F a été découvert indépendamment par le logicien Jean-Yves Girard (1972) et l' informaticien John C. Reynolds (1974).

Alors que le calcul lambda simplement typé a des variables s'étendant sur des termes et des classeurs pour eux, System F a en plus des variables s'étendant sur des types , et des classeurs pour eux. A titre d'exemple, le fait que la fonction d'identité puisse avoir n'importe quel type de la forme A → A serait formalisé dans le système F comme le jugement

${\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha }$

où est une variable de type . La majuscule est traditionnellement utilisée pour désigner les fonctions au niveau du type, par opposition à la minuscule qui est utilisée pour les fonctions au niveau de la valeur. (L'exposant signifie que le x lié est de type ; l'expression après les deux points est le type de l'expression lambda qui le précède.) ${\style d'affichage \alpha }$${\style d'affichage \Lambda }$${\style d'affichage \lambda }$${\style d'affichage \alpha }$${\style d'affichage \alpha }$

En tant que système de réécriture de termes , le Système F est fortement normalisant . Cependant, l' inférence de type dans System F (sans annotations de type explicites) est indécidable. Sous l' isomorphisme de Curry-Howard , le système F correspond au fragment de logique intuitionniste du second ordre qui n'utilise que la quantification universelle. Le système F peut être considéré comme faisant partie du cube lambda , avec des calculs lambda typés encore plus expressifs, y compris ceux avec des types dépendants .

Selon Girard, le « F » du système F a été choisi par hasard.

Règles de saisie

Les règles de typage du Système F sont celles du calcul lambda simplement typé avec en plus les éléments suivants :

${\displaystyle {\frac {\Gamma \vdash M{\mathbin {:}}\forall \alpha .\sigma }{\Gamma \vdash M\tau {\mathbin {:}}\sigma [\tau /\alpha ]}}}$ (1)

${\displaystyle {\frac {\Gamma ,\alpha ~{\text{type}}\vdash M{\mathbin {:}}\sigma }{\Gamma \vdash \Lambda \alpha .M{\mathbin {:} }\forall \alpha .\sigma }}}$ (2)

où sont les types, est une variable de type, et dans le contexte indique qu'elle est liée. La première règle est celle de l'application, et la seconde est celle de l'abstraction. ${\displaystyle \sigma ,\tau }$${\style d'affichage \alpha }$${\displaystyle \alpha ~{\text{type}}}$${\style d'affichage \alpha }$

Logique et prédicats

Le type est défini comme : , où est une variable de type . Cela signifie : est le type de toutes les fonctions qui prennent en entrée un type α et deux expressions de type α, et produisent en sortie une expression de type α (notez que nous considérons comme associative à droite .) ${\displaystyle {\mathsf {Booléen}}}$${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$${\style d'affichage \alpha }$${\displaystyle {\mathsf {Booléen}}}$${\style d'affichage \to }$

Les deux définitions suivantes pour les valeurs booléennes et sont utilisées, étendant la définition des booléens d'Église : ${\displaystyle \mathbf {T} }$${\displaystyle \mathbf {F} }$

${\displaystyle \mathbf {T} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}x}$

${\displaystyle \mathbf {F} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}y}$

(Notez que les deux fonctions ci-dessus nécessitent trois - et non deux - arguments. Les deux derniers devraient être des expressions lambda, mais le premier devrait être un type. Ce fait se reflète dans le fait que le type de ces expressions est : le quantificateur universel liant le correspond au liant l'alpha dans l'expression lambda elle-même. Notez également que c'est un raccourci pratique pour , mais ce n'est pas un symbole du système F lui-même, mais plutôt un "méta-symbole". De même, et sont aussi "méta-symboles", raccourcis pratiques, des "assemblages" du Système F (au sens de Bourbaki ) ; sinon, si de telles fonctions pouvaient être nommées (au sein du Système F), alors il n'y aurait pas besoin de l'appareil expressif lambda capable de définir des fonctions de manière anonyme et pour le combinateur à virgule fixe , qui contourne cette restriction.) ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$${\displaystyle {\mathsf {Booléen}}}$${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$${\displaystyle \mathbf {T} }$${\displaystyle \mathbf {F} }$

Ensuite, avec ces deux termes, on peut définir quelques opérateurs logiques (qui sont de type ) : ${\style d'affichage \lambda }$${\displaystyle {\mathsf {Booléen}}\rightarrow {\mathsf {Booléen}}\rightarrow {\mathsf {Booléen}}}$

${\displaystyle {\begin{aligned}\mathrm {AND} &=\lambda x^{\mathsf {Booléen}}\lambda y^{\mathsf {Booléen}}{.}x\,{\mathsf {Booléen} }\,y\,\mathbf {F} \\\mathrm {OU} &=\lambda x^{\mathsf {Booléen}}\lambda y^{\mathsf {Booléen}}{.}x\,{\ mathsf {Booléen}}\,\mathbf {T} \,y\\\mathrm {NOT} &=\lambda x^{\mathsf {Booléen}}{.}x\,{\mathsf {Booléen}}\, \mathbf {F} \,\mathbf {T} \end{aligné}}}$

Notez que dans les définitions ci-dessus, est un argument de type to , spécifiant que les deux autres paramètres qui sont donnés à sont de type . Comme dans les encodages Church, il n'y a pas besoin d'une fonction IFTHENELSE car on peut simplement utiliser des termes bruts comme fonctions de décision. Cependant, si l'on en fait la demande : ${\displaystyle {\mathsf {Booléen}}}$${\style d'affichage x}$${\style d'affichage x}$${\displaystyle {\mathsf {Booléen}}}$${\displaystyle {\mathsf {Booléen}}}$

${\displaystyle \mathrm {IFTHENELSE} =\Lambda \alpha .\lambda x^{\mathsf {Booléen}}\lambda y^{\alpha }\lambda z^{\alpha }.x\alpha yz}$

ça ira. Un prédicat est une fonction qui renvoie une valeur typée. Le prédicat le plus fondamental est ISZERO qui renvoie si et seulement si son argument est le chiffre d'Église 0 : ${\displaystyle {\mathsf {Booléen}}}$${\displaystyle \mathbf {T} }$

${\displaystyle \mathrm {ISZERO} =\lambda n^{\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }{.}n\,{\mathsf {Boolean}}\ ,(\lambda x^{\mathsf {Booléen}}{.}\mathbf {F} )\,\mathbf {T} }$

Structures du système F

Le système F permet aux constructions récursives d'être intégrées de manière naturelle, liée à celle de la théorie des types de Martin-Löf . Les structures abstraites (S) sont créées à l'aide de constructeurs . Ce sont des fonctions typées comme :

${\displaystyle K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S}$.

La récursivité se manifeste quand elle - même apparaît dans l'un des types . Si vous avez de ces constructeurs, vous pouvez définir le type de comme : ${\style d'affichage S}$${\displaystyle K_{i}}$${\style d'affichage m}$${\style d'affichage S}$

${\displaystyle \forall \alpha .(K_{1}^{1}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\dots \rightarrow (K_{1}^{m}[\alpha /S ]\rightarrow \dots \rightarrow \alpha )\rightarrow \alpha }$

Par exemple, les nombres naturels peuvent être définis comme un type de données inductif avec des constructeurs ${\style d'affichage N}$

${\displaystyle {\mathit {zéro}} :\mathrm {N} }$

${\displaystyle {\mathit {succ}}:\mathrm {N} \rightarrow \mathrm {N} }$

Le type System F correspondant à cette structure est . Les termes de ce type comprennent une version dactylographiée des chiffres de l' Église , dont les premiers sont : ${\displaystyle \forall \alpha .\alpha \to (\alpha \to \alpha )\to \alpha }$

{{{1}}}${\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x}$

{{{1}}}${\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx}$

{{{1}}}${\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)}$

{{{1}}}${\displaystyle \Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))}$

Si nous inversons l'ordre des arguments curry ( c'est-à-dire, ), alors le nombre d'église pour est une fonction qui prend une fonction f comme argument et renvoie la ^ième puissance de f . C'est-à-dire qu'un chiffre d'église est une fonction d'ordre supérieur - il prend une fonction à un seul argument f et renvoie une autre fonction à un seul argument. ${\displaystyle \forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }$${\style d'affichage n}$${\style d'affichage n}$

Utilisation dans les langages de programmation

La version du système F utilisée dans cet article est un calcul explicitement typé ou de style Church. Les informations de typage contenues dans les λ-terms rendent la vérification de type simple. Joe Wells (1994) a réglé un « problème ouvert embarrassant » en prouvant que la vérification de type est indécidable pour une variante de style Curry du Système F, c'est-à-dire qui manque d'annotations de typage explicites.

Le résultat de Wells implique que l' inférence de type pour le système F est impossible. Une restriction du système F connue sous le nom de " Hindley-Milner ", ou simplement " HM ", possède un algorithme d'inférence de type simple et est utilisée pour de nombreux langages de programmation fonctionnels à typage statique tels que Haskell 98 et la famille ML . Au fil du temps, alors que les restrictions des systèmes de types de style HM sont devenues apparentes, les langages ont progressivement évolué vers des logiques plus expressives pour leurs systèmes de types. GHC, un compilateur Haskell, va au-delà de HM (à partir de 2008) et utilise le système F étendu avec une égalité de type non syntaxique ; les fonctionnalités non-HM dans le système de types d' OCaml incluent GADT .

L'isomorphisme de Girard-Reynolds

Dans la logique intuitionniste du second ordre, le lambda calcul polymorphe du second ordre (F2) a été découvert par Girard (1972) et indépendamment par Reynolds (1974). Girard a prouvé le théorème de représentation : que dans la logique des prédicats intuitionniste du second ordre (P2), les fonctions des nombres naturels aux nombres naturels qui peuvent être prouvés totaux, forment une projection de P2 dans F2. Reynolds a prouvé le théorème d'abstraction : que chaque terme de F2 satisfait une relation logique, qui peut être intégrée dans les relations logiques P2. Reynolds a prouvé qu'une projection de Girard suivie d'un plongement de Reynolds forment l'identité, c'est-à-dire l' isomorphisme de Girard-Reynolds .

Système F _ω

Alors que le système F correspond au premier axe du cube lambda de Barendregt , le système F _ω ou le lambda calcul polymorphe d'ordre supérieur combine le premier axe (polymorphisme) avec le deuxième axe ( opérateurs de type ); c'est un système différent, plus complexe.

Système F _ω peut être définie sur une famille inductivement des systèmes, où l' induction est basé sur les types autorisés dans chaque système:

• ${\style d'affichage F_{n}}$ types de permis :
  • ${\displaystyle \star }$ (le genre de types) et
  • ${\displaystyle J\Rightarrow K}$où et (le genre de fonctions de types à types, où le type d'argument est d'ordre inférieur)${\displaystyle J\in F_{n-1}}$${\displaystyle K\in F_{n}}$

A la limite, nous pouvons définir le système comme étant ${\displaystyle F_{\omega }}$

• ${\displaystyle F_{\omega }={\underset {1\leq i}{\bigcup }}F_{i}}$

Autrement dit, F _ω est le système qui permet à des fonctions de types de types où l'argument (et suite) peut être de tout ordre.

Notez que bien que F _w impose aucune restriction à l' ordre des arguments dans ces applications, ne limite l' univers des arguments en faveur de ces applications: ils doivent être des types plutôt que des valeurs. Le système F _ω n'autorise pas les mappages de valeurs en types ( types dépendants ), bien qu'il autorise les mappages de valeurs en valeurs ( abstraction), les mappages de types en valeurs ( abstraction) et les mappages de types en types ( abstraction au niveau des types ) ${\style d'affichage \lambda }$${\style d'affichage \Lambda }$${\style d'affichage \lambda }$

Voir également

• Types existentiels - les contreparties quantifiées existentiellement des types universels
• System F _{< :} — étend le système F avec le sous-typage
• Système U

Remarques

Les références

Lectures complémentaires

• Pierce, Benjamin (2002). "V Polymorphism Ch. 23. Types universels, Ch. 25. Une implémentation ML du système F" . Types et langages de programmation . Presse MIT. p. 339-362, 381-388. ISBN 0-262-16209-1.

Liens externes

• Résumé du Système F par Franck Binard.
• System F _ω : le cheval de bataille des compilateurs modernes par Greg Morrisett