Avant-propos
Pour une bonne compréhension de cet article, une connaissance sommaire du langage OCaml est requise (connaître les types variants / disjonctions, les modules et les types abstraits et, évidemment, être à l'aise avec la syntaxe de OCaml). Avant de nous lancer dans le vif du sujet, nous commencerons par évoquer un cas pratique où les types fantômes auraient pu être utiles.
Ensuite nous rappellerons quelques fondamenteux relatifs à OCaml et nous définirons enfin ce que sont les types fantômes. Pour terminer, quelques cas pratiques seront présentés.
Il est important de noter que cet article utilise OCaml 4.x.
Mars Climate Orbiter
Le 23 Mars 1999, la sonde "Mars Climate Orbiter" tente d'effectuer sa manoeuvre d'insertion autour de l'orbite de Mars, via une procédure entièrement automatisée. Au cours de celle-ci, la radio fut coupée durant le temps où la sonde se trouvait derrière Mars. Après plus de 24h sans signal radio, la sonde a été considérée comme perdue. Elle avait suivi une trajectoire beaucoup trop basse (près de 140 km
en dessous de ce qui était prévu) par rapport à sa vitesse et s'est donc probablement transformée en boule de feu. Mais comment une telle erreur a pu se produire ?
Une commission d'enquête révèlera vite la raison de cette erreur de trajectoire : la sonde recevait la poussée de ses micropropulseurs en livre-force.seconde (une unité de mesure anglo-saxonne) et le logiciel interne de la sonde traitait ces données comme s'il s'agissait de newton.seconde. Cette discordance d'unité a entraîné des
erreurs de calcul de la trajectoire de la sonde, l'amenant à sa destruction et faisant perdre à la NASA près de 125 millions de dollars.
Ce qu'il faut retenir de cette histoire, c'est qu'une simple erreur de manipulation d'unité de mesure est à l'origine d'une catastrophe impressionnante qui a coûté au final plus de 125 millions de dollars - juste une dizaine de lignes de code perdues dans des millions (voire milliards) d'autres.
L'enjeu de cet article est de présenter une manière élégante de prévenir ce genre d'erreur, dès la compilation.
Tentative en utilisant des variants classiques
Restons dans le sujet et limitons notre problème à une distinction entre les centimètres et les kilomètres avec comme fonctionnalités, des conversions :
cm_to_km;km_to_cm.
Naïvement, lorsque j'ai été amené à lire le problème de typage soulevé par la sonde Mars Climate Orbiter, et de manière plus générale à la représentation d'unités de mesure, j'ai pensé à la définition d'une disjonction séparant les kilomètres des centimètres. Voici un exemple d'implémentation :
exception IllegalMeasureData
type measure =
| Cm of float
| Km of float
let cm x = Cm x
let km x = Km x
let cm_to_km = function
| Cm x -> Km (x *. 100000.0)
| _ -> raise IllegalMeasureData
let km_to_cm = function
| Km x -> Cm (x /. 100000.0)
| _ -> raise IllegalMeasureData
(*
exception IllegalMeasureData
type measure = Cm of float | Km of float
val cm : float -> measure = <fun>
val km : float -> measure = <fun>
val cm_to_km : measure -> measure = <fun>
val km_to_cm : measure -> measure = <fun>
*)
Bien que cette manière de procéder semble correcte, si je tente une conversion sur une valeur invalide, par exemple let test = km_to_cm (cm 10.0), mon code renverra une erreur IllegalMeasureData, et ce lors de la compilation. Cependant, si l'erreur se déclenche, c'est uniquement parce que la variable test évalue directement l'expression km_to_cm (cm 10.0). Voyons ce qu'il se passe si nous essayons de compiler notre code avec cette déclaration : let test () = km_to_cm (cm 10.0). Cette fois-ci, le programme compile.
La distinction entre les kilomètres et les centimètres ne peut pas être assurée lors de la compilation car les fonctions km_to_cm et cm_to_km ont le type measure -> measure. Et donc une incohérence telle que passer une valeur en kilomètre à la
fonction cm_to_km ne peut être détectée à la compilation.
Implémentation des types fantômes
Nous venons de voir que les variants classiques ne permettent pas assez de
vérifications pour distinguer des données au sein d'un même type à la
compilation. Oui, il serait possible de distinguer chaque unité de
mesure dans des types différents, de cette manière :
module Measure =
struct
type km = Km of float
type cm = Cm of float
end
Cependant ce n'est absolument pas confortable car il faudrait écrire
des opérateurs spécifiques pour chaque unité de mesure
et ce n'est pas réellement l'objectif de cet article.
Donc avant de définir et de proposer une implémentation, nous allons
devoir (re)voir quelques outils en relation avec le langage OCaml.
Les variants polymorphiques
Bien que très utiles dans le design d'application, les variants possèdent certaines limitations. Par exemple, le fait qu'un type Somme ne puisse être enrichi de constructeurs (ce qui n'est plus tout-à-fait vrai depuis OCaml 4.02.0),
mais aussi le fait qu'un constructeur ne puisse appartenir qu'à un seul type.
Les variants polymorphes s'extraient de ces deux contraintes et peuvent
même être déclarés à la volée, sans appartenir à un type prédéfini. La définition d'un constructeur polymorphe est identique à celle d'un constructeur normal (il commence par une majuscule) mais est précédée
du caractère `.
# let a = `Truc 9;;
val a : [> `Truc of int ] = `Truc 9
# let b = `Truc "test";;
val b : [> `Truc of string ] = `Truc "test"
Comme vous pouvez le voir, je me suis servi deux fois du constructeur
`Truc en lui donnant des arguments de types différent et sans l'avoir
déclaré.
Borne supérieure et inférieure
L'usage des variants polymorphes introduit une notation de retour
différente de celle des variants normaux. Par exemple :
let to_int = function
| `Integer x -> x
| `Float x -> int_of_float x;;
let to_int' = function
| `Integer x -> x
| `Float x -> int_of_float x
| _ -> 0
# val to_int : [< `Float of float | `Integer of int ] -> int = <fun>
# val to_int' :[> `Float of float | `Integer of int ] -> int = <fun>
On remarque que le chevron varie. Dans le cas où la
fonction n'évalue que les constructeurs Integer et Float, le
chevron est <. Si la fonction peut potentiellement évaluer autre
chose, le chevron est >. En résumé :
[< K]indique que le type ne peut contenir que K ;[> K]indique que le type peut contenir au moins K ;
Nous verrons que cette restriction sur les entrées permet d'affiner
le typage de fonctions.
Restriction sur les variants polymorphes
Les variants polymorphes ne permettent pas de faire des
choses comme :
let truc = function
| `A -> 0
| `A x -> x
Au sein d'une même fonction, on ne peut pas utiliser un même variant
avec des arguments différents. De mon point de vue, c'est plus logique
que limitant. Mais rien n'empêche de faire deux fonctions qui, elles,
utilisent des variants polymorphes à arguments variables.
Nommer les variants polymorphes
Bien que l'on puisse les nommer à l'usage, il peut parfois être
confortable de spécifier des variants polymorphes dans un type nommé
(ne serait-ce que pour le confort de la réutilisation). Leur syntaxe (que
nous verrons un peu plus bas) est assez proche des déclarations de
variants classiques. Cependant, on ne peut pas spécifier la borne
dans la définition de type de variants polymorphes. Ce qui est
parfaitement logique dans la mesure où un type ouvert (donc borné) ne correspond pas
à un seul type mais à une collection de types.
À la différence des variants normaux, les variants polymorphes se
déclarent dans une liste dont les différentes énumérations sont séparées
par un pipe. Par exemple :
type poly_color = [`Red of int | `Green of int | `Blue of int]
Il est tout de même possible d'utiliser les variants polymorphes dans la
déclaration de variants normaux, par exemple :
type color_list =
| Empty
| Cons of ( [`Red of int | `Green of int | `Blue of int] * color_list)
En revanche, même si dans les définitions de type on ne peut pas
spécifier de borne, on peut le faire dans les contraintes de type des
fonctions. C'est d'ailleurs grâce à cette autorisation que nous utiliserons les
types fantômes avec des variants polymorphes.
Conclusion sur les variants polymorphes
Les variants polymorphes permettent plus de flexibilité que les variants
classiques. Cependant, ils ont aussi leurs petits soucis :
- ils entraînent des petites pertes d'efficacité (assez superflues) ;
- ils diminuent le nombre de vérifications statiques ;
- ils introduisent des erreurs de typage très complexes.
J'ai introduit les variants polymorphes car nous nous en
servirons pour les types fantômes, cependant il est conseillé de ne
les utiliser qu'en cas de réel besoin.
A l'assaut des types fantômes
Après une très longue introduction et maintenant que les prérequis ont été
évoqués, nous allons pouvoir nous intéresser à la notion de type fantôme.
Concrètement, un type fantôme est un paramètre de type qui n'est
pas utilisé dans la définition du type. Par exemple : type 'a t = x.
On se servira de ce paramètre pour donner des informations sur comment
utiliser ce type.
Sachez que les types fantômes sont utilisés à plusieurs reprises dans
la bibliothèque standard. Il ne s'agit donc pas d'une feature
particulière ou marginale.
Concrètement, voici un exemple de type fantôme : type 'a t = float.
Si le type n'est pas abstrait, le type t sera identique à un flottant.
Par contre, si le type est abstrait (donc que son implémentation
est cachée), le compilateur le différenciera d'un type flottant.
Avec cette piètre définition on ne peut pas aller très loin. Voyons dans
les sections suivantes quelques cas de figure précis d'utilisation
des types fantômes.
Distinguer des unités de mesure
Si cet article a été introduit via une erreur due à des unités de mesure,
ce n'est pas tout à fait innocent. Nous avions vu que, via des variants
classiques, il n'était à priori pas possible (en gardant un confort
d'utilisation) de distinguer à la compilation des unités de mesure.
Nous allons voir qu'au moyen des types fantômes, cela devient très simple.
Par souci de lisibilité, j'utiliserai des sous-modules. Cependant, ce
n'est absolument pas obligatoire.
module Measure :
sig
type 'a t
val km : float -> [`Km] t
val cm : float -> [`Cm] t
end = struct
type 'a t = float
let km f = f
let cm f = f
end
Ce module implémente des fonctions qui produisent des valeurs de typeMeasure.t, mais qui sont décorées. Les kilomètres et les
centimètres ont donc une différence structurelle.
Enrichissions notre module d'une fonction addition, dont le prototype serait :'a t -> 'a t -> 'a t.
module Measure :
sig
type 'a t
val km : float -> [`Km] t
val cm : float -> [`Cm] t
val ( + ) : 'a t -> 'a t -> 'a t
end = struct
type 'a t = float
let km f = f
let cm f = f
let ( + ) = ( +. )
end
Que se passe-t-il si je fais l'addition de centimètres et de kilomètres
(créés au moyen des fonctions km et cm) ? Le programme ne compilera pas.
En effet, il est indiqué dans le prototype de la fonction que le paramètre
du type t ('a) doit impérativement être le même pour les deux membres
de l'addition. Cet exemple nous permet de constater que nous avons
une distinction, au niveau du typeur, des unités de mesure, pourtant représentées
via des entiers.
Retournons à notre exemple de conversion, cette fois enrichissons notre module
des fonctions de conversion :
module Measure :
sig
type 'a t
val km : float -> [`Km] t
val cm : float -> [`Cm] t
val ( + ) : 'a t -> 'a t -> 'a t
val km_of_cm : [`Cm] t -> [`Km] t
val cm_of_km : [`Km] t -> [`Cm] t
end = struct
type 'a t = float
let km f = f
let cm f = f
let ( + ) = ( +. )
let km_of_cm f = f /. 10000.0
let cm_of_km f = f *. 10000.0
end
En utilisant ce module, le typeur refusera formellement des conversions improbables.
Dans cet exemple, j'aurais pu utiliser autre chose que des variants
polymorphes pour distinguer mes centimètres de mes kilomètres. Cependant,
nous allons voir qu'il est possible de se servir des bornes pour affiner
le typeur. De plus, le fait de ne pas devoir les déclarer les rend agréable
à utiliser.
J'ai rédigé une implémentation concrète des unités de mesures via des types
fantômes via une extension de syntaxe. Son code source est disponible
ici.
Du HTML valide
Dans plusieurs frameworks web, il arrive que l'on se serve
de la syntaxe des fonctions du langage pour l'écriture de HTML.
Dans Yaws, un serveur web pour créer
des applications web en Erlang, les tuples et des atomes de Erlang
sont utilisés pour générer du HTML. De même que Ocsigen, le
framework de développement web OCaml, qui propose, entre autres, une écriture
fonctionnelle. Il existe plusieurs intérêts à cet usage, le premier étant
le plus évident : c'est généralement beaucoup plus rapide à écrire !
En effet, en HTML, beaucoup de balises doivent être fermées, les
attributs doivent être entre guillemets et liés par un égal, bref,
énormément de verbosité (Une petite blague
trouvée sur le site de Philip Wadler).
Dans un langage comme OCaml, le typage (et les types fantômes) nous
permettront d'encoder une partie du DTD du HTML pour ne permettre de créer
que des pages valides (selon le W3C) et donc amoindrir fortement le flux
de travail, ne devant plus passer par de la vérification avec les outils
du W3C et sachant que si une page compile, c'est qu'elle est formulée en HTML valide.
Un exemple classique : une balise span ne peut pas contenir de balisediv. Et de manière plus générale, aucune balise de type block ne peut
être contenue dans une balise de type inline. Autant de règles de validation
statiques qui peuvent être formalisées.
Sous-typage, covariance et contravariance
Les variants polymorphes introduisent une notion de sous-typage dans le
langage OCaml. Concrètement, un premier type (défini par des constructeurs
polymorphes) fermé est un sous-type d'un autre type (défini lui aussi par des
constructeurs polymorphes) fermé, si tous les constructeurs du premier
sont inclus dans les constructeurs du second.
En OCaml, le fait de considérer un sous-type comme son type parent est possible
au moyen d'une coercion, via l'opérateur :>, ce qui aura pour effet de projeter
un sous-type dans son sur-type (et donc le rendre plus générique).
Concrètement, la coersion d'une valeur d'un type t1 en
type t2 s'écrit de cette manière : valeur : t1 :> t2.
Le sous-typage des variants polymorphes introduit des règles particulières
dans le cas des fonctions :
- le type de retour d'une fonction suit la même direction de sous-typage que le type fonctionnel, on dit qu'il est covariant (et noté
+) ; - le type du paramètre va dans le sens inverse, on dit qu'il est contravariant (et noté
-).
Le compilateur de OCaml peut déterminer si un type est un sous-type d'un
autre pour les types concrets. Cependant, il lui est impossible de déduire
les sous-types des types abstraits.
type (+'a) t (* Type covariant *)
type (-'a) t (* Type contravariant *)
Cette précision est importante car nous nous servirons de la covariance et
de la contravariance pour produire des documents HTML statiquement typés.
Organisation par les types
Pour produire un document HTML, il faut d'abord isoler les constituants d'un
document HTML. Pour ma part, j'ai décidé de fragmenter les balises en trois
catégories :
- le texte brut (
pcdata) ; - les balises feuilles (
<br />,<hr />) par exemple ; - les balises noeuds (des balises pouvant en contenir d'autres).
Ces balises seront elles-mêmes divisées en plusieurs sous-catégories, par
exemple les balises dites inline (comme <span>), qui ne peuvent pas
contenir de balises dites block (comme <div>).
Je suggère cette implémentation :
module HTML :
sig
type (+'a) tag
end = struct
type raw_tag =
| Pcdata of string
| Leaf of string
| Node of string * raw_tag list
type 'a tag = raw_tag
end
Le fait que les feuilles et les noeuds prennent des chaînes de caractères
dans leur signature permettra de parser une arborescence HTML typée et d'en
produire le HTML textuel correspondant.
Nous pouvons nous atteler à la construction de balises, au moyen de fonctions.
Construction de balises
Les balises sont assez simples à construire. Commençons par la balise Pcdata, dont
la principale contrainte est de ne pouvoir prendre qu'une chaîne de caractères :
val pcdata : string -> [`Pcdata] tag
let pcdata x = Pcdata x
L'implémentation de <hr /> et <br /> est assez évidente, et ne demande pas
de précision :
val hr : [`Hr] tag
val br : [`Br] tag
let hr = Leaf "hr"
let br = Leaf "br"
Passons maintenant aux implémentations les plus intéressantes. Une <div> peut
à priori prendre n'importe quel type de balise (ce n'est pas tout-à-fait vrai,
mais nous partirons de ce principe pour l'exemple), son implémentation est donc
elle aussi assez facile :
val div : 'a tag list -> [`Div] tag
let div children = Node ("div", children)
Les <span> sont un peu différents car ces derniers ne peuvent contenir que des<span> ou des Pcdata. Il faut donc restreindre leur domaine d'entrée :
val span : [< `Span | `Pcdata ] tag list -> [`Span] tag
let span children = Node ("span", children)
Cette fois, la décoration du type tag restreint les entrées à seulement des données<span> ou des Pcdata car la borne est supérieure, donc on limite l'entrée
à ces deux types uniquement.
Pour rappel, le code général du module est :
module HTML :
sig
type (+'a) tag
val pcdata : string -> [`Pcdata] tag
val hr : [<`Hr] tag
val br : [<`Br] tag
val div : 'a tag list -> [`Div] tag
val span : [< `Span | `Pcdata ] tag list -> [`Span] tag
end = struct
type raw_tag =
| Pcdata of string
| Leaf of string
| Node of string * raw_tag list
type 'a tag = raw_tag
let pcdata x = Pcdata x
let hr = Leaf "hr"
let br = Leaf "br"
let div children = Node ("div", children)
let span children = Node ("span", children)
end
Je vous invite maintenant à saisir quelques expressions pour tester notre code,
par exemple : HTML.(span [br]) qui devrait échouer, ou encore HTML.(span [pcdata "hello"]),
qui devrait réussir. Un autre exemple un peu plus long :
let open HTML in
div [
span [pcdata "Hello world"];
hr;
span [pcdata "Hello Nuki"];
br;
]
Ce code est parfaitement valide et ne provoque donc aucune erreur. Par contre, si le dernier<span> avait été : span [div [pcdata "Hello Nuki"]], une erreur aurait été levée.
Retour d'expérience sur la production de HTML valide
L'exercice est intéressant et permet de comprendre le rôle des variants polymorphes dans la
décoration de types, via les types fantômes. C'est une méthode de ce genre (pas identique
ceci dit, sans aucun doute plus riche) qui est utilisée dans TyXML,
un des composants de Ocsigen pour rendre la production de XML invalide
impossible (il peut s'utiliser au moyen d'une extension de syntaxe).
Je trouve cette manière de procéder assez astucieuse, même si cet article n'en présente qu'une
infime partie. En effet, il faudrait aller plus loin en typant, par exemple, les attributs. Cependant, la
vocation de cet article n'est que de montrer un rapide exemple d'utilisation des types
fantômes.
Requêtes SQL statiquement typées
Une fois de plus, mon exemple est emprunté au cadriciel Ocsigen. En effet,
dans beaucoup de langages web, lorsque l'on doit effectuer une communication avec une base de données, il est courant de construire la requête dans une chaîne de caractères, qui est un moyen expressif de construire du SQL et de l'envoyer au serveur de base de données, lui délégant la vérification de la formation de cette dernière. C'est une manière de faire peu fiable, qui provoque des erreurs d'exécution de code, ce que le programmeur OCaml aime éviter.
Macaque est une bibliothèque permettant de formuler des requêtes vérifiées à la compilation. Pour cet exemple, je ne rentrerai pas dans les détails car le système de type de SQL est riche et complexe, mais Macaque s'appuie sur des types fantômes pour décorer des types de OCaml avec des informations relatives à SQL.
Pour l'avoir utilisé, Macaque est très utile mais discutablement agréable à utiliser. Par contre il offre le confort de la validation de requêtes syntaxiquement et logiquement.
Conclusion
Je terminerai cette brève présentation en limitant la notion de type fantômes
à "un (ou plusieurs) labels donnant des informations d'utilisations complémentaires
à des types". Cet étiquetage permet une vérification statique d'un bon usage des données.
Cependant, bien qu'amenant plus de sûreté dans nos programmes, les types fantômes peuvent parfois limiter l'expressivité et introduire, dans certains cas, des erreurs de typages
très complexes.