Théorie des Types

Les mathématiques sont un monde passionnant mais parfois quelque peu complexe à appréhender à l’image du lambda calcul que je vous ai présenté dans mon dernier article. Que dire alors de la théorie des types que j’aborde dans cet article-ci ? Comme nous le verrons ci-après, il n’existe pas une mais plusieurs théories des types. Laissez-vous plonger dans l’univers des types à travers de nombreux exemples et cas d’application qui vous permettront de mieux comprendre le concept.

Les mathématiques sont un monde passionnant mais parfois quelque peu complexe à appréhender à l’image du lambda calcul que je vous ai présenté dans mon dernier article. Que dire alors de la théorie des types que j’aborde dans cet article-ci ? Comme nous le verrons ci-après, il n’existe pas une mais plusieurs théories des types. Laissez-vous plonger dans l’univers des types à travers de nombreux exemples et cas d’application qui vous permettront de mieux comprendre le concept.

Évoquer la théorie des types est quelque peu complexe, d’autant qu’il n’existe pas de théorie unique relative aux types mais bien plusieurs comme par exemple :

• La théorie du type intuitionniste de Per Martin-Löf
• La théorie des types homotopiques
• Le lambda calcul simplement typé

C’est par ce dernier que nous avons fait le choix d’introduire la notion de type. L’idée n’est pas de décrire une théorie du type précisément, mais plus de vous donner les moyens de comprendre les idées induites par les fondements de la programmation fonctionnelle et de vous plonger dans la littérature des mathématiques concernant ces théories.

Un peu d’histoire …

Bertrand Russell et Gottlob Frege

Le début du XXe siècle n’a pas été tendre avec les mathématiques ou plutôt avec l’idée des mathématiques absolues qui commençait à émerger à la fin du XIXe siècle. Bertrand Russell a lancé la première pierre dans la théorie des ensembles de Gottlob Frege avec son paradoxe homonyme. On peut le formuler de la façon suivante : L’ensemble des ensembles qui ne se contiennent pas eux-mêmes se contient-il ?. Notons E un tel ensemble, et supposons qu’il ne se contienne pas. Alors il fait partie des ensembles qui ne se contiennent pas eux-mêmes, c’est-à-dire lui-même. On aboutit donc à une contradiction et la supposition inverse nous amène rapidement au même genre de contradiction.

Pour la petite histoire, Frege apprit l’existence de ce paradoxe dans une lettre de Russell. Lettre qu’il reçut juste avant la publication du deuxième volume de Fundamentals of Arithmetics. Il a fallu alors une grande force de persuasion de la part de son éditeur pour que Frege accepte de publier ce second volume mais en y ajoutant une note en début d’ouvrage pour raconter ce qui lui arrivait (l’effondrement de la base de sa théorie).

En réalité, ce que Frege était en train d’expérimenter, c’est la preuve de l’inconsistance de sa théorie. La consistance d’une théorie en mathématiques à une définition précise s’applique si, à partir de cette dernière, on ne peut pas démontrer une proposition et son opposé. C’est en général sur ce point que reposent les paradoxes. C’est à cette époque qu’ils devinrent de véritables armes pour montrer l’inconsistance de théories pourtant à l’apparence triviale.

Ce qui est intéressant avec Bertrand Russell, c’est qu’il a lui-même apporté une solution à son propre paradoxe. Elle consiste à rendre l’énoncé même de ce paradoxe impossible et repose sur une notion de type. L’intuition de Russell était de créer ces types de façon à classer et à hiérarchiser les ensembles. Par exemple, dans le paradoxe de Russell, il existe deux types d’ensemble. Le premier concerne les ensembles qui ne contiennent pas d’ensemble. Le deuxième correspond aux types qui ne contient que des ensembles d’ensembles du premier type. Ainsi présenté, il est impossible de définir l’auto-appartenance présente dans le paradoxe de Russell et donc le paradoxe lui-même.

Mais cette théorie n’a pas vraiment séduit à cette époque. Beaucoup ont alors essayé de construire d’autres formes de théorie des ensembles. La plus utilisée aujourd’hui est la théorie ZFC, qui est la théorie Zermello Frankel à laquelle on ajoute l’axiome du choix. Cette théorie est particulièrement élaborée et difficile à maîtriser. Malgré sa popularité, elle n’est pas non plus exempte de toutes critiques comme par exemple, l’impossibilité de démontrer sa consistance en utilisant uniquement les objets de cette théorie. C’est une conséquence du deuxième théorème d’incomplétude de Gödel.

Alonso Church et le lambda calcul

Alonso Church a cependant eu utilisé la théorie des types ont et a ouvert de nouvelles voies avec la logique combinatoire et le lambda calcul (et réciproquement). Même si c’est deux théories sont intimement liées, nous allons nous intéresser à la seconde. La première version du lambda calcul de Church était incohérent pour des raisons liées au paradoxe de Kleene Rosser et au paradoxe de Richard. L’argumentation de ce point est assez complexe et utilise plusieurs arguments difficiles à maîtriser. On va le supposer admis mais le lien ci-dessus nous donne une argumentation.

Pour corriger cette incohérence, Alonso Church a introduit le lambda calcul simplement typé dans son article de 1940,“A formulation of the simple theory of types”. L’idée de formaliser les types avait déjà été proposée par Bertrand Russell. Formuler dans Principia Mathematica, elle a été développée afin de pouvoir répondre aux paradoxes qui ont submergé la théorie naïve des ensembles). Le temps a fourni à la théorie des types et à Alonso Church les arguments pour en faire une des théories les plus importantes du XXe siècle.

Les types

Nous avons tous une petite idée de ce qu’est un type, en particulier si on a déjà touché à un langage de programmation. Que nous apporte donc la théorie du type que l’intuition ne nous apporte déjà ? Commençons déjà par nous différencier du cas de la théorie des ensembles.

Théorie des ensembles vs théorie des types

Les théories des ensembles traitent de l’existence de ces ensembles et des interactions qu’ils ont entre eux. Les ensembles sont des collections de choses que l’on met les unes avec les autres. À cette fin, on utilise un système déductif employant la logique du premier ordre (basé sur les calculs de prédicat) déjà existant, afin de définir les axiomes sur lesquels construire une théorie particulière des ensembles (ZF, ZFC, etc.).

Les théories du type contiennent leurs propres systèmes déductifs. C’est-à-dire que les règles permettant de raisonner sont intrinsèques à la théorie à laquelle elles sont liées. Ces règles sont appelées des jugements.

Pour commencer, limitons-nous à l’idée que l’on veut simplement d’adjoindre à des éléments un type. Et comme les types contiennent un certain nombre de jugements, on a donc un certain nombre de règles de manipulation qui viennent avec ce type. Ici, les jugements sont équivalents au système de logique du premier ordre utilisé en théorie des types. Mais comme on l’a dit, c’est vraiment « livré » avec le modèle de type que l’on utilise.

Poursuivons et prenons un autre exemple simple : tout le monde a déjà manipulé le chiffre 1, il peut sembler évident qu’il s’agit d’un entier naturel. On peut interpréter cette affirmation comme « 1 fait partie de l’ensemble des entiers naturels ». L’inconvénient, c’est que cette affirmation est composée de deux parties. En effet, on peut parler du chiffre 1 sans parler de son appartenance aux entiers naturels. Dans un second temps, on considère l’appartenance de 1 aux entiers naturels. Il s’agit en tout cas du point de vue de la théorie des ensembles.

En théorie des types, on considérera plutôt la formulation afin de signifier que est du type . Il s’agit d’une affirmation insécable. En fait, on ne souhaite pas pouvoir parler d’un élément sans parler de son type dans ce cadre.

L’exemple de l’égalité entre membres d’un type

Une autre interprétation de cette relation peut paraître également assez déroutante, l’isomorphisme Curry Howard qui voit T comme un théorème et M comme une preuve de ce dernier. Une des conséquences de cet isomorphisme est que, pour démontrer un théorème, il suffit de montrer que le type correspondant est habité.

Cette interprétation est particulièrement importante car elle permet de mettre en avant des types qui ne sont pas forcément intuitifs. Prenons encore une fois un exemple : l’égalité entre membres d’un type. Considérons un type , et et ( en plus court : ). Montrer que et sont égaux revient à montrer que la proposition est vraie. Cela signifie que est un type que l’on notera  Montrez que la proposition est vraie revient à montrer que le type correspondant est habité. On parle alors d’égalité propositionnelle entre et .

Mais on a également besoin d’une notion d’égalité plus conventionnelle dans le sens où on peut la voir comme une égalité par définition. Elle se note :

En plus des types, Russell a introduit une notion d’ordre dans les types. On les formalise par les Univers notés . Il s’agit de types dont les éléments sont eux-mêmes des types. En fait, on utilise plutôt des univers placés de façon hiérarchique :

tel que : , .

En d’autres termes, est un élément de . Rappelons que Russell a créé cette construction afin d’éviter le paradoxe homonyme (cf. plus haut).

Quand il n’y aura pas d’ambiguïté sur la place dans cette hiérarchie, on notera plus simplement .

Lambda Calcul simplement typé

Anatolii nous a déjà introduit le lambda calcul dans une série de trois article que vous pouvez retrouver en suivant ces liens : l’histoire lambda calcul, Lambda-calcul : de la définition à la logique booléenne et Lambda calcul, nombres de Church et programmation fonctionnelle. Il s’agit maintenant d’introduire les types au sein des -abstractions. Dans ce cas, on parle de lambda calcul simplement typé. Dans le cadre de cette théorie, on notera parfois les lambda plutôt que simplement .

Pour cela, on se donne une variable x et une expression M, alors l’expression :

x.M,

définit une fonction lambda. Donc si x est du type A et M de type B, est une fonction du type . D’ailleurs, on pourra plutôt préciser cette expression de la façon suivante :

.

Les mêmes règles de calcul ne s’appliquent que dans le cas du lambda calcul non typé comme dans cet article de Anatolii sur les lambda. Rappelons juste les noms des quatre règles :

• -conversion
• la substitution
• -reduction
• -conversion

Il faut simplement prendre en compte le typage. Par exemple, la -reduction réduction s’écrit :

x:A.M M.

Mais pour cela, il faut que  soit de type A. Bien que les raisons paraissent évidentes, on vient d’appliquer intuitivement une règle de typage (nous reviendrons sur ce point plus tard quand nous parlerons des jugements).

En plus de fournir un moyen d’utiliser des fonctions dans le cadre de la théorie des types, elles définissent également de nouveaux types. Seulement former de nouveaux types n’est pas anodin et répond à des règles assez précises et parfois subtiles. Voyons donc comment cela fonctionne avec les -abstractions.

Formation des Types

Il existe quatre règles essentielles pour former un type.

Règle de formation

Il s’agit de donner les ingrédients utiles à la formation du type. Dans le cas des fonctions, étant donné deux types A et B, on peut former une fonction

Règle de construction (ou règle d’introduction)

Cette règle a pour but de définir comment créer un élément du type. Pour les fonctions, il s’agit des règles de construction des -abstractions elles-mêmes.

Règle d’élimination

On donne ici la règle qui permet de manipuler les éléments du type. Dans le cas de notre exemple, il s’agit de la règle de substitution.

Règle de calcul

Cette règle définit le lien entre les deux précédentes. Ou plus précisément comment la règle d’élimination agit sur la règle de construction. Dans le cas des lambda fonctions typées, il s’agit de la -réduction.

Du point de vue de la théorie des types, nous bénéficions donc des informations nécessaires pour manipuler les -abstractions. Ces règles sont également nécessaires pour définir tous les types que l’on souhaite.

On peut même en ajouter une optionnelle qui concerne l’unicité des éléments.

Règle d’unicité

Cette règle s’applique pour les éléments uniquement déterminés sous l’effet des règles définies plus haut.

Fonction de type dépendant (Dependant function type)

Pour commencer, nous allons définir des fonctions un peu particulières. Étant donné un type , une famille est une fonction de type . Clairement, il s’agit bien d’une fonction, mais d’un type un peu particulier. Pour chaque élément d’un type , on associe un élément de l’univers dans lequel il est défini. Autrement dit, cette fonction crée des types. C’est un constructeur de type paramétré par les éléments de .

Pour les développeurs, ce type de fonction n’est pas inconnu. Prenez n’importe quel type paramétrique, son constructeur est un constructeur de type. Pas dans le sens que l’on vient de définir, mais d’une façon très similaire tout de même. Mais dans ce cas, existe-t-il des fonctions exactement comme celles que l’on a définies ? La réponse est oui et elles sont même assez communes.

• Exemple 1 : la fonction qui a associe les vecteurs de ,
• Exemple 2 : la fonction qui a associe les mots de taille ,
• Exemple 3 : la fonction qui a associe …

On vient donc de définir de façon un peu formel le polymorphisme paramétrique. Quand on réfléchit au lambda que nous avons évoqué précédemment, on utilisait déjà ce type de polymorphisme dans le sens où on ne précisait sur les types que le fait que… ce soit des types. Mais il va falloir aller encore plus loin. On dispose d’un moyen simple de générer des familles de types. On veut maintenant être capable de définir des fonctions définies de façon suffisamment souple pour pouvoir ne la définir qu’une seule fois pour tous les types de la famille.

Si maintenant, on se donne un type , une famille est une fonction de type , on notera une fonction qui à associe un élément . Notez la différence avec une famille qui à un élément associe un type de .

De telles fonctions existent. Commençons simplement par le cas où . En d’autres termes, la famille est composée d’un seul type. Dans ce cas, est simplement une fonction de type . Les fonctions standards sont donc des cas particuliers de ces fonctions de type dépendant. Il est alors possible de considérer ces fonctions comme une généralisation de la notion de fonction.

On peut également définir de façon polymorphique la fonction identité. C’est-à-dire une fonction qui, quel que soit le type, renvoie l’élément passé en argument. En suivant ce que l’on vient de décrire, il est possible d’écrire sa définition de la façon suivante :

On peut donc en déduire le type de cette fonction :

J’ai mis un moment à comprendre les subtilités de ces deux équations. C’est certainement dû au fait que la notation est assez compacte et, comme souvent, le diable se cache dans les détails.

Ici, l’univers est utilisé comme source de dépendance de type. En effet, conformément à ce que nous avons défini plus haut, les univers sont des types dont les éléments sont d’autres types. Le type dépendant correspond à une fonction dont le domaine et le codomaine sont le type provenant de . Autrement dit, nous venons de définir une lambda polymorphe (le polymorphisme paramétrique bien connu des développeurs). Plus particulièrement dans notre cas, il s’agit de la fonction identité qui a été définie pour tous les types de l’univers .

Ce type de construction constitue réellement une des clefs de démonstration en théories des types. Grâce à elle, il est possible de construire des lambda qui vont nous permettre de vérifier les règles qui permettent de prouver le bien fondé des types (cf. ci-dessus).

Le type produit

Afin de mettre en application les dernières constructions dans le cadre de la définition d’un type, intéressons-nous au cas du type produit. Considérons et deux types de . Sans pertes de généralités, on peut dire qu’un type produit sur et que l’on notera  est une paire constituée d’un élément et de . Plus succinctement, on le notera .Comment justifier alors son existence ?

Règle de formation

Ce que nous venons d’écrire définit la règle de formation de la façon suivante : si et , alors on peut former .

Règle de construction (ou règle d’introduction)

Tout comme la règle de formation, on déduit immédiatement la règle de construction de notre définition de la façon suivante : soit et , alors je peux créer .

Règle d’élimination

Ici, il faut se demander d’abord ce que cela veut dire. Il s’agit de définir une règle de substitution de lorsque l’on est en situation de manipulation du type. Mais en réalité, dans ce cas, on va surtout chercher à manipuler ses éléments constitutifs, c’est-à-dire et . Étant donné que nous avons défini le type produit comme une paire de deux éléments, il est tout à fait possible de manipuler l’un et l’autre séparément. Voilà ce qui constitue la règle d’élimination.

Règle de calcul

Il faut garder en tête que l’on a défini notre règle d’élimination de façon à manipuler les éléments constitutifs de la paire. Il faut donc continuer sur cette voie et définir les fonctions sur . Étant donné une fonction , on peut définir une fonction où est , de la façon suivante :

En résumé, on construit les fonctions en appliquant d’abord la première composante de puis la seconde à une fonction du type .

Exemples de construction de fonction utilisant le type produit.

La règle d’élimination peut être retravaillée de façon à définir des fonctions de projection de chacune des coordonnées. Appelons , la projection qui va extraire le premier élément et celle sur le second élément.

Je ne suis pas certain que cette notation soit très standard, je préfère employer le nom que j’utilise dans mes codes parce qu’il y a un lien direct. J’espère aussi que cela facilitera un peu la lecture.

On obtient donc les types de fonctions :

Ce qui nous amène aux définitions suivantes :

Pour être utilisable avec les fonctions de type dépendant, la règle d’élimination doit être quelque peu généralisée. Pour aller plus loin, je vous recommande la lecture du livre Homotopy Type Theory

Conclusion

Il resterait encore beaucoup à dire mais il ne s’agit pas ici de rédiger un ouvrage mais plutôt d’amener un concept, de faire découvrir quelque chose qui paraît parfaitement trivial (les types). Si trivial que l’on n’a pas forcément cherché à les manipuler en tant qu’objet d’étude. Il relevait plutôt de l’ordre du naturel. En effet, qui pouvait douter que ?!!!! Et pourtant, les problèmes arrivent dès qu’on cherche à construire !!!!

J’imagine que certains d’entre vous se diront que les mathématiciens sont des gens qui aiment se compliquer la vie pour avoir envie d’écrire ce genre de choses. Après tout, le produit cartésien est complètement naturel !!!! Alors rappelez-vous Frege…L’approche « naturelle » aboutit rapidement à des paradoxes. C’est la raison pour laquelle je pense que Russell disait ceci :

« Les mathématiques peuvent être définies comme une science dans laquelle on ne sait jamais de quoi on parle, ni si ce qu’on dit est vrai. »

Personnellement, même avec une formation assez poussée en mathématiques, j’ai lutté pour comprendre le peu que je pense comprendre de cette théorie. Ce que j’ai appris, je le dois principalement au livre Homotopy Type Theory dont je me suis inspiré pour écrire cet article. Pour le lecteur, le premier chapitre présente bien les généralités de la théorie des types et va encore plus loin. Pour le lecteur plus aguerri (et peut-être un peu masochiste), le reste du livre (que je n’ai pas encore fini) est très intéressant et présente un tout autre point de vue sur les mathématiques telles que j’ai pu les pratiquer à l’université.

Références

• Aha! gotcha, Martin Gardner, 1982
• Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, 2013