• # À propos du coté algébrique des ADT

    Posté par . En réponse à la dépêche Sortie de GHC 8.0.2 et une petite histoire de typage statique. Évalué à 4.

    ADT ?
    Il s’agit d’un croisement un peu douteux entre les struct, bien connus de nombreux langages de programmation, et les union, utilisés en C/C++ et qui sont une sorte d’enum. Le tout gonflé aux stéroïdes de la généricité, de la sécurité et du sucre syntaxique.

    C'est pas douteux du tout :-) c'est vraiment une algèbre sur les types.

    Si on a trois types, mettons Char, Int, et Bool, que l'on peut voir comme l'ensemble des caractères, l'ensemble des entiers, et {true,false}.

    On a l'opérateur | haskell qui permet de faire l'union de deux types, par exemple :

    data B_OU_I = B Bool | I Int

    et un opérateur implicite, qui permet de faire le produit cartésien :

    data C_ET_I = CI Bool Int
    -- on peut même expliciter cet opérateur, c'est , (virgule) (en ocaml c'est * )
    data C_ET_I = CI (Bool,Int)

    C'est bien une algèbre avec des propriétés cool :

    data Zero
    data Un = Un
    data NeutreUnion t = V Zero | C t
    -- la déclaration précédente est équivalente (isomorphe) à t (en fait c'est faux en haskell à cause des valeurs non définies, mais vrai en ocaml). Équivalent ça veut dire que vous pouvez écrire une fonction de NeutreUnion t dans t, et une de t dans NeutreUnion t telle que la composition des deux soit la fonction identité
    data NeutreProduit t = P t Un
    -- la déclaration précédente est aussi équivalente à t (c'est pas vrai non plus en haskell)
    -- On a des propriété d'associativité
    data Somme a b = A a | B a
    data Produit a b = P a b
    -- du style Somme a (Somme b c) est équivalent à Somme (Somme a b) c, idem pour le produit
    -- La distributivité, par exemple :
    type Personne = Produit Nom (Somme Homme Femme)
    -- est équivalent à 
    type Personne' = Somme (Produit Nom Homme) (Produit Nom Femme)

    Donc, tout ça, c'est vraiment une algèbre sur les types. Et là où c'est encore plus fort... c'est que c'est pas seulement une algèbre... C'est tout un langage :

    Quand j'écrivais :

    data Somme a b = Somme a b

    Ce Somme c'est une "fonction", au niveau des types. On lui donne deux types et elle en construit le type somme. Haskell permet aussi de faire des choses du genre :

    data ApplyTypeFun f a b = App (f a b)

    Donc là, le f c'est une fonction sur les type à deux paramètres. Par exemple, ça peut être la somme, le produit, une projection, une liste, un ensemble, l'opérateur (->). Ça permet d'écrire du code super générique, et c'est super cool.