Introduction aux types fantômes

    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.

    Xavier Van de Woestyne

    Lire d'autres articles par cet auteur.