Type algébrique et GADT, en Haskell

Voir aussi : video youtube - video peertube - code source

Les types de données algébriques (ADT) sont des types composites très utiles dans des langages comme Haskell, Rust ou encore OCaml. Grossièrement, ils permettent à l’utilisateur de définir des types d’énumérations et des types de structures. En réalité, ils sont bien plus puissants que cela car ils supportent également le pattern-matching, la récursivité, du polymorphisme et même les types de données algébriques généralisés (GADT).

Cet article présente les ADT et les GADT en Haskell ainsi qu’un exemple d’utilisation classique.

Type algébrique (ADT)

Un type algébrique peut prendre différentes formes, présentées ci-dessous.

Type somme

Un type somme permet de définir les valeurs que peut prendre le type, à la manière d’une énumération.

data Couleur = Rouge | Vert | Bleu

Dans cet exemple, on définit un nouveau type Couleur, qui peut prendre les valeurs Rouge, Vert et Bleu. La cardinalité d’un type somme (c’est-à-dire le nombre total de valeurs que ce type peut représenter) est la somme des valeurs utilisées pour le définir, ici 3.

Ce type peut ensuite être utilisé dans le reste du code comme n’importe quel autre type en Haskell. Par exemple, on peut faire du pattern-matching pour définir une fonction selon les différentes valeurs du type.

toHtml :: Couleur -> String
toHtml Rouge = "#ff0000"
toHtml Vert = "#00ff00"
toHtml Bleu = "#0000ff"

main :: IO ()
main = do
    putStrLn $ toHtml Rouge     -- construit une valeur Rouge et appelle toHtml
    putStrLn $ toHtml Vert      -- idem avec la valeur Vert

Type produit

Un type produit permet de définir une valeur et de lui associer des données.

data Figure 
    = Rectangle Double Double

Dans cet exemple, on définit un nouveau type Figure qui peut prendre la valeur Rectangle. Cette valeur contient deux données de type Double. La cardinalité du type est donc le produit de celle des ensembles utilisés pour définir, ici c’est donc le carré de la cardinalité du type Double.

On peut ensuite faire du pattern-matching, pour déconstruire les données associées à la valeur Rectangle.

aire :: Figure -> Double
aire (Rectangle l h) = l * h

Enfin pour construire une valeur, il faut spécifier les données associées.

main :: IO ()
main = do
    let rect = Rectangle 21 2   -- construit une valeur Rectangle
    print $ aire rect           -- appelle la fonction aire sur la valeur construite

Type enregistrement

Les données associées à une valeur d’un type produit peuvent également être nommées.

data Figure 
    = Rectangle
        { _largeur :: Double
        , _hauteur :: Double
        }

Le nom de ces champs définit également des accesseurs.

aire :: Figure -> Double
aire r = _largeur r * _hauteur r

Type algébrique

Les types algébriques combinent les types sommes et les types produits. Plus exactement, un type algébrique est une somme de types produits.

data Figure 
    = Rectangle Double Double
    | Disque Double

Ici, le type Figure est la somme de la valeur Rectangle (qui comprend deux Double) et de la valeur Disque (qui comprend un Double).

Le pattern-matching fonctionne toujours de la même façon.

aire :: Figure -> Double
aire (Rectangle l h) = l * h
aire (Disque r) = pi * r**2

Type récursif

Les types algébriques peuvent être récursifs, c’est-à-dire qu’une valeur peut contenir un champs du type qu’on est en train de définir. Ceci est très pratique pour définir des arbres ou encore des listes.

data Liste
    = Fin
    | Element Int Liste

liste1 :: Liste
liste1 = Element 1 (Element 2 Fin)

Type polymorphe

Enfin, les types algébriques peuvent être polymorphes, c’est-à-dire paramétrés.

data Figure a
    = Rectangle a a
    | Disque a

Ici, le type Figure a est polymorphe. On peut donc l’utiliser pour représenter un type Figure Float où les champs de la valeur Rectangle sont de type Float, mais également un type Figure Double, où les champs seront de type Double, etc.

On notera, qu’il peut alors être nécessaire d’utiliser des contraintes sur ce paramètre selon son utilisation. Par exemple, la fonction aire suivante fait des calculs flottants, ce qui signifie qu’elle est définie pour tous les types Figure a où le type a est de classe Floating.

aire :: Floating a => Figure a -> a
aire (Rectangle l h) = l * h
aire (Disque r) = pi * r**2

main :: IO ()
main = do
    let rect = Rectangle 21 (2::Float)
        disq = Disque (1::Double)
    print $ aire rect
    print $ aire disq

Type algébrique généralisé (GADT)

Les “valeurs” d’un type algébrique peuvent être vues comme des constructeurs, c’est-à-dire des fonctions qui retournent des valeurs du type.

Un type algébrique généralisé est un type algébrique où on écrit explicitement le type des constructeurs. Par exemple, le type Figure a précédent peut s’écrire avec un GADT, de la façon suivante.

{-# LANGUAGE GADTs #-}

data Figure a where
    Rectangle :: a -> a -> Figure a
    Disque :: a -> Figure a

...

Ici, on a juste explicité les constructeurs donc ce GADT est équivalent à l’ADT précédent. Cependant, les GADT permettent de définir des constructeurs plus évolués. La section suivante en présente un exemple.

Exemple : expressions arithmétiques

Les ADT sont un outil déjà très puissant et permettent de répondre à de nombreux cas d’utilisation. Les GADT sont plus évolués mais ils sont intéressants pour des cas d’utilisation plus compliqués.

Pour illustrer l’intérêt des GADT, on considère le problème de représenter et d’évaluer des expressions arithmétiques. Il s’agit d’un exemple assez classique, également détaillé dans le Wikibook sur Haskell.

Avec des entiers uniquement

Dans un premier temps, on considère uniquement des nombres entiers et les opérations d’addition et de multiplication.

Avec un ADT, on définirait le type suivant :

data Expr
    = Val Int
    | Add Expr Expr
    | Mul Expr Expr

Et avec un GADT :

data Expr where
    Val :: Int -> Expr
    Add :: Expr -> Expr ->  Expr
    Mul :: Expr -> Expr ->  Expr

Dans les deux cas, l’utilisation du type Expr est la même. Par exemple, pour implémenter et tester la fonction d’évaluation :

eval :: Expr -> Int
eval (Val x) = x
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2

main :: IO ()
main = do
    print $ eval $ Val 21
    print $ eval $ Mul (Val 2)
                       (Add (Val 10) (Val 11))

Avec des entiers et des booléens

On veut maintenant gérer également des booléens et pouvoir tester l’égalité de deux expressions.

Avec un ADT, on peut ajouter une valeur pour représenter les booléens et une valeur pour représenter l’opérateur de comparaison.

data Expr
    = ValI Int
    | ValB Bool
    | Add Expr Expr
    | Mul Expr Expr
    | Equals Expr Expr
    deriving (Eq, Show)

La fonction d’évaluation doit alors prendre en compte les cas d’incompatibilité, par exemple, en générant une erreur.

eval :: Expr -> Expr
eval (Add e1 e2) = 
    case (eval e1, eval e2) of
        (ValI x1, ValI x2) -> ValI (x1 + x2)
        _ -> error "Add failed"
eval (Mul e1 e2) = 
    case (eval e1, eval e2) of
        (ValI x1, ValI x2) -> ValI (x1 * x2)
        _ -> error "Mul failed"
eval (Equals e1 e2) = ValB (eval e1 == eval e2)
eval x = x

Ici, la fonction eval est partielle. Il est donc possible d’écrire du code qui compile mais qui va échouer à l’exécution :

eval $ Equals (ValI 42) (Mul (ValI 2) (ValI 21))     -- ok

eval $ Equals (ValB True) (Mul (ValI 2) (ValI 21))  -- erreur à l'exécution

Avec un GADT, on peut définir un type polymorphe Expr a et préciser le type des valeurs construites :

data Expr a where
    ValI :: Int -> Expr Int
    ValB :: Bool -> Expr Bool
    Add :: Expr Int -> Expr Int -> Expr Int
    Mul :: Expr Int -> Expr Int -> Expr Int
    Equals :: Eq a => Expr a -> Expr a -> Expr Bool

Ainsi, l’addition et la multiplication sont restreintes aux types Expr Int, et la comparaison est contrainte à prendre deux paramètres de même type et à retourner un Expr Bool.

Tout ceci est vérifié par le compilateur, si bien qu’on n’a plus d’incompatibilité à gérer pour implémenter la fonction eval.

eval :: Expr a -> a
eval (ValI x) = x
eval (ValB x) = x
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Equals e1 e2) = eval e1 == eval e2

De même, les expressions invalides sont désormais détectées à la compilation, selon le principe consistant à rendre les états invalides impossibles à représenter.

eval $ Equals (ValI 42) (Mul (ValI 2) (ValI 21))     -- ok

eval $ Equals (ValB True) (Mul (ValI 2) (ValI 21))  -- erreur à la compilation

Conclusion

Un type algébrique permet de définir une “somme de types produits”. Concrètement, c’est un outil puissant, permettant d’implémenter des énumérations et des structures, avec de la récursivité, du polymorphisme, du pattern-matching… Les types algébriques généralisés permettent d’ajouter encore plus d’information aux types que l’on définit.