Type fantôme et datakind, pour sauver des sondes spatiales avec Haskell

Voir aussi : video youtube - video peertube - code source

Le 23 septembre 1999, la sonde Mars Climate Orbiter a été perdue. La cause de cet échec est l’utilisation d’unités de mesure différentes entre deux logiciels de la sonde. D’une façon plus générale, les types de base des langages de programmation portent assez peu d’information. Il est donc facile de confondre, par exemple, des Newton et des Livre-force si on les représente tous les deux par des Double.

Haskell possède un système de types évolué, qui permet de programmer “au niveau des types” (type-level). Ainsi, on profite automatiquement des vérifications du compilateur, ce qui évite de nombreuses erreurs potentielles, comme par exemple mélanger des unités de mesure.

Cet article présente quelques fonctionnalités de programmation type-level, comme les types fantômes et les datakinds, à partir d’une problématique initiale.

Problématique

Le problème traité ici est inspiré d’une question sur stackoverflow.

On veut écrire du code manipulant différentes unités de mesure : des distances en kilomètre ou en mille marin, et des vitesses en kilomètre par heure ou en noeud.

On veut notamment pouvoir calculer la vitesse, à partir d’une distance et d’une durée Si on représente ces informations par des Double, il suffit d’écrire la fonction suivante.

calculerVitesse :: Double -> Double -> Double
calculerVitesse dx dt = dx / dt

Malheureusement, on n’a aucune vérification sur les unités de mesure avec ce code. On peut par exemple mélanger des km/h et des noeuds, et ainsi obtenir un résultat faux mais ne générant aucune erreur, ni à la compilation, ni à l’exécution (il faut attendre la collision avec Mars).

main :: IO ()
main = do
    let d1 = 21                         -- km
        d2 = 11.33                      -- mille
        v1 = calculerVitesse d1 0.5     -- km/h
        v2 = calculerVitesse d2 0.5     -- noeud
    print v1
    print v2
    print $ v1 + v1     -- ok : on ajoute des km/h
    print $ v2 + v2     -- ok : on ajoute des noeuds
    print $ v1 + v2     -- erreur : le résultat est faux, et rien ne nous le dit

Solution avec des ADT

Une première solution est d’écrire un type algébrique pour définir une distance et un autre pour définir une vitesse (voire encore un autre pour définir une durée).

data Distance
    = Km Double
    | Mille Double
    deriving (Show)

data Vitesse
    = KmH Double
    | Noeud Double
    deriving (Show)

On peut ensuite implémenter la fonction calculerVitesse avec un pattern-matching, et construire une vitesse selon la distance donnée, avec la bonne unité de mesure.

calculerVitesse :: Distance -> Double -> Vitesse
calculerVitesse (Km dx) dt = KmH $ dx / dt
calculerVitesse (Mille dx) dt = Noeud $ dx / dt

Pour implémenter les calculs sur les vitesses, on peut instancier la classe Num pour le type Vitesse.

instance Num Vitesse where
    KmH x + KmH y = KmH (x + y)
    Noeud x + Noeud y = Noeud (x + y)
    _ + _ = error "Vitesse + Vitesse"

    ...

Ici aussi on peut utiliser le pattern-matching, par exemple pour vérifier qu’on ajoute bien deux vitesses de la même unité de mesure. Cependant, si on tente d’ajouter deux vitesses avec des unités de mesure différentes, on ne peut pas faire beaucoup mieux que générer une erreur d’exécution.

main :: IO ()
main = do
    let d1 = Km 21
        d2 = Mille 11.33
        v1 = calculerVitesse d1 0.5
        v2 = calculerVitesse d2 0.5
    print v1
    print v2
    print $ v1 + v1
    print $ v2 + v2
    print $ v1 + v2     -- erreur à l'exécution

Solution avec des GADT

Commençons par définir des types représentant simplement les notions d’unités de distance.

data Km
data Mille

On peut ensuite définir des types algébriques généralisés Distance a et Vitesse a. Ceci nous permet d’intégrer l’unité de distance, dans le paramètre de type a.

data Distance a where
    DistanceKm :: Double -> Distance Km
    DistanceMille :: Double -> Distance Mille

data Vitesse a where
    VitesseKmH :: Double -> Vitesse Km
    VitesseNoeud :: Double -> Vitesse Mille

Pour la fonction calculerVitesse, seule la signature change légèrement.

calculerVitesse :: Distance a -> Double -> Vitesse a
calculerVitesse (DistanceKm dx) dt = VitesseKmH $ dx / dt
calculerVitesse (DistanceMille dx) dt = VitesseNoeud $ dx / dt

En revanche, l’instance de la classe Num pour le type Vitesse a est plus simple et plus robuste car le GADT nous assure déjà qu’on ajoute des vitesses de même unité de mesure.

instance Num (Vitesse a) where
    VitesseKmH x + VitesseKmH y = VitesseKmH (x + y)
    VitesseNoeud x + VitesseNoeud y = VitesseNoeud (x + y)

    ...

instance Show (Vitesse a) where
    ...

Si on essaie d’ajouter des vitesses d’unités de mesure différentes, le compilateur détecte l’erreur. On a donc rendu un état invalide impossible à représenter, et ainsi supprimé toute une classe d’erreurs potentielles.

main :: IO ()
main = do
    let v1 = calculerVitesse (DistanceKm 21) 0.5
        v2 = calculerVitesse (DistanceMille 11.33) 0.5
    print v1
    print v2
    print $ v1 + v1
    print $ v2 + v2
    -- print $ v1 + v2      -- erreur à la compilation

Solution avec des types fantômes

Un type fantôme est un type algébrique polymorphe mais dont le paramètre de type n’est pas utilisé dans la définition de type. Ceci permet, d’intégrer de l’information dans le type lui-même, même si on ne l’utilise pas directement dans les valeurs.

Pour notre exemple, on peut donc définir des types pour les unités de distance et des types fantômes pour la distance et pour la vitesse. Pour rappel, newtype est équivalent à data mais avec un seul constructeur.

data Km
data Mille

newtype Distance a = Distance Double

newtype Vitesse a = Vitesse Double
    deriving (Num, Show)

Ici, Haskell est capable d’instancier automatiquement la classe Num. De même, la fonction calculerVitesse est plus simple car on a un seul constructeur et l’unité de mesure apparaitra simplement dans le paramètre de type.

calculerVitesse :: Distance a -> Double -> Vitesse a
calculerVitesse (Distance dx) dt = Vitesse $ dx / dt

Comme avec les GADT, le compilateur est capable de détecter des erreurs comme l’addition de vitesses d’unités différentes. A noter, qu’on doit ici préciser le “paramètre fantôme” du type car celui-ci n’est plus porté par le constructeur.

main :: IO ()
main = do
    let v1 = calculerVitesse (Distance 21 :: Distance Km) 0.5
        v2 = calculerVitesse (Distance 11.33 :: Distance Mille) 0.5
    print v1
    print v2
    print $ v1 + v1
    print $ v2 + v2
    -- print $ v1 + v2      -- erreur à la compilation

Solution avec types fantômes + datakinds

La solution précédente, avec les types fantômes, apporte déjà beaucoup de simplicité et de robustesse. Cependant, on n’a indiqué aucune restriction sur les types utilisables pour le “paramètre fantôme”.

Pour cela, Haskell propose la notion de sorte (en anglais : kind), c’est-à-dire le type d’un type. Par exemple, l’extension DataKinds permet de définir un type et ses valeurs, et de le promouvoir au niveau des types, c’est-à-dire utiliser ces valeurs comme des types.

Appliqué à notre exemple de calcul de vitesse, on peut définir un type UniteDistance de valeurs Km et Mille.

data UniteDistance = Km | Mille

On définit ensuite des types fantômes comme dans la solution précédente, mais en indiquant que le paramètre fantôme est de type UniteDistance (c’est-à-dire Km ou Mille uniquement).

newtype Distance (a :: UniteDistance) = Distance Double
    -- type polymorphe mais restreint aux unités de distance

newtype Vitesse (a :: UniteDistance) = Vitesse Double
    deriving (Num, Show)

La fonction calculerVitesse est identique à la solution précédente.

calculerVitesse :: Distance a -> Double -> Vitesse a
calculerVitesse (Distance dx) dt = Vitesse $ dx / dt

Enfin à l’utilisation, le compilateur vérifie maintenant également que le paramètre fantôme correspond à Km ou Mille, en plus de vérifier l’addition de vitesses d’unités identiques. A noter qu’on utilise Km et Mille comme des types alors qu’on les a définies comme des valeurs (du type UniteDistance). On dit qu’on fait de la promotion de valeur et on l’écrit 'Km et 'Mille.

main :: IO ()
main = do
    let v1 = calculerVitesse (Distance 21 :: Distance 'Km) 0.5
        v2 = calculerVitesse (Distance 11.33 :: Distance 'Mille) 0.5
    print v1
    print v2
    print $ v1 + v1
    print $ v2 + v2
    -- print $ v1 + v2      -- erreur à la compilation

Conclusion

Haskell fournit différentes fonctionnalités pour programmer au niveau des types, par exemple les types fantômes et les datakinds. Un type fantôme permet d’ajouter, dans le type, une information qui n’apparait pas dans la définition. Un datakind permet de promouvoir des valeurs au niveau des types.

Ceci permet de profiter du système de types de Haskell pour vérifier automatiquement la validité du code, toujours dans l’objectif de rendre les états invalides impossibles à représenter.