Calendrier de l'Avent - Des théorèmes gratuits.

Aujourd’hui, un article qui ne porte pas sur les types dépendants ! Mais, restons tout de même sur un thème des systèmes de typage. Nous allons parler de types polymorphes, et de ce que l’on peut en déduire.

Cet article est basé sur le papier “Theorems for free !”, de Philip Wadler, mais je ne vais pas le résumer ici, ne serait-ce que par-ce que je ne le comprends pas assez. Mon but va être de vous donner une intuition pour le genre de théorèmes qui sont prouvés par ce papier.

Les types polymorphes…

Mettons que, un jour, vous ayez besoin d’utiliser une liste d’entiers, par exemple pour stocker des notes de contrôles. En OCaml, vous pourriez écrire un type pour représenter ces listes.

type int_list = IntNil | IntCons of int * int_list

Ici, on représente une liste d’entiers comme soit la liste vide, soit un entier suivi d’une liste d’entiers. Par exemple, on écrit la liste [15; 18; 17] comme IntCons (15, IntCons (18, IntCons (17, IntNil))).

Mais, si on voulait maintenant ajouter le nom des étudiant·e·s à la liste, on se heurte à un problème: il faut créer un nouveau type liste.

type string_int_list = StrIntNil
	| StrIntCons of (string * int) * string_int_list

L’idée est la même, et on peut représenter une liste avec, par exemple, StrIntCons (("Jean", 15), StrIntCons (("Pierre", 18), StrIntCons (("Paul", 17), StrIntNil))).

Mais, il est très embêtant de devoir écrire un nouveau type pour chaque sorte de liste que l’on souhaite utiliser, et toute fonction qui opère sur les listes devra être réécrite autant de fois. Ainsi, on souhaiterait pouvoir écrire le type une bonne fois pour toutes.

type 'a list = Nil | Cons of 'a * 'a list

Ici, on dit que, pour n’importe quel type ‘a, 'a list est une liste de ‘a. Nil représente la liste vide pour les listes de n’importe quels types, et Cons correspond à un ‘a suivi d’une liste de ‘a.

Par exemple, nos deux listes précédentes peuvent être écrites Cons (15, Cons (18, Cons (17, Nil))) et Cons (("Jean", 15), Cons (("Pierre", 18), Cons (("Paul", 17), Nil))), et sont de types int list et (string * int) list respectivement.

Maintenant, on peut écrire des fonctions qui opèrent sur des listes de n’importe quoi. Par exemple, on pourrait définir une fonction odds, qui prends une liste et en retourne une valeur sur 2.

let rec odds l = (* Odds prends 1 argument, l. *)
	match l with (* On regarde la valeur de l. *)
	| Cons (v, Cons (_, vs)) -> Cons (v, odds vs)
		(* Si la liste contient au moins deux valeurs,
		   on garde la première, on saute la deuxième,
		   et on continue à appliquer la fonction sur
		   le reste. *)
	| l -> l
		(* Sinon, que la liste ait une valeur ou zéro,
		   on la retourne sans y toucher. *)

Mais, quel est le type de cette fonction ? Eh bien, elle prend une liste d’éléments de type ‘a, peu importe le type ‘a, et la transforme en une autre liste de type ‘a. Elle est donc de type ∀ 'a, 'a list -> 'a list.

De même, on pourrait définir une fonction de tri, de type ∀ 'a, ('a -> 'a -> bool) -> 'a list -> 'a list. Ou encore, en sortant des listes pour un moment, on pourrait avoir une fonction qui retourne simplement son argument, de type ∀ 'a, 'a -> 'a.

…et ce qu’ils nous disent des fonctions.

Maintenant, concentrons-nous seulement sur les types, et pas sur la définition exacte de chaque fonction. Il s’avère que chaque type indique une propriété de toutes les fonctions de ce type. La méthode exacte de déduction de cette propriété est précisée dans l’article “Theorems for free !”, mais je vais ici essayer de vous donner une intuition pour ces propriétés.

Commençons par le plus simple, prenons le type ∀ 'a, 'a -> 'a. Intuitivement, comme elle ne sait rien du type ‘a, la fonction ne peut que retourner ce qu’on lui donne. Et, en effet, si f est de ce type, alors f x = x peut-importe la valeur de x. Le théorème donné dans le papier est un peu différent: il dit que, pour toute fonction g et valeur x, g (f x) = f (g x). Cependant, ces deux théorèmes sont équivalents.

Maintenant, prenons le type ∀ 'a, 'a list -> 'a list. Comme pour la fonction précédente, une fonction de ce type ne sait rien de ‘a, et ne peut donc pas manipuler la valeur des éléments de la liste, mais uniquement leur positions et leur nombre, indépendament de leurs valeurs. Par exemple, f de ce type pourrait inverser la liste, dupliquer tous les éléments, ou en supprimer un sur deux (on retrouve odds de tout-à-l’heure). Mais, elle ne pourrait pas garder les plus petits, ou retirer ceux présents en plusieurs exemplaires, car elle ne sait pas les comparer.
Dans le papier, ceci est exprimé en disant que, pour toute fonction g, si on note g* le fait d’appliquer g à tous les éléments d’une liste, pour toute liste l g* (f l) = f (g* l). L’idée est la même, la réorganisation des éléments ne dépend pas de leur valeur, donc on peut la changer avant ou après.

Essayons maintenant de décrypter les propriétés d’une fonction de type ∀ 'a, ('a -> 'a -> bool) -> 'a list -> 'a list. Comme la précédente, on ne peut pas modifier les éléments. Mais, cette fois-ci, f peut les comparer pour les réordonner. En effet, on lui donne une relation (appelons là r) entre les différentes valeurs de ‘a. Ainsi, on pourrait faire une fonction qui trie les éléments d’une liste, ou qui retire les doubles de chaque élément. Mais, si deux types et relations associées sont isomorphes, alors la fonction fera la même chose sur les deux.
Dans le papier, on exprime celà en disant que, pour une fonction g et deux relations r et r’, si g préserve la relation (pour tout x et x’, r x x’ = r’ (g x) (g x’)), pour toute liste l, g* (f r l) = f r' (g* l).
Dans le cas d’une fonction de tri, ça veut dire que, par exemple, ajouter 1 à chaque élément ou les multiplier par deux peut être fait avant ou après le tri. Dans le cas d’une fonction qui retire les doublons, tant que g ne donne pas le même résultat pour deux valeurs différentes, appliquer g à tous les éléments avant ou après avoir retiré les doublons ne change rien.

Ces propriétés sont, entre autre, assez utile pour ce qui est de définir des fonctions qui doivent respecter certaines propriétés: si une ou deux de ces propriétés suivent directement des autres et du théorème gratuit, on n’a plus besoin de les montrer à chaque fois, ce qui nous simplifie beaucoup la vie.

Enfin voilà, j’espère que cette petite introduction vous aura donné une idée du pouvoir qui se cache derrière ces types polymorphes, quand bien examinés sous toutes leurs coutures, et à bientôt.

Amélia Coutard