Revenir à l'accueil

Un cas d'école à l'utilisation des GADTs

Publié le 16 du 10 2017

Cet article fait écho à un tweet et à une conversation que nous avons eu sur le Slack de LilleFP. L’article propose de survoler un cas d’école de l’usage des types algébriques généralisés (GADTs) avec le langage OCaml qui a l’avantage d’avoir une syntaxe concise et relativement claire.

L’objectif de l’article est avant tout de donner un exemple clair de l’utilisation des GADTs, sans rentrer dans des considérations théoriques complexes (en plus je n’en ai pas les compétences), et de fournir une définition naïve de ce qu’ils sont, par rapport à des types algébriques classiques. A la fin de l’article, on parlera un peu des langages orientés objets, de leur manière de représenter des types sommes et de pourquoi il ne s’agit pas réellement de GADTs en donnant une définition un peu plus fine que lors de la première partie de l’article.

Une connaissance d’un langage de la famille ML est préférable pour la lecture de cet article.

Dans le monde des langages de programmation statiquement typés, on tâche de toujours typer correctement nos données pour que le compilateur puisse vérifier la cohérence d’un programme à la compilation, nous déchargeant ainsi d’un lourd travail de vérification. Dans les langages de la famille ML, on a, à notre disposition, les types de données algébriques (ADT), permettent d’exprimer, de manière assez élégante, des structures de données diverses (des arbres, ou des listes par exemple).

En OCaml, on possède deux formes d’ADTs :

Dans cet article, on va surtout s’intéresser aux types sommes. Cependant, n’hésitez pas, pour plus d’informations, à lire cet excellent tutoriel qui survole une grande partie du langage OCaml.

Rappel sur les types sommes

Les types sommes permettent d’unifier plusieurs types de données au sein d’un même type au moyen de constructeurs. Par exemple :

type color = 
 | Red   
 | Blue  
 | Green 

let a_color = Red 
let a_color_list = [Red; Green; Blue]

Dans cet exemple, la variable red aura le type color et la variable a_color_list aura le type color list.

Il est important de préciser que les constructeurs ne sont pas des sous-types, ce sont des valeurs qui appartiennent au type color.

Notre propre type pour les listes

Grâce aux types sommes, il est possible de construire facilement, au moyen de types récursifs, des structures de données communes. Par exemple, une liste :

type 'a my_list = 
  | Empty
  | Cons of ('a * 'a my_list)

let a_list = Cons (Red, Cons (Blue, Cons (Green, Empty)))

Ici, a_list aura le type color my_list. Les constructeurs d’un type t construisent des termes de type t. De plus, ils s’utilisent très bien avec la correspondance de motifs. Par exemple, voyons comment implémenter la fonction iterate pour notre nouveau type liste, dont le type serait :

val iterate : ('a -> unit) -> 'a my_list -> unit

let rec iterate f list = 
  match list with 
  | Empty -> ()          
  | Cons (head, tail) -> 
     let () = f head in 
     iterate f tail           

Implémentation de head et tail

Comme nous le montre notre type et notre fonction iterate, il est commun et pratique de caractériser une liste par une tête et une queue. Dans une valeur de type 'a my_list, la tête aura le type 'a et la queue aura le type 'a my_list. Voyons tout de suite comment implémenter ces fonctions.

Traiter le cas des listes vides

L’implémentation de ces deux fonctions est simple, cependant, que doit-on faire quand on essaye d’avoir la tête ou la queue pour une liste vide ? Une approche classique serait de faire comme beaucoup de langages font pour traiter un cas exceptionnel, en lançant une exception :

exception Empty_list of string

let head list = 
  match list with 
  | Empty -> raise (Empty_list "head") 
  | Cons (head, _) -> head                        

let tail list = 
  match list with 
  | Empty -> raise (Empty_list "tail") 
  | Cons (_, tail) -> tail

Cette approche fonctionne, et c’est d’ailleurs le choix qui a été fait pour la bibliothèque standard de OCaml. D’autres langages, comme Elm ont fait le choix de changer le type habituel de head et tail pour emballer le résultat de la fonction dans une option. De cette manière, le type des deux fonctions indique directement qu’il faut traiter, à la main, le cas des listes vides et comme Elm interdit une correspondance de motifs non-exhaustive, on est sur, après la compilation, qu’on aura traité les cas où une liste est vide.

let head list = 
  match list with 
  | Empty -> None
  | Cons (head, _) -> Some head                        

let tail list = 
  match list with 
  | Empty -> None
  | Cons (_, tail) -> Some tail

Pour peu que l’on possède suffisament d’outils pour manipuler les options, je préfère largement cette approche à celle de lancer une exception. En effet, je trouve le code plus facile à lire, à maintenir, et la signature de type des deux fonctions nous donne directement une indication sur le fait qu’une fonction puisse “échouer”, alors que la signature de type ne donne aucune information sur le fait qu’une fonction lance une exception (c’est le rôle de la documentation de nous informer de ce genre d’informations).

Cependant, il serait intéressant de se demander s’il serait possible, à la compilation et donc, au niveau du système de type, de définir que head et tail ne peuvent prendre que des listes non-vides.

L’utilisation de types fantômes

J’avais déjà, à l’époque où je travaillais chez Dernier Cri, rédigé un article qui expliquait (de manière abordable, je l’espère), l’idée et l’intérêt des types fantômes.

Sans rentrer dans les détails, un type fantôme est un type que l’on va passer en paramètre d’un autre type, et dont le seul intérêt d’encoder des informations statiques sur le type dont il est le paramètre.

type ('a, 'b) t = 'b my_list

Dans cet exemple, 'b sera le type des données de la liste, et on utilisera 'a pour définir si la liste est vide ou non.

type empty_t 
type not_empty_t 

type 'a my_list =
 | Empty
 | Cons of ('a * 'a my_list)

type ('a, 'b) t = 'b my_list 

let empty = Empty
let cons x xs = Cons (x, xs)
let head list =
 match list with
 | Cons (x, _) -> x
 (* on ne devrait jamais être ici grâce aux types *)
 | Empty -> assert false

L’implémentation générale ne diffère pas réellement de ce que nous avions fait précédemment. les deux types empty_t et not_empty_t serviront uniquement à être le paramètre 'a de notre type ('a, 'b) t. C’est pour ça qu’ils n’ont pas de forme, la seule chose qui nous intéresse est leur nom. Nous allons pouvoir implémenter l’interface de notre module:

type empty_t
type not_empty_t 
type ('a, 'b) t

val empty : (empty_t, 'a) t
val cons : 'b -> ('a, 'b) t -> (not_empty_t, 'b) t
val head : (not_empty_t, 'a) t -> 'a

Dans l’interface, nous n’allons pas exposer le types non nécéssaire, par exemple, my_list, comme ça, on peut forcer l’utilisation de nos fonctions cons et empty qui retournent des types t bien typés.

Maintenant, il suffit de définir le type de la fonction head en spécifiant qu’elle ne peut prendre que des listes non vides : (not_empty_t, 'a) t -> 'a.

Avec un type de liste comme nous l’avons implémenté, il n’est pas possible d’implémenter la fontion tail, car on ne pourrait pas savoir si la liste renvoyée est vide. Pour palier à ce manque, il suffirait d’encoder la taille de la liste dans le type fantôme. Pour cela, on peut se servir de des entiers de Peano, qui rend l’implémentation de nombres positifs dans le système de type très aisé.

Cependant, ce n’est pas le sujet de l’article, donc je vous propose d’expérimenter ceci par vous même.

Utilisations des GADTs

Dans l’exemple proposé, on peut rapidement se rendre compte de quelques faiblesses liées à l’usage de types fantômes :

C’est pour répondre à ces problématiques que OCaml intègre, depuis sa version 4.00, des types algébriques généralisés. En effet, les GADTs permettent de séparer le type retourné par les constructeurs d’un autre type. Par exemple, avec notre type my_list précédemment définit (que l’on va renommer t par soucis de concision) :

type ('a, 'b) t =
  | Empty : (empty_t, 'b) t
  | Cons : ('b * ('a, 'b) t) -> (not_empty_t, 'b) t

Avec ce type, OCaml inférera directement le bon type 'a en fonction du constructeur utilisé, par exemple :

let x = Empty
val x : (empty_t, 'a) t = Empty

Il devient donc très facile d’implémenter la fonction head :

let head list = 
  match list with 
  | Cons (x, _) -> x

(* ou de manière plus concise *) 
let head (Cons (x, _)) = x                  

Globalement, les GADTs permettent de décrire une relation entre un constructeur de type et un autre type. Ils amènent deux points utiles :

Ils permettent de faire ce que l’on faisait avec des types fantômes, de manière moins verbeuses et imposent moins de boilerplate.

Comme pour les types fantômes, leur usage peut éliminer des soucis de types ennuyeux et produire du code “plus sûr” et pour lesquels on laisse au compilateur une grosse charge de vérifications. On peut trouver beaucoup d’usages où leur utilisation améliore le code, par exemple, dans les récentes modifications apportée à la bibliothèque Lwt.

De plus, en OCaml (et en Haskell) comme à la compilation, on perd toute information de typage, leur utilisation n’apporte aucun préjudice à la performance. Cependant, l’usage excessif de GADTs peut entrainer des erreurs de types (à la compilation) plus cryptiques.

Dans la bibliothèque standard de OCaml, les GADTs ont étés utilisés, notamment, pour une nouvelle implémentation des Formats.

Les types sommes dans les langages objets

Tout d’abord, je voudrais sincèrement remercier Nicolas Rinaudo et Gabriel Scherer pour m’avoir aidé dans la rédaction de cet article, respectivement pour m’avoir expliqué des traits relatifs à Scala et pour m’avoir donné plus d’éléments théoriques sur ce que sont réellement les GADTs et les travers liés à l’analogie entre GADTs et héritage.

Dans un langage de programmation orientée objets, on peut faire une rapide analogie entre les types sommes et les classes unifiés par des liens d’héritage. Implémentons le type option que nous avons utilisé précédemment, en Scala :

sealed trait Option[+A]
case object None extends Option[Nothing]
case class  Some[A](value: A) extends Option[A]

Sans rentrer dans les détails de l’implémentation, on définit deux cases, un objet, qui n’aura qu’une seule valeur habitante possible (un Singleton), et une classe (qui elle pourra avoir plus d’un habitant possible). L’usage de case nous permet de supporter la correspondance de motifs et donc offrir à nos instances, la déconstruction que nous avions évoqués dans les avantages des types sommes.

Ce que l’on remarque assez vite, c’est que, pour créer cette notion d’ union discriminée, on va créer une type parent (ici, le trait Option) et que nos deux types enfants (None et Some) hériteront du parent. Comme nos constructeurs sont ici des classes, l’approche orienté objets des types sommes introduit déjà une notion de types de constructeurs. De ce fait, je peux très facilement implémenter une fonction qui ne pourrait prendre que des Some(x), par exemple :

def unwrap[A](x : Some[A]) = x.value

Obserervons maintenant l’implémentation d’une liste, le code ne varie pas beaucoup du type Option :

sealed trait MyList[+A]
case object Empty extends MyList[Nothing]
case class Cons[A](x: A, xs: MyList[A]) extends MyList[A] 

Comme pour la fonction unwrap, nous pourrions simplement l’écrire dans un objet quelconque, cependant, comme nous sommes dans un langage orienté objet, considérons maintenant que head est une méthode de notre classe Cons :

sealed trait MyList[+A]
case object Empty extends MyList[Nothing]
case class Cons[A](x: A, xs: MyList[A]) extends MyList[A] {
  def head() : A = x
}

Ce qui est très amusant, c’est qu’il ne faut pas spécialement un langage futuriste pour encoder ce genre de types. En effet, on pourrait très facilement transposer ce code en Java. Nous pouvons donc nous poser deux questions :

  1. est-ce que les liens d’héritages produisent la même chose que des GADTs ?
  2. A-t-on besoin de GADTs dans un langage orienté objet (typé statiquement) ?

Scala possède-t-il des GADTs

De la même manière que Scala ne possède pas, à proprement parlé, de types sommes, Scala ne possède pas de GADTs. La manière d’encoder quelque chose qui s’apparente aux types sommes est l’application de caractéristiques communes aux classes liées par héritage et aux types sommes.

Concernant les GADTs, Nicolas Rinaudo m’a transmis un article qui explique pourquoi, en jouant uniquement sur l’héritage, on ne peut simuler qu’une partie de l’usage des GADTs et il propose une autre implémentation pour tâcher, au mieux, de profiter pleinement des GADTs.

Concrètement, dans l’exemple des listes vides/non-vides, que j’ai choisi parce que je le trouve facile à appréhender (et qu’il permet d’avoir un cheminement linéaire des types sommes aux GADTs en passant par les types fantômes), on ommet un autre point essentiel aux types algébriques généralisés : l’égalité entre types.

L’article propose d’ajouter des preuves d’égalités pour typer finement les consommateurs de données. On appelle cette méthode l’encodage final. Par opposition, les GADTs typent finement les données, on appelle ça un encodage initial.

En Scala, le traitement des égalités entre type est trop fragile et pose parfois des soucis au compilateur. De ce fait, Scala ne possède pas de GADTs à proprement parlé, mais permet, via l’héritage, de répondre à certaines problématiques que les GADTs solutionnent aussi. Cependant, Dotty (un compilateur expérimental pour le langage Scala, qui fait aussi office d’incubateur et qui a pour vocation de faire reposer Scala sur des bases plus formalisées) semble intégrer de véritables GADTs… wait and see.

Conclusion

Comme beaucoup d’usages avancés du système de type, il est parfois difficile de trouver des cas d’usages où les GADTs sont essentiel. J’espère tout de même que cet article aura, pour certain, pu être une introduction abordable à leurs usages. Je remercie encore sincèrement Nicolas Rinaudo et Gabriel Scherer pour leurs apports techniques sur la question et tous les membres de la communauté LilleFP pour m’avoir forcé (voire oppressé) pour la mise en place d’un blog !

Cet article est terminé !
Si jamais vous avez des remarques, n'hésitez pas à écrire un commentaire ou à contribuer