Re: Solution à base de types variants en ADA

J'ai l'impression qu'on navigue à la frontière entre le rôle du compilateur et celui de l'analyseur de statique de code.

Certes, mais le contrôle de type (type checking) effectué par un compilateur relève de l'analyse statique de code. Dans les faits, on ajoute des outils d'analyse statique de code à l'extérieur du compilateur pour pallier aux déficiences du système de types d'un langage. Et pour fonctionner, ces outils nécessitent habituellement l'ajout d'annotations au code sous forme de commentaires, annotations qui correspondent à un enrichissement du langage des types du langage de départ.

Dans tout langage de programmation, il y a en réalité deux langages :

• le langage des termes pour décrire les calculs à effectuer ;
• le langage des types pour rejeter à la compilation, ou à l'exécution, certains termes comme sémantiquement invalides (vides de sens).

Plus le langage des types est évolué, plus il permet de contrôler la bonne formation des termes à la compilation (c'est-à-dire statiquement). L'idée des ADT est de pouvoir effectuer du raisonnement par cas non sur la valeur des termes (ce qui ne peut se faire qu'à l'exécution, là où la valeur est connue) mais sur leur type (ce qui est connu statiquement à la compilation).

On peut même pousser le principe plus loin avec des GADT pour discriminer plus fortement la construction des termes, et faciliter l'optimisation du code généré sans avoir à gérer d'exception au runtime. Je vais l'illustrer sur un exemple en OCaml avec une fonction qui retourne la valeur du nœud racine d'un arbre binaire parfait.

Avec les ADT, on peut encoder les arbres binaires parfaits ainsi :

type 'a t =
 | Empty : 'a t
 | Node : 'a * ('a * 'a) t -> 'a t

Les contraintes sur le type ne permettent que de construire des arbres parfaits : soit l'arbre est vide, soit c'est un nœud qui contient une valeur de type a et un arbre paramétré par un couple de type 'a * 'a (ce qui représente les sous-arbres gauche et droite).

Pour extraire, la valeur du nœud racine on procède ainsi :

let top = function
 | Empty -> failwith "Empty tree"
 | Tree (v, _) -> v

La fonction retournera une exception à l'exécution si on lui passe un arbre vide :

top Empty;;
Exception: Failure "Empty tree".

Maintenant, avec les GADT, on peut encoder ce type d'arbre ainsi :

type z = Z
type 'n s = S : 'n -> 'n s
type ('a, 'n) t =
 | Empty : ('a, z) t
 | Tree : ('a, 'n) t * 'a * ('a, 'n) t -> ('a, 'n s) t

Ici, c'est plus subtil et plus précis au niveau des contraintes de types. On commence par encoder les entiers dans le système de type avec z pour représenter zéro, et 'n s pour représenter la fonction successeur. Ensuite, on paramètre le type des arbres à la fois par le type des nœuds ('a) ainsi que par sa profondeur ('n). La définition dit qu'un arbre vide est de profondeur nulle et que les sous-arbres d'un nœud ont la même profondeur 'n (l'arbre est parfait) et que sa profondeur est 'n + 1 = 'n s.

Pour coder la fonction top, il est n'est plus nécessaire de traiter le cas de l'arbre vide :

let top : type a n. (a, n s) t -> a = function
 | Tree (_, v, _) -> v

Le type de la fonction déclare explicitement que la profondeur de l'arbre est du type successeur ('n s) et donc l'arbre ne peut être vide. Cette fois, si on lui passe un arbre vide, on a une erreur de typage à la compilation :

top Empty;;
Error: This expression has type ('a, z) t
 but an expression was expected of type ('a, 'b s) t
 Type z is not compatible with type 'b s

Pour ce qui est du code généré par le compilateur (option -dlambda du compilateur), on peut vérifier qu'il peut faire l'économie d'un test à l'exécution.

Avec ADT, on obtient :

let 
 (top =
 (function p
 (if p (field 0 p)
 (apply (field 1 (global Pervasives!)) "Empty tree"))))

Avec les GADT, on a :

let (top = (function p (field 1 p))

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.