Programmation Avancée

TP9: les GDATs à la rescousse (2)

Exercices conçu par François Thiré

L'objectif de ce TP est de vous montrer à travers l'exemple des arbres rouge et noir que le système de type d'OCaml permet de garantir des invariants assez forts sur nos données. Pour cela, on va se servir d'une fonctionnalité d'OCaml qui existe depuis la version 4.0 : les Generalized Algebraic Data Types (GADT).

Les GADTs par l'exemple

Comme le nom le laisse entendre, un GADT est une généralisation des types algébriques habituels. Cette généralisation passe par le polymorphisme, et permet de préciser un type plus précis pour les constructeurs. Par exemple, le type habituel des listes :

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

peut se réécrire avec la syntaxe GADT par

type 'a list = Empty : 'a list | Cons : 'a * 'a list -> 'a list

La différence est que l'on précise le type de retour ( 'a list pour le constructeur Empty par exemple). Par défaut, le type de retour est toujours celui que l'on déclare. Les GADTs nous permettent de donner un type un peu différent. Par exemple, on peut mémoriser dans le type de retour si une liste est vide ou non


type empty



type not_empty 

type ('a,'b) list = Empty : ('a,empty) list 

| Cons : 'a * ('a,'b) list -> ('a, not_empty) list

L'intérêt de faire ça, est de pouvoir garantir que la fonction hd sur nos listes est totale, seul son type va changer :


let hd (l: ('a, not_empty) list) : 'a =



match l with

| Cons(x,_) -> x

Ici, OCaml détecte que le pattern-matching est exhaustif, car la seule façon que l'on a pour construire un objet de type ('a, not_empty) list , c'est d'utiliser le constructeur Cons . Bien sûr, cela implique que le code suivant sera refusé par le type checker à la compilation :

let _ = hd (Empty)

avec l'erreur :

This expression has type ('a, empty) list



but an expression was expected of type ('a, not_empty) list 
Type empty is not compatible with type not_empty

Les GADTs nous permettent de transformer une fonction qui avant était partielle en une fonction totale !

Question 1

Comment utiliser un GADT pour connaître statiquement la longueur d'une liste ?

Red-Black trees

Un Red-Black tree est une structure de données permettant de gérer un arbre binaire de recherche avec une garantie que la profondeur de l'arbre sera toujours en O(log n). C'est une alternative à d'autres structures de données comme les arbres AVL ou les arbres 2 - 3 - 4. Pour cela, toutes les opérations sur cette structure de données maintiennent 5 invariants :

Un noeud est soit rouge soit noir ;
La racine est noire ;
Le parent d'un noeud rouge est noir ;
Les feuilles sont noires ;
Le chemin de chaque feuille à la racine contient le même nombre de noeuds noirs.

Vous trouverez à cette addresse, une implémentation naïve (et partielle) en OCaml des arbres rouge et noir. Dans cette implémentation, seul le premier invariant est garanti par typage. L'objectif de ce TP est de voir qu'il est possible de garantir aussi les quatre autres invariants par typage grâce aux GADTs.

Question 2

Implémenter une fonction is_valid qui vérifie qu'un arbre respecte bien les 5 invariants.

Question 3

Compléter la fonction balance (1 ligne)

Les GADTs à la rescousse

Pour cette partie, je vous invite à repartir d'un module vierge.

Question 4

En utilisant un GADTs, implémenter un type 'a tree qui permet de connaître par typage la couleur de la racine.

Question 5

Raffiner votre type 'a tree pour en plus garantir l'invariant 3 si ce n'est pas déjà le cas.

Question 6

En utilisant une nouvelle fois un GADT, raffiner votre type 'a tree en un ('a,'b) tree pour compter le nombre de noeuds noirs dans chaque branche.

Question 7

Implémenter le type t , le type des arbres rouge et noir (je vous invite à utiliser un GADT pour faire un type existentiel).

Question 8

Implémenter la fonction mem : int -> t -> bool sur ce nouveau type. OCaml aura du mal à typer votre fonction à cause des GADTs. Pour l'aider, vous pouvez utiliser l'une annotation de type suivante :

let rec mem : type a b. int -> (a, b) tree -> bool = fun x t -> ...

à ce stade, on est seulement à moitié content. En effet, on n'a toujours pas créé notre fonction insert . Le problème qui va se poser est que l'insertion d'un noeud peut créer un arbre dans un état incohérent, ce qui n'est pas valide d'après nos nouvelles définitions de type. Ainsi, la fonction balance n'est pas typable actuellement.

Question 9

Caractériser les différents types d'arbre dans un état incohérent lors de l'exécution des fonctions insert et balance ?

Question 10

Insérer un noeud dans un arbre ne crée pas toujours une incohérence. En utilisant cette remarque et la question précédente, en déduire un type ('a) dirty représentant des arbres potentiellement incohérents avec (n+1) constructeurs où n représente les types d'arbres identifiés à la question précédente.

Question 11

Comme la fonction balance renvoie un arbre dont on ne connaît pas la couleur de la racine (pourquoi ?), implémenter un type 'a utree qui oublie la couleur de la racine d'un arbre

L'ancienne fonction balance : rbtree -> rbtree peut-être transformée en une fonction de type color -> int -> rbtree -> rbtree -> rbtree . En utilisant les remarques suivantes :

L'arbre gauche ou l'arbre droit est dans un état incohérent mais pas les deux
Quand la racine est rouge, la fonction balance retourne un arbre incohérent mais le nombre de noeuds noirs n'a pas changé dans chaque branche
Quand la racine est noire, la racine de l'arbre retournée est soit rouge soit noire et le nombre de noeuds noirs dans chaque branche a augmenté de 1

Question 12

Implémenter 4 fonctions qui découpent le rôle de l'ancienne fonction balance .

Question 13

Maintenant que nous faisons une distinction entre les arbres dont la racine est rouge et les arbres dont la racine est noire, cela implique qu'on devra créer deux fonctions d'insertion qui dépendent du type de la racine.

Implémenter ces deux fonctions.

Question 14

En déduire la fonction d'insertion finale sur le type t défini précédemment.

Question 15

(Bonus) Transformer votre implémentation pour que le type t soit polymorphe (on pourra faire un foncteur).

Question 16

(Bonus) Implémenter la suppression d'un noeud dans un arbre.