Mathématypes

En attendant de regarder à l’intérieur des entrailles d’un compilateur optimisant comme promis dans le précédent billet, faisons un petit intermède plus théorique mais qui offre une perspective nouvelle sur la programmation en général. En effet, ce blog parle de langages de programmation et de leurs paradigmes, et jusqu’ici nous avons vu une opposition assez nette entre tenants du tout orienté objet et partisans de la programmation fonctionnelle. Le débat entre les deux se place au niveau de l’ergonomie et de la facilité du développeur à utiliser l’un ou l’autre paradigme, mais est-ce l’unique manière de juger et comparer ces paradigmes ?

Attention, ce billet contient plus de mathématiques que les précédents. Néanmoins, il suffit de comprendre à quoi sert une démonstration pour saisir le sens du propos plus bas.

Un peu d’arithmétique

Commençons notre voyage par un peu d’arithmétique. Ceux qui ont fait un peu d’algèbre savent que pour toute variable \(\tau \) (prononcez tau), \(\tau \times(\tau + 1) = \tau \times \tau + \tau\). Nous allons montrer que ce résultat est aussi vrai si \(\tau \) est un type d’un langage fonctionnel.

Pour cela, il nous faut établir un lien entre les constructions du langage et les symboles mathématiques. Rappelons-nous que dans un langage fonctionnel, il y a deux sortes de types : les types « structure » comme dans un langage orienté objet, et les types « l’un ou l’autre » correspondant à une disjonction de cas. Dans le billet sur la programmation fonctionnelle, j’avais dit les types de cette dernière sorte étaient appelés types somme. Ici, nous allons décider d’associer les type somme avec le symbole mathématique « \(+\) ». Cette décision est techniquement arbitraire, mais nous allons voir que procéder ainsi permet de construire un tout cohérent.

Symétriquement, associons les types « structure » avec le symbole « \(\times\) » et appelons les les types produit. Nous avons maintenant établi un lien entre nos symboles mathématiques usuels et les sortes de type. Les opérations mathématiques correspondent donc aux opérations sur les types. De manière naturelle, les nombres vont donc correspondre aux types.

Passons sous silence le cas du 0 et demandons nous à quoi pourrait correspondre le type appelé « 1 ». Tout bêtement, c’est le type qui contient exactement un élément. En OCaml, ce type s’appelle unit et son unique élément est noté (). C’est un type assez prévisible, puisque si une valeur du programme est de type unit, cela ne peut être que (). Le type unit correspond à peu près au mal-nommé type void de Java et de C/C++ : en effet une fonction par définition mathématique retourne toujours une valeur, qui peut être de type unit dans les cas où l’on utilise void dans d’autres langages.

Passons maintenant au type noté « 2 ». C’est le type qui contient exactement deux éléments. Comment écrire en OCaml un type qui ne contient que deux éléments distincts ? Comme cela :

type two = First of unit | Second of unit

Il n’y a que deux valeurs de type two : First () et Second (). Or two est un type somme ! Ainsi, nous avons définit 2 comme \(1+1\)… Et ainsi de suite pour tous les autres nombres.

Maintenant, comment montrer que \(\tau \times(\tau + 1) = \tau \times \tau + \tau\) ? D’abord, donnons des noms à chaque membre de l’équation : A est \(\tau \times(\tau + 1)\), et B est \(\tau \times \tau + \tau\) . Il nous faut montrer que si on a une valeur de type A, alors on peut la transformer en une valeur de type B, et vice-versa. Nous ferons ici le premier sens de la démonstration, le second étant laissé en exercice.

Prenons une valeur de type A : elle est de la forme (x,y) car A est un type produit. Or le deuxième terme du produit est lui-même un type somme, donc nous avons deux cas : y peut soit être de type \(\tau\), ou bien de type unit. Si y est de type \(\tau\), alors (x,y) est de type \(\tau\times\tau\), qui est une des deux possibilités du type somme B. Si y est de type unit, alors on utilise juste x qui est de type \(\tau\), l’autre possibilité de B. Dans tous les cas, on peut reconstruire une valeur de type B à partir d’une valeur de type A.

Ainsi les types d’un langage fonctionnel peuvent se manipuler dans une certaine mesure comme des nombres avec des opérations usuelles, qui fonctionnent comme on pourrait s’y attendre. Mais à quoi cela sert-il de faire ce parallèle ?

Dualité des données

Cette approche devient plus intéressante lorsque l’on commence à parler des fonctions. Nous ne détaillerons pas ici la correspondance avec les objets mathématiques des fonctions informatiques, pour éviter de rentrer trop dans la technique. Néanmoins l’esprit reste le même qu’avant. Ce qui est intéressant, c’est d’observer qu’il existe deux manières différentes de représenter un agencement de données.

Pour cela, reprenons notre exemple de cafetières à poudre ou à dosettes. Dans un langage orienté objet, comme nous l’avons vu, il nous faut définir deux classes contenant chacune deux méthodes. Or avec un langage fonctionnel, on peut sans perte d’informations représenter le même agencement de données par deux fonctions prenant chacune un type somme correspondant aux cafetières. Dans les deux cas, il y a quatre informations importantes : comment faire du café et recharger la cafetière, selon que la cafetière est à dosette ou à poudre. Représentons les dans un tableau :

Dans une approche orienté objet, le type de la cafetière est en réalité \((f_1\times f_3)+(f_2\times f_4)\) : une cafetière est soit à dosette, soit à poudre et dans chaque cas on a les méthodes associées. Dans une approche fonctionnelle, ce type devient \((f_1 \odot f_2)\times(f_3 \odot f_4)\), c’est à dire les deux fonctions « faire du café » et « recharger », qui contiennent chacune les deux cas pour la cafetière. Ces deux approches correspondent à selon qu’on lit le tableau ci-dessus par les colonnes ou par les lignes.

Le symbole cabalistique \(\odot\) utilisé est une notation arbitraire qui signifie le fait de « réunir » deux fonctions qui ont le même ensemble d’arrivée mais pas le même ensemble de départ pour en faire une nouvelle à l’ensemble de départ plus grand. On ne rentrera pas dans le détail de la démonstration, mais il est possible de prouver, similairement à ce que l’on a fait au paragraphe précédent, que \((f_1 \odot f_2)\times(f_3 \odot f_4)=(f_1\times f_3)+(f_2\times f_4)\).

Ce qu’il faur retenir, c’est qu’il existe très souvent deux manières d’agencer des données dans un programme informatique. Ces deux manières correspondent mathématiquement à deux types d’opérations sur les types, qui sont les sommes et les produits de types. Sommes et produits sont deux facettes complémentaires, et il est avantageux de pouvoir voir des données sous l’un ou l’autre des facettes selon la situation.

Pour la diffusion des type somme

On touche là à ce qui fait la limite intrinsèque de la programmation orientée objet : elle contraint le développeur à ne voir ses données que sous une certaine facette, et toujours la même : celle des types produit. Cette contrainte est en réalité artificielle, même si elle semble au premier abord plus « naturelle » au développeur.

Prenons un parallèle un peu exagéré : se refuser à considérer autre chose que l’orienté objet revient à se contenter d’utiliser uniquement des nombres positifs en toutes situations. Un comptable peut faire ce choix, mais il est alors obligé d’utiliser des artifices pour soustraire ses dépenses de ces recettes, et est bien embêté lorsque les premières excèdent les dernières. Il comprend bien vite l’utilité des nombres négatifs, qui viennent en complément des nombres positifs.

De la même manière, les types somme sont le complément naturel des types produit, et n’inclure que l’un ou l’autre dans un langage de programmation est contre-productif. Au lieu d’inventer des mécanismes complexes d’héritage par classe abstraite pour simuler les disjonctions, il est bien plus facile et logique d’adopter un système de type inspiré de principes simples et cohérents qui nous sont inspirés par les mathématiques.

C’est pour cela que, depuis quelques années, les nouveaux langages de programmation qui apparaissent contiennent tous une implémentation de type somme : Rust, Swift, etc. Ceci est un bel exemple de l’influence des mathématiques qui petit à petit remettent de l’ordre dans des constructions décidées des décennies plus tôt de manière un peu arbitraire, mais qui ont définit un standard de facto.

Pour aller plus loin

• Ce billet est très largement inspiré du livre de Robert Harper, Practical Foundations for Programming Languages et du cours associé numéroté 15-312 qu’il enseigne à la Carnegie Mellon University.