Programmation Avancée

TP3: Sous-typage et abstraction

Préliminaire: types fantômes

Exercices conçu par David Baelde

L'idée générale des types fantômes est d'attacher à un type abstrait un paramètre de type qui serait inutile du point de vue du type concret associé, ceci afin d'obtenir une API agréable et (plus) sure.

Cette idée n'est pas propre à OCaml. Le wiki Haskell illustre cette technique avec l'exemple (vu en cours) de sanitisation de chaines de caratères. Voici ce que cela donne en OCaml. D'abord la signature:

type 'a str
type clean
type dirty

(** On peut calculer la longueur de toute chaîne. *)
val length : 'a str -> int
(** Les inputs sont sales: on se méfie de l'utilisateur. *)
val read : unit -> dirty str
(** Il faut les nettoyer ... *)
val sanitize : dirty str -> clean str
(** ... avant de pouvoir les afficher. *)
val write : clean str -> unit

puis l'implémentation, très simple et sans surcoût à l'exécution:

type 'a str = string
type clean = unit (* ou autre, qu'importe *)
type dirty = unit

let length s = String.length s
let read () = read_line ()
let write s = Printf.printf "%s\n" s
let sanitize s = Filename.quote s

Avec cette API on ne peut exécuter write (read ()). On est forcés de faire write (sanitize (read ())) ce qui évite d'afficher des caractères spéciaux sans échappement.

A l'intérieur du module défini ci-dessus, on notera que le type 'a str est covariant et contravariant en son paramètre 'a, puisque celui-ci est inutilisé. La signature de ce module rend le type abstrait: en l'absence d'information, le type 'a t y est invariant en son paramètre. On peut le rendre covariant en annotant, dans la signature, type +'a str (ou contravariant avec -'a); cela ne serait bien sûr pas permis si la définition concrète de str dans l'implémentation n'était pas covariante (et contravariante pour l'annotation -'a).

Exercice: permissions fantômes

Dans l'exemple préliminaire, on avait des fonctions qui ne prennent qu'un type de chaine, et des fonctions qui les prennent tous. Nous allons voir dans l'exercice qui suit comment exploiter le sous-typage pour faire des distinctions plus fines.

Question 1

On considère un type de descripteur de fichier, annoté par les permissions que l'on a sur le fichier: rw pour lecture+écriture, ro pour lecture seule et wo pour écriture seule. Nous souhaitons interdire, par typage, l'écriture sur un fichier en lecture seule, et vice versa.

Récupérer la base de code ici, et là, le Makefile, ainsi que les différents fichiers de no tests, le fichier test ainsi que les fichiers strings Quand vous tapez make, cela compile le module File ainsi que quelques tests d'utilisation. Les fichiers test<i>.ml sont censés compiler, mais pas les fichiers notest<i>.ml. Si quelquechose ne se passe pas comme prévu, make échoue en affichant ERREUR; c'est le cas dans l'archive initiale.

Votre mission est de mettre en place une discipline de type qui empêche les mauvais bouts de code de compiler, en modifiant uniquement file.mli et file.ml: il est interdit d'insérer ne serait-ce qu'une coercion dans les autres fichiers.

Vous utiliserez un type fantôme, dont le paramètre sera instancié par différents types d'objets en fonction des permissions associées au fichier. Clairement, il vous faudra utiliser du sous-typage sur le paramètre fantôme.