Calendrier de l'Avent - Types indexés par leur taille.
Dans ce deuxième article sur les types dépendants, nous allons voir un moyen de les utiliser pour définir des structures de données plus précises qu’à l’ordinaire, d’une taille fixée. J’utiliserai une syntaxe proche de celle d’ocaml pour écrire les exemple, mais j’essayerai de l’expliquer au fur et à mesure.
Les listes classiques.
Pour la définition classique des listes chainées, une liste est soit une liste vide, soit un élément suivi d’une autre liste.
(* Liste d'éléments de type 'a, pour n'importe quel 'a. *)
type 'a list
= Nil (* Soit une liste vide, soit *)
| Cons of 'a * 'a list (* un 'a et une liste de 'a. *)
On peut définir plein de fonctions utiles sur ce type, par
exemple map
qui applique une fonction à tous les éléments
d’une liste.
(* Pour tous types 'a et 'b, map est une fonction qui prend
* une fonction de 'a vers 'b, et une liste de 'a, et retourne
* une liste de 'b. *)
let rec map (f : 'a -> 'b) (vs : 'a list) : 'b list =
(* Si vs est... *)
match vs with
(* une liste vide, on retourne une liste vide. *)
| Nil -> Nil
(* une valeur suivie d'une liste, on applique f à la
* valeur, et on applique f à tous les autres via map. *)
| Cons (v, vs') -> Cons (f v, map f vs')
Cependant, on se heurte à un problème si on essaye de faire une fonction similaire qui s’applique à deux listes au lieu d’une: que faire quand les listes sont de taille différente ?
let rec map2 (f : 'a -> 'b -> 'c) (vs : 'a list) (ws : 'b list)
: 'c list =
match (vs, ws) with
| (Nil, Nil) -> Nil
| (Nil, Cons _) -> ???
| (Cons _, Nil) -> ???
| (Cons (v, vs'), Cons (w, ws')) ->
Cons (f v w, map2 f vs' ws')
Ici, on pourrait mettre Nil
à la place des ??? (c’est l’option choisie
par Haskell), ou on pourrait lever une erreur (c’est l’option choisie par
Ocaml). Mais, il serait pratique de pouvoir simplement s’assurer que le
cas n’arrive pas. Pour cela, il faudrait pouvoir garantir que les deux
listes ont la même longueur. Qu’à cela ne tienne, essayons de définir un
type des listes de taille n.
Les listes de taille n.
(* Le type unit est un type qui n'a qu'une seule valeur.
* type unit = ()
* ('a * 'b) est un type qui représente les paires de 'a
* et 'b (un de chaque).
*)
type 'a list0 = unit (* 0 éléments, () = liste vide *)
type 'a list1 = 'a * unit (* 1 élément *)
type 'a list2 = 'a * ('a * unit) (* 2 éléments *)
type 'a listn = 'a * (... * ('a * unit)) (* n éléments *)
Bien sûr, définir un type distinct par taille est très peu pratique, et ne nous permet pas vraiment d’écrire des fonctions qui marchent sur toutes les tailles de listes.
Mais, on peut remarquer un point commun entre tous ces types. Si on avait des types dépendants en OCaml, on pourrait écrire quelque chose qui ressemblerait un peu à ça:
type ('a, 0) list = unit (* 0 éléments *)
type ('a, 'n + 1) list = 'a * ('a, 'n) list (* 'n + 1 éléments *)
(* Ici, 'n est un entier ≥ 0. *)
Ici, l’idée est simple: au lieu d’avoir deux constructeurs au choix, le choix du constructeur dépend uniquement de la taille de la liste: si elle est de taille 0, c’est le cas qui ressemble à Nil, et si elle est de taille n + 1, c’est le cas Cons, 1 élément + une liste de n éléments.
Reprenons maintenant notre tentative d’implémentation de map2.
let rec map2 (f : 'a -> 'b -> 'c) (vs : ('a, 'n) list)
(ws : ('b, 'n) list) : ('c, 'n) list =
match (vs, ws) with
(* 'n = 0 *)
| ((), ()) -> ()
(* 'n = 'm + 1, l'appel récursif de map2 se fait avec
* la taille 'm. *)
| ((v, vs'), (w, ws')) ->
(f v w, map2 f vs' ws')
(* | ((), (_, _)) -> 'n ne peut pas être à la fois 0 et
* quelque chose + 1, donc ce cas est impossible. *)
(* | ((_, _), _) -> Même raisonnement. *)
Ici, plus de problème: le système de typage nous garantit que les listes font la même taille, et que l’on n’aura donc jamais à traiter les cas problématiques.
Ici, j’ai donné l’exemple des listes de taille n, mais on aurait pu donner bien d’autres exemples, comme les nombres inférieurs à n, les langages de mots de taille au plus n, etc. Une fois qu’on les a un peu utilisés, on a du mal à s’en passer.
Enfin voilà, j’espère que ça vous aura intéressé et appris quelque chose, et à bientôt pour la suite.