xavier-van-de-woestyne-initial
Xavier Van de Woestyne
Functional Programmer

Introduction aux types fantômes

09/05/2017

Présentation d'une utilisation amusante des types paramétrés avec le langage OCaml pour répondre à une problématique pouvant être très coûteuse.

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 type Measure.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 balise div. 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.