Sortie de GHC 8.0.2 et une petite histoire de typage statique

Posté par  (site web personnel) . Édité par Davy Defaud, rogo, palm123, Benoît Sibaud, ZeroHeure, Ontologia, Anthony Jaguenaud, Nils Ratusznik et Lucas. Modéré par ZeroHeure. Licence CC By‑SA.
Étiquettes :
33
23
jan.
2017
Programmation fonctionnelle

GHC, le compilateur Haskell le plus utilisé, est sorti en version 8.0.2 ; vous pouvez consulter l’annonce de la sortie datée du 11 janvier 2017, ainsi que les notes de version.

Il s’agit principalement d’une version de suivi qui corrige plus de deux cents bogues depuis la version 8.0 dont l’annonce de la sortie avait été faite sur LinuxFr.org. Donc, à ce titre, il n’y a pas grand chose à raconter. Le futur, c’est GHC 8.2 qui devrait arriver aux environs d’avril, si l’on en croit le planning. Celle‐ci devrait apporter principalement des améliorations de performance de l’environnement d’exécution parallèle et du ramasse‐miettes.

Comme on frôle la dépêche bookmark et que je tiens à mon karma, je vais vous présenter une fonctionnalité de Haskell, que l’on retrouve dans de nombreux langages. J’ai nommé les ADT, ou types algébriques de données.

Sommaire

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.

Remarque : cette dépêche a été rédigée avec la chasse aux coquilles et les remarques bénéfiques de palm123, Anthony Jaguenaud, rogo et Lucas.

ADT : un struct

Un ADT c’est un type. Commençons d’abord par la partie qui ressemble à des struct. Si je veux concevoir un point à trois dimensions en Haskell, je ferai :

data Point = PointC Float Float Float deriving (Show)

Il s’agit de la déclaration du type Point. Ce type peut être construit grâce à un constructeur PointC qui prend trois Float et renvoie un Point. Le type de ce constructeur est PointC :: Float -> Float -> Float -> Point, une fonction qui prend un Float, puis un autre Float, et encore un Float et renvoie un Point. Le nom du constructeur est libre, il aurait très bien pu être le même que le nom du type.

La clause deriving (Show) sert à générer automatiquement des fonctions d’affichage qui respecteront la type class nommée Show.

Un petit exemple de cas d’utilisation dans le shell interactif GHCI :

Prelude> PointC 1 2 3
PointC 1.0 2.0 3.0
Prelude> PointC 4 5 6
PointC 4.0 5.0 6.0

Le constructeur PointC peut aussi servir à « déconstruire » (filtrage par motif, pattern matching) les valeurs quand il apparaît du côté gauche du signe = :

Prelude> PointC a b c = PointC 1 2 3
Prelude> a
1.0
Prelude> b
2.0
Prelude> c
3.0

Ceci est très pratique lors de la création de fonctions :

Prelude> getX (PointC x _ _) = x
Prelude> getY (PointC _ y _) = y
Prelude> getZ (PointC _ _ z) = z
Prelude> norm (PointC x y z) = sqrt (x * x + y * y + z * z)
Prelude> p = PointC 1 2 3
Prelude> getX p
1.0
Prelude> getY p
2.0
Prelude> getZ p
3.0
Prelude> norm p
3.7416575

Nous avons donc vu qu’un type en Haskell peut être vu comme un struct ou un objet dans d’autres langages, c’est‐à‐dire un agrégat de champs de types hétérogènes. Si cela vous inquiète, on peut aussi donner des noms aux champs :

data Point = Point {x :: Float, y :: Float, z :: Float}

Dans ce cas, appelé Record en Haskell, une nouvelle contrainte apparaît : les noms (x, y et z) des champs doivent être uniques dans le module Haskell, à moins de recourir à des extensions du compilateur. Mais ceci est une autre histoire, qui est en train de s’écrire.

ADT : un enum

Les enum dans de nombreux langages permettent de créer un type pouvant être représenté par plusieurs valeurs. L’exemple d’école :

data Couleur = Rouge | Vert | Bleu | Marron | Noir | Blanc deriving (Show)

Ici nous avons créé le type Couleur et nous lui avons associé six constructeurs différents. Observez bien le | entre les constructeurs, il représente l’alternative.

L’usage du nom  « constructeur » ici est souvent troublante pour qui n’y est pas habitué. Dites‐vous simplement que Rouge est une fonction qui ne prend pas d’argument et renvoie une valeur de type Couleur. En ce sens, c’est un constructeur de Couleur.

On peut utiliser ces constructeurs pour créer des objets de type Couleur :

Prelude> Rouge
Rouge
Prelude> Bleu
Bleu

On peut aussi réaliser différentes opérations dessus grâce à de la déconstruction, comme vu précédemment. Dans la fonction réaction qui suit, je liste les différents cas de couleur, le _ servant de joker. En Haskell, on peut définir des fonctions en listant les cas :

réaction Rouge = "Cool"
réaction Bleu = "Cool aussi, mais je préfère le rouge"
réaction Vert = "Bof bof"
réaction Noir = "Moche"
-- cas générique (le compilateur impose l'exhaustivité)
réaction _ = "Je n'aime pas les autres couleurs"

Et l’usage dans l’interpréteur nous donne :

Prelude> réaction Rouge
"Cool"
Prelude> réaction Blanc
"Je n'aime pas les autres couleurs"

Nous avons vu comment réaliser en Haskell l’équivalent des enum que l’on peut trouver dans d’autres langages.

ADT : enum avancés, ou union

Le C et le C++ proposent un mécanisme d’union, où un type peut contenir au choix plusieurs sous‐types. Par exemple :

union Forme
{
     struct {
          float cote;
     } carre;

     struct {
          float coteA;
          float coteB;
     } rectangle;
};

Je ne reviendrai pas sur son usage en C, sachez seulement que le type Forme peut contenir soit un float cote, soit deux float coteA et coteB. L’usage des deux simultanément est indéfini et on ajoute souvent à la structure de donnée un marqueur pour informer l’utilisateur du type de la donnée réellement stockée.

En haskell, ce type peut être facilement représenté par un ADT combinant struct (ou type « produit ») et enum (ou type « somme ») :

data Forme = Carré Float | Rectangle Float Float deriving (Show)

Ici nous avons un type Forme qui contient deux constructeurs :

  • Carré, qui associe un Float à une Forme ;
  • Rectangle, qui associe deux Float à une Forme.

Contrairement aux langages qui supportent les enum où les unions, on remarque notamment que n’importe quel type complexe peut apparaître dans les différents cas de l’énumération.

Les outils décrits précédemment de construction et de déconstruction par analyse de cas fonctionnent également. Ainsi, on peut créer des Forme :

Prelude> Carré 10
Carré 10.0
Prelude> Rectangle 20 30
Rectangle 20.0 30.0

Et l’on peut faire des fonctions qui vont traiter notre type par analyse de cas :

surface (Carré c) = c * c
surface (Rectangle a b) = a * b

Ici, la fonction surface déconstruit un Carré et renvoie sa surface. Si la déconstruction n’est pas possible (car c’est un Rectangle), alors la fonction passe au cas suivant). À l’usage :

Prelude> surface (Carré 10)
100.0
Prelude> surface (Rectangle 5 3)
15.0

Plusieurs remarques :

  • le compilateur nous protège et ce de plusieurs manières :
    • si j’avais oublié de gérer les cas Rectangle, le compilateur m’aurait prévenu,
    • contrairement aux unions en C/C++, on ne peut pas confondre un Rectangle et un Carre, c’est de nombreuses heures de recherche d’erreurs qui disparaissent soudainement ;
  • la syntaxe et l’usage sont succincts, c’est agréable à mon goût ; la même chose est possible dans de nombreux langages, par exemple en C++, grâce à l’utilisation de « variant », mais l’usage est lourd. Comparez le programme entier en Haskell à la version C++ :
data Forme = Carré Float | Rectangle Float Float

surface (Carré c) = c * c
surface (Rectangle a b) = a * b

main = do
   let carré = Carré 10
       rectangle = Rectangle 5 3

   print (surface carré)
   print (surface rectangle)

La version C++ équivalente suivante utilise boost::variant, en c++17 nous utiliserons std::variant :

#include <iostream>
#include <boost/variant.hpp>

struct Carre
{
    float c;
};

struct Rectangle
{
    float a;
    float b;
};

using Forme = boost::variant<Carre, Rectangle>;

class surface
{
public:
    float operator()(const Carre &carre) const
    {
        return carre.c * carre.c;
    }

    float operator()(const Rectangle &rectangle) const
    {
        return rectangle.a * rectangle.b;
    }
};

int main()
{
    Forme carre = Carre{10};

    Forme rectangle = Rectangle{5, 3};

    // affiche 100
    std::cout << boost::apply_visitor(surface(), carre) << std::endl;
    // affiche 15
    std::cout << boost::apply_visitor(surface(), rectangle) << std::endl;
}

Ce code passe par la définition du type en trois étapes : définition des sous‐types Carre et Rectangle et définition du type Forme comme un variant, un choix, entre les deux précédents types.

La classe surface est ici un visiteur qui propose une surcharge de l’opérateur float operator(const T &t) pour chaque sous‐type T que peut contenir notre variant.

La fonction boost::apply_visitor est chargée d’appeler la bonne surcharge de l’opérateur operator() de surface en fonction du contenu du variant passé en second paramètre.

ADT : exemple plus poussé

Alors, pourquoi je vous raconte tout cela ? En premier lieu, j’aime bien. En second lieu, je me dis que cela peut vous intéresser à Haskell ou au moins vous sensibiliser à l’existence de ce type d’outil et peut‐être que vous les utiliserez dans vos projets futurs. Par exemple, dans mon travail quotidien, je fais du C++, mais Haskell m’a beaucoup influencé et j’utilise tous les jours des boost::variant. Mon opinion là‐dessus c’est que, même si la syntaxe en C++ est verbeuse à souhait, cela sauve de certaines situations. Au final, je pense que le code est plus robuste.

Pour finir, je vais vous donner un exemple d’un problème que je rencontre souvent dans des API et qui serait, à mon sens, mieux traité avec des ADT. C’est le cas traditionnel des valeurs sentinelles. Je fais un peu concurrence au journal de cette semaine sur la prévention de bogues en Ocaml grâce à un typage plus strict. Là où ce journal s’intéressait à la définition d’un type synonyme mais incompatible, je m’intéresse à la définition d’un type totalement différent permettant de représenter un contexte différent et ainsi de supprimer les cas impossibles et de rendre plus robustes les cas possibles.

Introduction

Pour appuyer mon propos, intéressons‐nous à une bibliothèque C++ que j’utilise tous les jours, OpenEXR, qui permet, entre autres, de lire et d’écrire des images au format EXR, très utilisé dans l’industrie de l’image (Cf. la page GitHub d’OpenEXR.

Cette bibliothèque propose, entre autres, la lecture et l’écriture de fichiers via plusieurs fils d’exécution, ce qui est une fonctionnalité très pratique quand l’écriture de plusieurs gigaoctets d’images en séquentiel est le facteur limitant sur des machines à 24 cœurs.

Le point de l’API qui nous intéresse est le suivant : les fonctions setGlobalThreadCount et globalThreadCount :

void setGlobalThreadCount (int count);
int globalThreadCount();

Alors, si l’on lit la documentation, on peut voir que count dans setGlobalThreadCount sert à définir le nombre de fils d’exécution utilisés globalement pour réaliser les écritures.

En cherchant un peu, on tombe sur ce commentaire :

The functions in this file query and control the total number
of worker threads, which will be created globally for the whole
library. Regardless of how many input or output files are
opened simultaneously, the library will use at most this number
of worker threads to perform all work. The default number of
global worker threads is zero (i.e. single‐threaded operation;
everything happens in the thread that calls the library).

Traduction à l’arrache :

La fonction setGlobalThreadCount contrôle le nombre total de fils d’exécution […] la bibliothèque utilisera au maximum ce nombre de fils d’exécution. Le nombre par défaut est zéro, ce qui signifie que les opérations ne seront pas parallélisées.

On tombe aussi sur des discussions GitHub intéressantes, dont je ne trouve plus le lien, désolé, traitant du moyen de fournir à setGlobalThreadCount une valeur qui correspond au nombre optimal de fils d’exécution système (sans avoir à trouver celui‐ci, on peut imaginer qu’il puisse changer à la volée en fonction de la charge de la machine, ou dans un environnement virtualisé, en fonction des besoins), et les débats tournaient autour du fait de mettre -1 comme nombre de fils d’exécution pour ce cas de figure. Ce n’est pas implémenté à ma connaissance dans openEXR, mais supposons que cela le soit.

Donc, en gros, voici le comportement que nous pouvons imaginer pour setGlobalThreadCount(n) :

  • si n > 0, alors c’est le nombre de fils d’exécution utilisé globalement ;
  • si n = 0, alors il n’y aura pas d’exécution parallélisée  ;
  • si n = -1, alors on utilise le nombre de fils d’exécution de la machine ;
  • si n = -12, autre cas particulier que nous pourrions imaginer.

Le problème

Premier problème, en tant qu’utilisateur, je n’avais pas conscience de l’existence des cas 0, -1 et -12, sans lire le code source et la documentation d’OpenEXR.

Second problème, on va se planter, largement, en beauté. Qui ? Les développeurs d’OpenEXR sans doute, et moi, en utilisant leur API. Comment je le sais ? Parce que je me suis planté.

Où pouvons‐nous nous planter ? Partout où le nombre global de fils d’exécution est utilisé. Si le cas particulier 0, -1 et -12 n’est pas géré explicitement, eh bien c’est un bogue. Cela peut faire des choses marrantes, par exemple créer 0 fil d’exécution de travail et répartir le travail entre eux, ce qui donne un blocage de l’application.

Troisième problème, le futur. Même si c’est bien géré actuellement, que se passera‐t‐il demain lorsque quelqu’un va écrire une nouvelle fonction basée sur cette valeur sans connaître l’existence des cas particuliers possibles ? Eh bien, cela va marcher, jusqu’à ce que quelqu’un utilise un cas particulier non traité. Et, là, pan ! Ou si quelqu’un ajoute un nouveau cas particulier et ne le gère pas à tous les endroits nécessaires.

On peut aussi se planter en passant une mauvaise constante par erreur. Imaginons qu’il existe dans le même espace de noms, une constante nommée NoThreading, mais utilisée par une autre bibliothèque et ayant pour valeur magique un entier. Si celui‐ci est négatif, c’est le drame, le comportement du programme est largement indéfini, au mieux c’est une erreur à l’exécution, au pire, c’est l’inconnu total. Si celui‐ci est positif, il faut espérer qu’il ne soit pas trop gros, car je n’aimerais pas créer 100 000 fils d’exécution sur ma machine de production, le système d’exploitation ne tiendrait pas.

Ce type de bogue potentiel rend la montée de version sur un gros projet logiciel difficile, du fait de la peur des régressions. Et même le meilleur système de test unitaire ne peut rien garantir à ce sujet.

Je passe aussi sur le problème de documentation et de lecture de code avec l’utilisation de constantes magiques en paramètres de fonction. setGlobalThreadCount(-123) n’est pas très informatif. Alors, oui, cela se règle avec des définitions de constantes, mais on peut encore se tromper, en définissant la constante à une mauvaise valeur, et rien ne force le développeur à utiliser la constante magique.

Ce problème est présent de partout, dans toutes les bibliothèques que nous utilisons, dans tous les langages que nous utilisons. Ceux‐ci proposent des valeurs sentinelles. Python avec la méthode find des chaînes de caractères, qui renvoie -1 si la chaîne n’est pas trouvée (il y a la version avec exception, c’est moins mauvais). C++ avec la fonction std::find qui retourne un itérateur vide en cas d’échec et rien qui ne vous force à tester cela.

La solution

La solution passe par la définition d’un type représentant le problème plus finement. Dans le cas d’OpenEXR, et si celui‐ci était écrit en Haskell, nous pourrions avoir un type :

-- Word est le type pour un entier non signé
data PolitiqueThread = NombreFixé Word | NombreMaximumHardware | PasDeThreading | CasParticulier

Ainsi, on pourrait appeler la fonction setGlobalThreadCount de différentes façons :

setGlobalThreadCount (NombreFixé 8)

setGlobalThreadCount NombreMaximumHardware

setGlobalThreadCount PasDeThreading

setGlobalThreadCount CasParticulier

Nous réglons en premier lieu le problème de documentation lors de l’appel. En tant qu’utilisateur, je suis forcé de voir que ce n’est pas juste un entier et d’au moins voir la documentation avec la liste des cas, qui est automatiquement à jour. Le code est lisible et il est explicite que cette valeur n’est pas anodine.

Nous réglons aussi le problème lors de l’usage. On ne peut plus utiliser les valeurs -1 et -12 et 0 par erreur en considérant qu’il s’agit d’un nombre de fils d’exécution et non pas d’un cas particulier, car le langage nous force à déconstruire et à gérer les différents cas de déconstruction. Observez comment 0, -1 et -12 n’apparaissent pas :

threadCount <- getGlobalThreadCount
case threadCount of
   NombreFixé n -> "nombre fixé à " ++ show n
   NombreMaximumHardware -> "Fait chauffer la ferme de calcul"
   PasDeThreading -> "Plutôt tranquille"
   CasParticulier -> "Celui-ci je ne l'aime pas"

Nous réglons aussi le problème de l’évolution future et de l’ajout de nouveaux cas particuliers, puisque le compilateur va protester aux endroits où tous les cas ne sont pas gérés.

Le problème de passer une valeur qui n’a pas de sens par défaut n’existe plus non plus. Le type PolitiqueThread est incompatible avec un autre type.

Grâce aux types algébriques, le gain de clarté et de fiabilité du code est donc important. Si les ingénieurs travaillant pour Mars Climate Orbiter avaient utilisé un mécanisme ADT comme type distance = Meters Float | Inches Float, ils n’auraient pas pu se tromper d’unité et les sept années de travail international sur la sonde n’auraient pas abouti à une bête galette métallique dans un cratère de Mars.

Imperfection résiduelle

La seule erreur possible reste de passer un nombre qui n’a pas de sens à NombreFixé. Soit un nombre négatif, soit un nombre trop grand qui ferait exploser le système.

Je n’ai pas de solution parfaite à ce dernier problème. On peut en premier lieu cacher le constructeur NombreFixé et le remplacer par une fonction type :

nombreFixé n
 | n > 0 && n < maximumThread = NombreFixé (fromIntegral n)
 | otherwise = erreurRuntime ("n est trop bizarre: " ++ show n)

-- fromIntegral sert à convertir n qui est un entier signé vers un `Word`.

Cette solution limite la casse. Il y en d’autres. On pourrait par exemple utiliser de l’analyse statique de code en imposant des contraintes sur nombreFixé. Liquid Haskell sait faire cela, mais dans un contexte limité.

Conclusion

En profitant de la sortie de GHC 8.0.2, j’ai essayé de vous sensibiliser un peu plus au problème des valeurs sentinelles. À mon sens, ce problème est grave, car il en découle du code peu lisible, peu « naturellement » documenté, peu robuste à l’évolution et peu robuste à l’utilisation normale par un développeur qui ne connaît pas par cœur les détails de l’API qu’il utilise. Une solution est l’emploi des ADT. Ceux‐ci sont disponibles dans de nombreux langages, comme Haskell, Caml, Rust, Scala, Swift, etc., et peuvent plus ou moins facilement être remplacés par des structures équivalentes à la simplicité près, comme avec les variant en C++.

Ce que je vous ai montré n’est qu’une partie de ce qui est possible avec les ADT, et un lecteur motivé pourra commencer sa lecture sur la section de Wikipédia consacrée aux ADT généralisés.

Aller plus loin

  • # Data.Natural

    Posté par  (site web personnel) . Évalué à 3.

    Tu pourrais passer un Data.Natural à NombreFixé, pour avoir toujours un nombre positif. Ou (et c'est très laid) tu pourrais passer une liste, et en utiliser la taille :)

  • # Solution à base de types variants en ADA

    Posté par  (site web personnel) . Évalué à 7.

    Par rapport à ton exemple, je pense qu'ADA propose également des solutions robustes du point de vu typage (et c'est un peu l'objectif de ce langage…).

    Le code

    WITH Ada.Text_IO;
    USE Ada.Text_IO;
    
    PROCEDURE Variant IS
    
       TYPE PolitiqueThreadCase IS
             (NombreFixe,
              NombreMaximumHardware,
              PasDeThreading,
              CasParticulier);
    
       TYPE PolitiqueThread (Politique : PolitiqueThreadCase := PasDeThreading) IS
       -- valeur par défaut obligatoire
       RECORD
          CASE Politique IS
             WHEN NombreFixe =>
                NombreThread : Positive; -- alias pour : Integer RANGE 1..Integer'Last
             WHEN OTHERS =>
                NULL;
          END CASE;
       END RECORD;
    
       PROCEDURE TestPolitique (Pol : IN PolitiqueThread) IS
       BEGIN
          CASE (Pol.Politique) IS
             WHEN NombreFixe =>
                Put_Line("Nombre fixé à" & Integer'Image(Pol.NombreThread));
             WHEN NombreMaximumHardware =>
                Put_Line("Fait chauffer la ferme de calcul");
             WHEN PasDeThreading =>
                Put_Line("Plutôt tranquille");
             WHEN CasParticulier =>
                Put_Line("Celui-ci je ne l'aime pas");
          END CASE;
       END TestPolitique;
    
       MaPolitique : PolitiqueThread;
    
    BEGIN
       TestPolitique(MaPolitique); -- Par défaut : PasDeThreading
       MaPolitique := (NombreFixe, 8);
       TestPolitique(MaPolitique);
       MaPolitique := (Politique => NombreMaximumHardware);
       TestPolitique(MaPolitique);
       MaPolitique := (Politique => CasParticulier);
       TestPolitique(MaPolitique);
       MaPolitique := (NombreFixe,  0); -- Warning: "Constraint Error will be raised at Runtime"
    
    EXCEPTION
       WHEN CONSTRAINT_ERROR =>
          Put_Line("n est trop bizarre...");
    
    END Variant;

    Le résultat

    Plutôt tranquille
    Nombre fixé à 8
    Fait chauffer la ferme de calcul
    Celui-ci je ne l'aime pas
    n est trop bizarre...
    

    Exceptions

    Donc, ça permet de gérer automatiquement le cas d'une valeur négative. Ada permet d'ajouter très simplement des tests au Runtime avec l'option RANGE. Très utile pour les tableaux également. Si l'on souhaite privilégier la performance, il est aussi possible de compiler en désactivant ces tests à l'exécution :

    pragma Suppress( Range_Check );

    On a droit également à une exception si on tente d'accéder ou de modifier un champ alors que le discriminant n'est pas le bon :

    MaPolitique := (Politique => CasParticulier);
    MaPolitique.NombreThread := 5; -- CONSTRAINT_ERROR : discriminant check failed

    La solution Ada est comme souvent un peu verbeuse, mais garde une bonne lisibilité.

    • [^] # Re: Solution à base de types variants en ADA

      Posté par  (site web personnel) . Évalué à 4.

      J'ai pas trop de souci avec la verbosité d'ADA (Que je découvre en lisant ton code). Je suis plus embêté par le concept de devoir fournir un cas par défaut pour un type comme tu le laisse supposer en commentaire. Cela veut dire qu'ADA, si tu n'initialise pas explicitement ta valeur, va prendre le choix par défaut ? Je n'aime pas ;)

      On a droit également à une exception si on tente d'accéder ou de modifier un champ alors que le discriminant n'est pas le bon :

      MaPolitique := (Politique => CasParticulier);
      MaPolitique.NombreThread := 5;—CONSTRAINT_ERROR : discriminant check failed

      Il n'y a pas de garantie statique sur ce genre de chose ? Ça c'est dommage.

      Les range, c'est sympa que le langage propose cela de façon native, mais au final cela s'émule assez bien dans n'importe quel autre langage avec un peu de typage dépendant.

      Par exemple, en Haskell :

      {-# LANGUAGE KindSignatures, DataKinds, TypeApplications, ScopedTypeVariables #-}
      import GHC.TypeLits
      import Control.Exception (assert)
      import Data.Proxy
      
      newtype Range (a :: Nat) (b :: Nat) = RangeVal Integer deriving (Show)
      
      newValInRange :: forall a b. (KnownNat a, KnownNat b) => Integer -> Range a b
      newValInRange i = assert (i >= bMin && i <= bMax) (RangeVal i)
        where bMin = natVal @a Proxy
              bMax = natVal @b Proxy

      C'est assez verbeux et incompréhensible pour l’œil non habitué, donc en gros, si on passe les import et LANGUAGE nécessaires. On a une définition de type Range, paramétrée par deux types "phantoms", bMin et bMax qui représentent les borne du range, mais ces valeurs sont stockées au niveau du type. Cependant la valeur stockée ne peut pas être contrainte, donc on stock un Integer dedans.

      Tous le problème se résume maintenant à empêcher la création d'un Range sans passer par une procédure de vérification. Pour cela on n'exportera pas le constructeur RangeVal, à la place, on va exporter la fonction newValInRange. Son type est assez barbare, newValInRange :: forall a b. (KnownNat a, KnownNat b) => Integer -> Range a b, mais en gros elle prend un Integer et renvoie un Range a b. Le truc c'est que on va se servir du a et b attendus (au niveau du type) pour déduire la vérification au niveau valeur.

      La ligne assert (i >= bMin && i <= bMax) (RangeVal i) se contente de renvoyer notre Integer bien encapsulé dans un RangeVal, mais après avoir testé qu'il est bien dans les bornes, en se servant de bMin = natVal @a Proxy pour transformer le type a, Integer au niveau du type, vers la valeur bMin, integer au niveau valeur.

      Après cela s'utilise comme cela. Imaginons la fonction suivante qui accepte un Range 0 10 :

      launchMissile :: Range 0 10 -> IO ()
      launchMissile r = case getValInRange r of
        0 -> putStrLn "Paix et harmonie"
        n -> putStrLn (unwords (replicate (fromInteger n) "EXTERMINATE!"))

      qui se sert entre autre de la fonction utilitaire getValInRange (RangeVal i) = i qui permet d'extraire l'Integer du range.

      Alors, nous obtenons :

      *Main GHC.TypeLits> launchMissile (newValInRange 0)
      Paix et harmonie
      
      *Main GHC.TypeLits> launchMissile (newValInRange 10)
      EXTERMINATE! EXTERMINATE! EXTERMINATE! EXTERMINATE! EXTERMINATE! EXTERMINATE! EXTERMINATE! EXTERMINATE! EXTERMINATE! EXTERMINATE!
      
      *Main GHC.TypeLits> launchMissile (newValInRange 11)
      *** Exception: Assertion failed
      CallStack (from HasCallStack):
        assert, called at range.hs:9:19 in main:Main

      On note que l’inférence de type fait son boulot et déduit tout seul que le résultat de newValInRange doit être un Range 0 10.

      Mais bon, c'est une usine à gaz de typage dépendant pour au final avoir une erreur au runtime, donc c'est assez inutile, on pourrait remplacer la même chose par un bête check dans la fonction launchMissile.

      Ce qui est par contre intéressant c'est quand on peut faire tout ce processus à la compilation. Par exemple, une fonction launchMissile qui connait son nombre de missile à la compilation et peut faire des vérifications statiques dessus :

      launchMissile' :: forall (n :: Nat). (KnownNat n, 0 <= n, n <= 10) => IO ()
      launchMissile' = case natVal @n Proxy of
        0 -> putStrLn "Paix et harmonie"
        n -> putStrLn (unwords (replicate (fromInteger n) "EXTERMINATE!"))
      

      (Cette solution demande les extensions TypeOperators, ConstraintKinds, TypeFamilies, AllowAmbiguousTypes, rien que ça, et aussi le package typelits-witnesses et l'import de 'GHC.TypeLits.CompareetData.Type.Bool.) IcilaunchMissile'est une fonction qui est paramétrée parnà la compilation, donc c'est à la compilation que l'erreur surn` pétera.

      Bon, çà c'est vachement plus simple en C++, qui gère super bien le typage dépendant sur les entiers et vivent les constexpr :

      template<int n>
      void launchMissile2()
      {
          static_assert(n >= 0 && n <= 10, "WTF!");
      
          if(n == 0)
              std::cout << "Paix et harmonie\n" << std::endl;
          else
              for(auto i = 0u; i < n; ++i)
              {
                  std::cout << "EXTERMINATE!\n";
              }
      }
      
      constexpr int fact(const int n)
      {
          int res = 1;
          for(int i = 1; i <= n; i++)
          {
              res *= i;
          }
      
          return res;
      }
      
      int main()
      {
          launchMissile2<fact(3)>(); // lance 3! == 6 missiles
      }

      (Bon, le c++ c'est bon des fois, constexpr déchire très souvent, jusqu'à ce que tu veuilles créer des valeurs plus poussées au niveau du type. ;)

      Aller, dodo.

      • [^] # Re: Solution à base de types variants en ADA

        Posté par  (site web personnel, Mastodon) . Évalué à 2.

        Déjà, je me permets de renvoyer vers un excellent commentaire sur ton journal… Le mien :D

        Je suis plus embêté par le concept de devoir fournir un cas par défaut pour un type comme tu le laisse supposer en commentaire

        En fait, c'est normal que cela t'embête puisque c'est faux.
        C'est la partie que j'avais laissée à l'appréciation du lecteur quand je parlais de mutabilité et qui se trouve décrite ici.
        Lorsque l'on ne précise pas de discriminant par défaut, le type est immuable de facto, il faut définir le discriminant à la déclaration. Il devient alors impossible de changer de discriminant en cours de route et donc, il est impossible d'accéder à un composant qui n'est pas disponible et c'est vérifié à la compilation :)

        • [^] # Re: Solution à base de types variants en ADA

          Posté par  (site web personnel, Mastodon) . Évalué à 3.

          c'est vérifié à la compilation

          Petite correction, c'est effectivement juste un avertissement mais bon, les warnings en Ada, il vaut mieux les écouter ;)

        • [^] # Re: Solution à base de types variants en ADA

          Posté par  (site web personnel) . Évalué à 1.

          Déjà, je me permets de renvoyer vers un excellent commentaire sur ton journal… Le mien :D

          Désolé Blackknight, je n'avais pas lu le journal à l'origine de la dépêche. Mon exemple est effectivement plutôt redondant avec le tien. Mais ça fait toujours plaisir de voir d'autres personnes coder en Ada. On se sent moins seul !

          Lorsque l'on ne précise pas de discriminant par défaut, le type est immuable de facto

          C'est vrai que j'ai passé sous silence le cas immuable, parce qu'un variant immuable, bon ben… en fait ça ne varie plus trop (blague, pas taper svp).

          Mais je reconnais que lorsqu'on code en Haskell, on a plutôt le réflexe de l'immuabilité, comme souvent avec les langages fonctionnels.

      • [^] # Re: Solution à base de types variants en ADA

        Posté par  . Évalué à 3.

        Concernant les ranges, que dirais-tu du module Ranged-sets ?

        {-# LANGUAGE GeneralizedNewtypeDeriving #-}
        
        -- Module 'Ranged-sets'
        import Data.Ranged.Boundaries
        import Data.Ranged.Ranges
        import Data.Ranged.RangedSet
        
        newtype Fusées = F Integer deriving (Num, Ord, Eq, DiscreteOrdered, Show)
        
        class PrêtePourLaRampe a where
            délivrerFeuVert :: a -> RSet a
        
        instance PrêtePourLaRampe Fusées where
            délivrerFeuVert x = rSetIntersection
                ( makeRangedSet [Range (BoundaryBelow 0) (BoundaryAbove 10)] )
                ( rSingleton x )
        
        launchMissile'' :: Fusées -> Maybe String
        launchMissile'' x
            | not $ rSetIsEmpty $ délivrerFeuVert x = Just $ show x
            | otherwise                             = Nothing
        
        main :: IO()
        main = do
            putStrLn $ show $ launchMissile'' . F <$> [10, 0, 7, negate 11, 17]
            -- Si on n'a pas de GHC sous la main, les sorties devraient ressembler à ça:
            -- [Just "F 10",Just "F 0",Just "F 7",Nothing,Nothing]

        Ça semble ne pas être usine à gaz et ce petit exemple est plutôt lisible en n'ayant que quelques notions dans le langage.

        • [^] # Re: Solution à base de types variants en ADA

          Posté par  (site web personnel) . Évalué à 4.

          Merci, je ne connaissais pas ce module. Après la complexité est cachée dans le module, on pourrait tout aussi bien mettre mon implémentation de Range dans un module et la complexité ne serait plus aussi visible.

          Ton approche avec un Maybe est clairement préférable à la mienne qui est basée sur des exceptions. Par contre, lire la ligne de putStrLn m'a demandé un effort du fait des priorités des opérateurs. Pour ceux qui ont du mal, cela se lit putStrLn (show ((launchMissile'' . F) <$> [10, 0, 7, negate 11, 17])). Généralement quand j'ai plus d'un opérateur infix non trivial dans la même ligne, je met des parenthèses explicites.

          • [^] # Re: Solution à base de types variants en ADA

            Posté par  . Évalué à 2.

            Réserve partagée sur l'abus d'opérateurs ; cela dit, les parenthèses à la Lisp ne demandent pas de moindres efforts non plus. Dans le cas présent, on peut éliminer l'alias du functor et expliciter fmap, voire éviter le lifting et utiliser tout simplement map qui est devenu un idiome répandu dans moult langages. Bref :

            putStrLn $ show $ map (launchMissile'' . F) [10, 0, 7, negate 11, 17]

            À part ça, oui la complexité est refoulée dans le module et à mon sens, c'est le chemin à suivre. Consommer facilement les APIs de modules bien conçus devrait se faire sans modération et sans se prendre la tête avec leurs cuisines internes. Lorsqu'on voudra être à la baguette soi-même, là on pourra alors se farcir les détails. Après tout, de nos jours, même les compilateurs sont des modules et ce ne serait pas raisonnable de s'en passer en prétextant qu'ils nous cachent de la complexité.

            P.S. De rien sur l'indication de Ranged-sets, c'est moi qui te remercie pour tes efforts constants de vulgarisation sur Haskell en particulier et, plus généralement, sur le fonctionnel : ces choses-là ne devraient pas avoir le statut confidentiel qu'elles apparaissent avoir actuellement et les efforts comme les tiens contribuent beaucoup à faire évoluer la situation.

            • [^] # Re: Solution à base de types variants en ADA

              Posté par  . Évalué à 3. Dernière modification le 26 janvier 2017 à 18:49.

              Réserve partagée sur l'abus d'opérateurs ; cela dit, les parenthèses à la Lisp ne demandent pas de moindres efforts non plus.

              C'est sans doute une question d'habitude. Je ne connais pas les règles de précédences des opérateurs infixes en Haskell mais, à partir des types des fonctions et des constructeurs, j'ai eu plus de facilité à lire ta version à celle avec parenthèses. J'ai du relire une deuxième (voire troisième) fois la version à la lisp pour bien me repérer; là où j'ai compris ton code à la première lecture.

              Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

              • [^] # Re: Solution à base de types variants en ADA

                Posté par  . Évalué à 2.

                C'est sans doute une question d'habitude.

                Tout à fait ! Ce bon vieux Lisp a le trépas difficile, sinon ça m'est également plus facile de lire un code écrit comme on l'a pensé. Mais peut-être que, du point de néophytes dans le langage, sur-usiter d'opérateurs infixés laisse l'impression qu'on jargonne et mes réserves concernaient ce cas de figure : si un certain style est un frein à la propagation de ce paradigme, autant lisser la courbe d'apprentissage en en adoptant un autre. Ça va dans le même sens que ta remarque d'il y a quelques mois :

                « […] je ne suis pas partisan du jargon employé fréquemment dans le monde de la programmation fonctionnel […]»

                Quant aux règles de précédence, le compilateur interactif GHCi est d'une grande aide. Dès qu'il laisse passer quelque chose, il suffira de lui demander ce qu'il en connaît via les commandes :type <machin>, :info <machin> ou :kind <machin>.

                -- N.B. Il y a élision volontaire de certaines sorties pour aller directement à la fixité.
                
                Prelude> :info $
                infixr 0 $
                
                Prelude> :info .
                infixr 9 .
                
                Prelude> :info <$>
                infixl 4 <$>

                La précédence est accordée suivant l'ordre décroissant de fixité infix<TRUC><TRUC> indique si l'opérateur est liant vers la gauche (l) ou vers la droite (r).

      • [^] # Re: Solution à base de types variants en ADA

        Posté par  (site web personnel) . Évalué à 1.

        Il n'y a pas de garantie statique sur ce genre de chose ? Ça c'est dommage.

        J'ai l'impression qu'on navigue à la frontière entre le rôle du compilateur et celui de l'analyseur de statique de code.

        MaPolitique := (NombreFixe,  0); -- Warning: "Constraint Error will be raised at Runtime"

        Ada le fait dans une certaine mesure comme dans la ligne ci-dessus. Pour des choses plus complexes, il faut donc faire appel à d'autres outils.

        Une des forces d'Ada est l'obligation de conformité (ACATS) des compilateurs. Cela participe sans doute au succès d'Ada pour des usages critiques. Mais c'est parfois aussi un point faible, en terme de disponibilité rapide d'un compilateur lors de la sortie d'un nouveau hardware. Il faudrait voir quel impact une telle complexification du compilateur aurait sur ce processus de validation, que peu de langages s'imposent.

        Un avantage de la solution Ada est que l'ensemble des tests au runtime peuvent être activés ou désactivés avec un simple pragma si on choisit de privilégier la performance. Je ne connais pas assez Haskell pour dire si ce type de modularité est possible avec les solutions proposées dans les commentaires.

        • [^] # Re: Solution à base de types variants en ADA

          Posté par  (site web personnel, Mastodon) . Évalué à 4.

          J'ai l'impression qu'on navigue à la frontière entre le rôle du compilateur et celui de l'analyseur de statique de code.

          Alors, je me suis aussi posé la question et j'ai fini par la poser au bon endroit à savoir sur le newsgroup.
          Au final, c'est la norme qui définit la notion d'erreur de compilation et celle-ci ne parle que de validité du code source.
          Bon, le compilateur, lui, le sait que ça ne va pas fonctionner mais c'est hors scope d'où le warning plutôt que l'erreur. Ceci dit, en utilisant l'option Warnings as errors à la compilation, ça revient au même ;)

          Après, il y a les solutions type AdaControl pour l'analyse statique et Spark pour la preuve de code pour aller plus loin

        • [^] # Re: Solution à base de types variants en ADA

          Posté par  . Évalué à 5. Dernière modification le 28 janvier 2017 à 14:05.

          J'ai l'impression qu'on navigue à la frontière entre le rôle du compilateur et celui de l'analyseur de statique de code.

          Certes, mais le contrôle de type (type checking) effectué par un compilateur relève de l'analyse statique de code. Dans les faits, on ajoute des outils d'analyse statique de code à l'extérieur du compilateur pour pallier aux déficiences du système de types d'un langage. Et pour fonctionner, ces outils nécessitent habituellement l'ajout d'annotations au code sous forme de commentaires, annotations qui correspondent à un enrichissement du langage des types du langage de départ.

          Dans tout langage de programmation, il y a en réalité deux langages :

          • le langage des termes pour décrire les calculs à effectuer ;
          • le langage des types pour rejeter à la compilation, ou à l'exécution, certains termes comme sémantiquement invalides (vides de sens).

          Plus le langage des types est évolué, plus il permet de contrôler la bonne formation des termes à la compilation (c'est-à-dire statiquement). L'idée des ADT est de pouvoir effectuer du raisonnement par cas non sur la valeur des termes (ce qui ne peut se faire qu'à l'exécution, là où la valeur est connue) mais sur leur type (ce qui est connu statiquement à la compilation).

          On peut même pousser le principe plus loin avec des GADT pour discriminer plus fortement la construction des termes, et faciliter l'optimisation du code généré sans avoir à gérer d'exception au runtime. Je vais l'illustrer sur un exemple en OCaml avec une fonction qui retourne la valeur du nœud racine d'un arbre binaire parfait.

          Avec les ADT, on peut encoder les arbres binaires parfaits ainsi :

          type 'a t =
            | Empty : 'a t
            | Node : 'a * ('a * 'a) t -> 'a t

          Les contraintes sur le type ne permettent que de construire des arbres parfaits : soit l'arbre est vide, soit c'est un nœud qui contient une valeur de type a et un arbre paramétré par un couple de type 'a * 'a (ce qui représente les sous-arbres gauche et droite).

          Pour extraire, la valeur du nœud racine on procède ainsi :

          let top = function
            | Empty -> failwith "Empty tree"
            | Tree (v, _) -> v

          La fonction retournera une exception à l'exécution si on lui passe un arbre vide :

          top Empty;;
          Exception: Failure "Empty tree".

          Maintenant, avec les GADT, on peut encoder ce type d'arbre ainsi :

          type z = Z
          type 'n s = S : 'n -> 'n s
          
          type ('a, 'n) t =
            | Empty : ('a, z) t
            | Tree : ('a, 'n) t * 'a * ('a, 'n) t -> ('a, 'n s) t

          Ici, c'est plus subtil et plus précis au niveau des contraintes de types. On commence par encoder les entiers dans le système de type avec z pour représenter zéro, et 'n s pour représenter la fonction successeur. Ensuite, on paramètre le type des arbres à la fois par le type des nœuds ('a) ainsi que par sa profondeur ('n). La définition dit qu'un arbre vide est de profondeur nulle et que les sous-arbres d'un nœud ont la même profondeur 'n (l'arbre est parfait) et que sa profondeur est 'n + 1 = 'n s.

          Pour coder la fonction top, il est n'est plus nécessaire de traiter le cas de l'arbre vide :

          let top : type a n. (a, n s) t -> a = function
            | Tree (_, v, _) -> v

          Le type de la fonction déclare explicitement que la profondeur de l'arbre est du type successeur ('n s) et donc l'arbre ne peut être vide. Cette fois, si on lui passe un arbre vide, on a une erreur de typage à la compilation :

          top Empty;;
          Error: This expression has type ('a, z) t
                 but an expression was expected of type ('a, 'b s) t
                 Type z is not compatible with type 'b s

          Pour ce qui est du code généré par le compilateur (option -dlambda du compilateur), on peut vérifier qu'il peut faire l'économie d'un test à l'exécution.

          Avec ADT, on obtient :

          let 
            (top =
              (function p
                (if p (field 0 p)
                  (apply (field 1 (global Pervasives!)) "Empty tree"))))

          Avec les GADT, on a :

          let (top = (function p (field 1 p))

          Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

          • [^] # Re: Solution à base de types variants en ADA

            Posté par  . Évalué à 3.

            Dans les faits, on ajoute des outils d'analyse statique de code à l'extérieur du compilateur pour pallier aux déficiences du système de types d'un langage. Et pour fonctionner, ces outils nécessitent habituellement l'ajout d'annotations au code sous forme de commentaires, annotations qui correspondent à un enrichissement du langage des types du langage de départ.

            Pas forcément. Déjà j'en connais un paquet qui ne demandent aucune annotation particulière. Ensuite, il y en a qui vérifie des choses qui ne sont pas liées au typage comme des constructions qui pourraient être plus lente ou l'usage d'API que tu ne souhaite plus utiliser ou d'avoir des propriété dans tes sources (avoir une doc en commentaire dans tes API publiques avoir une complexité cyclomatiques en dessous d'un certain seuil). Enfin tu as des cas où, effectivement ça pourrait être géré par un typage sophistiqué, mais vraiment trop (j'entends pour être véritablement utilisable). Par exemple les vérifications de couplages faible, vérifier que tes types sont correctes,…

            Toutes les discussions que l'on voit au dessus montrent justement qu'il y a suffisamment de façon de résoudre un problème pour que ça ne soit pas figé dans le langage. Pour autant tu peux vouloir, au sein d'un programme donné, n'autoriser qu'une seule solution à fin d'améliorer la cohérence.

            Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)

            • [^] # Re: Solution à base de types variants en ADA

              Posté par  . Évalué à 2.

              Toutes les discussions que l'on voit au dessus montrent justement qu'il y a suffisamment de façon de résoudre un problème pour que ça ne soit pas figé dans le langage. Pour autant tu peux vouloir, au sein d'un programme donné, n'autoriser qu'une seule solution à fin d'améliorer la cohérence.

              Où vois-tu dans mon propos que c'est figé dans le langage ? La discussion portait sur un bout de code ADA, celui-ci :

              MaPolitique := (Politique => CasParticulier);
              MaPolitique.NombreThread := 5; -- CONSTRAINT_ERROR : discriminant check failed

              qui générera une exception à l'éxecution car, dans ce cas du variant, il n'y a pas de champ NombreThread. C'est là une problématique de typage, et d'ailleurs le compilateur semble savoir qu'il y a problème, mais la norme semble avoir préférée émettre un warning et non une erreur de compilation. D'où la question de Guillaum : « Il n'y a pas de garantie statique sur ce genre de chose ? Ça c'est dommage ». Question à laquelle gerfaut83 a répondu : « J'ai l'impression qu'on navigue à la frontière entre le rôle du compilateur et celui de l'analyseur de statique de code ».

              D'une manière générale, le principe du typage statique se situe dans la question : comment refuser d'exécuter un code qui plantera nécessairement ? ou plutôt, comment savoir qu'un bout de code plantera nécessairement avant de le lancer ? D'où mon exemple pour refuser statiquement, par contrainte de type, un arbre vide comme entrée pour une fonction plutôt que de générer une exception à l'exécution; solution qui de plus réduit l'overhead du code généré.

              Dans l'exemple ci-dessus, ce n'est pas tant une impossibilité d'inférer statiquement qu'il y aura un problème, mais un choix de la norme qui considère cela comme un avertissement et non comme une erreur critique. Mais dans bien des cas, sans ajout d'informations qui ne sont pas définies par le langage, il n'est pas possible de garantir certains invariants d'un code. Ce à quoi je faisais référence, pour aborder cette problématique, était des outils d'analyse statique comme JML pour Java présenté, par exemple, dans la conférence Intégration de la vérification formelle dans les langages de programmation.

              Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

              • [^] # Re: Solution à base de types variants en ADA

                Posté par  . Évalué à 3.

                D'une manière générale, le principe du typage statique se situe dans la question : comment refuser d'exécuter un code qui plantera nécessairement ?

                Et justement, je dis que les analyseurs statiques servent aussi à refuser du code qui fonctionne parfaitement, mais qui ne correspond pas aux normes défini dans le programme en question par exemple.

                Tu peux très bien imaginer que ton langage possède un métalangage permettant ce genre de construction, mais ça n'apporte pas grand chose par rapport au fait de faire ça à coté.

                Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)

                • [^] # Re: Solution à base de types variants en ADA

                  Posté par  . Évalué à 5.

                  Et justement, je dis que les analyseurs statiques servent aussi à refuser du code qui fonctionne parfaitement, mais qui ne correspond pas aux normes défini dans le programme en question par exemple.

                  Soit mais là on est un plus dans un problème de définition de terme : je ne dispute jamais des mots pourvu que l'on me dise le sens qu'on leur donne.

                  Mon commentaire était en réponse à un échange entre Guillaum et gerfaut83 au sujet d'un bout de code ADA et du comportement du compilateur. Guillaum s'étonnait de l'absence de garantie statique (absence d'erreur de typage à la compilation), ce à quoi gerfaut83 lui a répondu qu'on se trouvait à la limite entre le travail du compilateur et celui d'un analyseur statique.

                  Je réponds alors : le type checking (tache qui incombe au compilateur) c'est de l'analyse statique; et dans l'exemple donné il y a clairement un problème de typage qui peut être détecté statiquement, c'est-à-dire à la compilation. Puis j'illustre mon propos sur un exemple pour montrer en quoi cela peut être utile : réduire l'overhead à l'exécution. Comme la chose est vérifiée une bonne fois pour toute à la compilation, il n'est pas nécessaire de faire un test dynamiquement qui générera une exception.

                  Ensuite, répondre que l'on peut faire rentrer dans la catégorie des tâches dévolues à l'analyse statique d'autres problématiques que le contrôle d'erreurs est hors de propos. Généraliser le concept de l'analyse statique au-delà du cas d'étude ici discuté fait de ton objection une sorte de stratagème III : la généralisation des arguments adeverses :

                  Il s’agit de prendre une proposition κατα τι, relative, et de la poser comme απλως, absolue ou du moins la prendre dans un contexte complètement différent et puis la réfuter. L’exemple d’Aristote est le suivant : le Maure est noir, mais ses dents sont blanches, il est donc noir et blanc en même temps. Il s’agit d’un exemple inventé dont le sophisme ne trompera personne. Il faut donc prendre un exemple réel.

                  Exemple 1

                  Lors d’une discussion concernant la philosophie, j’ai admis que mon système soutenait les Quiétistes et les louait. Peu après, la conversation dévia sur Hegel et j’ai maintenu que ses écrits étaient pour la plupart ridicules, ou du moins, qu’il y avait de nombreux passages où l’auteur écrivait des mots en laissant au lecteur le soin de deviner leur signification. Mon adversaire ne tenta pas de réfuter cette affirmation ad rem, mais se contenta de l’argumentum ad hominem en me disant que je faisais la louange des Quiétistes alors que ceux-ci avaient également écrit de nombreuses bêtises.

                  J’ai admis ce fait, mais pour le reprendre, j’ai dit que ce n’était pas en tant que philosophes et écrivains que je louais les Quiétistes, c’est-à-dire de leurs réalisations dans le domaine de la théorie, mais en tant qu’hommes et pour leur conduite dans le domaine pratique, alors que dans le cas d’Hegel, nous parlions des ses théories. Ainsi ai-je paré l’attaque.

                  Les trois premiers stratagèmes sont apparentés : ils ont en commun le fait que l’on attaque quelque chose de différent que ce qui a été affirmé. Ce serait un ignoratio elenchi de se faire battre de telle façon. Dans tous les exemples que j’ai donnés, ce que dit l’adversaire est vrai et il se tient c’est en opposition apparente et non réelle avec la thèse. Tout ce que nous avons à faire pour parer ce genre d’attaque est de nier la validité du syllogisme, c’est-à-dire la conclusion qu’il tire, parce qu’il est en tort et nous sommes dans le vrai. Il s’agit donc d’une réfutation directe de la réfutation per negationem consequentiæ.

                  Il ne faut pas admettre les véritables prémisses car on peut alors deviner les conclusions. Il existe cependant deux façons de s’opposer à cette stratégie que nous verrons dans les sections 4 et 5.

                  Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

                  • [^] # Re: Solution à base de types variants en ADA

                    Posté par  . Évalué à 4.

                    Ensuite, répondre que l'on peut faire rentrer dans la catégorie des tâches dévolues à l'analyse statique d'autres problématiques que le contrôle d'erreurs est hors de propos. Généraliser le concept de l'analyse statique au-delà du cas d'étude ici discuté fait de ton objection une sorte de stratagème III : la généralisation des arguments adeverses.

                    Non du tout. J'essayais juste de t'expliquer que ce sont des outils plus riches que ce que tu semblais affirmer dans la phrase que j'ai cité dans mon premier commentaire. Comme tu dis régulièrement que tu n'es pas développeur et que tu ne connais pas « l'industrie » ça ne me surprenait pas que tu ne connaisse pas ce pan là. Inutile de monter sur tes grands chevaux et de me faire une scène, je te laisse tranquille.

                    Tous les contenus que j'écris ici sont sous licence CC0 (j'abandonne autant que possible mes droits d'auteur sur mes écrits)

                    • [^] # Re: Solution à base de types variants en ADA

                      Posté par  . Évalué à 3.

                      Désolé si mon message a pu paraître agressif, telle n'était pas mon intention. C'est juste que je ne voyais pas où tu voulais en venir, ni le rapport avec les discussions du journal et des commentaires qu'il a suscités. Ma réaction était du même ordre que la fameuse réplique :

                      -- il dit qu'il a plus de genoux
                      -- il dit qu'il voit pas le rapport.

                      L'exemple central du journal tourne autour des garanties statiques que peut apporter Haskell (ou plus généralement, le système des ADT) pour la conception d'API et éviter les erreurs à l'exécution. S'en est suivi différentes discussions, avec des illustrations en ADA, Haskell ou OCaml, qui tournent toutes autour de ce même thème : peut-on (et si oui comment ?) contrôler la bonne formation des termes à la compilation (statiquement), ou doit-on mettre des gardes-fous et des tests lors de l'exécution (dynamiquement) ?

                      Ainsi lorsque je parlais d'outils d'analyses statiques, je ne considérais que ceux dont l'objectif se situe dans la gestion de cette problématique. C'est pour cela qu'à chacune de mes réponses, j'ai rappelé le contexte de la discussion. Je ne sous-entendais pas que les outils d'analyses de code se limitaient à gérer cette question. Et pour tous les cas d'usages que tu mentionnes, cela n'aurait d'ailleurs aucun sens d'avoir une alternative pour les traiter dynamiquement.

                      Une petite précision pour conclure :

                      Comme tu dis régulièrement que tu n'es pas développeur et que tu ne connais pas « l'industrie » ça ne me surprenait pas que tu ne connaisse pas ce pan là.

                      Il est vrai que je ne suis pas développeur (bien que je saches programmer, mais c'est loin d'être ma préoccupation première), et que je ne connais pas l'industrie. Mais quand je dis cela, c'est surtout pour exprimer que je ne sais pas ce qui est passé des laboratoires de recherche (et qui y est notoirement connu) vers le domaine industriel, ni le vocabulaire associé et le changement de dénomination qu'ont pu subir les notions lors du passage (ce qui est aussi parfois le cas lorsque la notion passe du domaine des mathématiques pures et de la logique à celui de l'informatique théorique).

                      Si je prends un exemple pour illustrer la chose. Dans la vidéo de la conférence sur JML (dont le lien était erroné, le voici), l'orateur expose sur un cas particulier une méthode d'analyse statique dite analyse polyédrique (vers la 40ème minute). Il conclue l'étude de cette exemple avec une diapo qui contient ce passage :

                      Principe de l'analyse de programme :

                      • traduction vers un flux d'équation sur des ordres partiels
                      • résolveur général basé sur des itérations

                      et la méthode de résolution (comme il le souligne à l'oral) est en partie fondée sur des travaux de Tarski qui datent des années 1930. Résultats auxquels j'avais fait allusion dans un autre journal. Ce type de technique se retrouve dans les solveurs SMT (Satisfiability modulo theories), comme par exemple l'outil alt-ergo (écrit en OCaml) utilisé, entre autre, par Spark dont a parlé Blackknight.

                      Les résultats de Tarski me sont connus depuis une bonne quinzaine d'années (époque où j'étais étudiant), et ce genre de conférence me permet de savoir que des industriels peuvent en faire usage (quant bien même ils ignoreraient ce qui se trouve sous le capot, ou dans quel contexte et pour quelles raisons ces problèmes ont été résolus à une époque où l'ordinateur n'existait pas encore).

                      Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

                      • [^] # Re: Solution à base de types variants en ADA

                        Posté par  (site web personnel, Mastodon) . Évalué à 2.

                        Ce type de technique se retrouve dans les solveurs SMT (Satisfiability modulo theories), comme par exemple l'outil alt-ergo (écrit en OCaml) utilisé, entre autre, par Spark dont a parlé Blackknight.

                        Spark utilise aussi les SMT Z3 et CVC4 écrits tout deux en C++.
                        Par contre, j'avoue que je n'y connais rien et que je ne fais qu'utiliser, mon niveau de math étant bien en-deça du pré-requis ;)

                      • [^] # Re: Solution à base de types variants en ADA

                        Posté par  . Évalué à 3.

                        Si je prends un exemple pour illustrer la chose. Dans la vidéo de la conférence sur JML (dont le lien était erroné, le voici), l'orateur expose sur un cas particulier une méthode d'analyse statique dite analyse polyédrique (vers la 40ème minute). Il conclue l'étude de cette exemple avec une diapo qui contient ce passage :

                        Juste un mot là-dessus : premièrement je n'ai pas encore vu la vidéo1.

                        L'analyse polyédrique a été proposée pour l'optimisation et la parallélisation en compilation depuis la fin des années 80 (voir ici par exemple pour un résumé du modèle). Lorsque j'ai décrit la technique à un pote bien plus avancé en maths que moi (faire une analyse de formes convexes dans un domaine discret), il a tout de suite pigé la difficulté (dans le domaine continu, c'est « trivial », mais dans le domaine discret, pas du tout), et a proposé de suite la première solution utilisée dans ce cas : utiliser un solveur de programmation linéaire entière (pas sûr de la traduction de integer linear programming solver). Et c'est ce qu'a fait Feautrier à l'époque (il a écrit PIP rien que pour ça).

                        Mais utiliser un solveur ILP mène à de sérieuses contraintes, entre autres que le temps de résolution des (in)équations augmente exponentiellement avec la complexité du nid de boucle à paralléliser/optimiser. De nos jours il y a enfin quelques compilateurs/transpilers qui sont relativement efficaces pour correctement compiler tout ça dans un temps raisonnable, et qui ne passent pas nécessairement par un solveur ILP (et donc le temps d'exploration des espaces d'itération est bien moins grand), mais même dans GCC qui a (avait?) une branche pour les optimisations suivant le modèle polyédrique, ce ne serait jamais activé par défaut.

                        Bref. Pour passer d'un modèle mathématique correct, et qui fonctionne sur des programmes/boucles jouet, à un compilateur qui peut compiler du « vrai » code (principalement scientifique), il a fallu attendre environ 20 ans (et sacrifier pas mal de thésards à l'autel du modèle polyédrique). Et malgré tout, ce n'est toujours pas intégré dans les compilateurs « mainstream » (tout au plus est-ce une option qu'il faut activer volontairement), car les résultats mathématiques ne se réduisent pas nécessairement en possibilité d'implémentation efficace.


                        1. Je suis en train de la télécharger, mais apparemment depuis les US ça prend 300 ans.  

                        • [^] # Re: Solution à base de types variants en ADA

                          Posté par  . Évalué à 3.

                          L'analyse polyédrique a été proposée pour l'optimisation et la parallélisation en compilation depuis la fin des années 80

                          Cela confirme une partie de la discussion qui suit la conférence : il semblerait que ce soit le bug d'Ariane V qui ait amené à s'intéresser à ce genre de technique.

                          Je ne me suis jamais penché sur la complexité de ce type d'algorithme, mais j'ai une question sur deux de tes remarques :

                          Mais utiliser un solveur ILP mène à de sérieuses contraintes, entre autres que le temps de résolution des (in)équations augmente exponentiellement avec la complexité du nid de boucle à paralléliser/optimiser.

                          et

                          Bref. Pour passer d'un modèle mathématique correct, et qui fonctionne sur des programmes/boucles jouet, à un compilateur qui peut compiler du « vrai » code (principalement scientifique), il a fallu attendre environ 20 ans (et sacrifier pas mal de thésards à l'autel du modèle polyédrique).

                          Les cas pathologiques pour la complexité exponentielle, on les rencontres dans du « vrai » code ? Je pose la question parce que, pour revenir sur le thème du journal et les ADT, ce système de type et son mécanisme d'inférence est basé sur l'algorithme d'unification de Robinson (milieu des années 1960) et le système Hindley-Milner ou le système F (début des années 70). Pour l'étude de la compléxité, il a fallu attendre 1991 et elle est doublement exponentielle. Xavier Leroy en propose une étude dans son livre sur le langage Caml (page 360 du livre et 370 du pdf). Cela étant, dans la « vraie » vie, sur du « vrai » code, on observe que l'algorithme se comporte linéairement : quand on double la taille du programme, on double le temps de compilation. Les pires cas en compléxité temporelle sont pathologiques; et à mon avis un programmeur qui les écriraient auraient soit l'esprit totalement tordu, soit aurait le cerveau qui exploserait bien avant de faire chauffer son CPU pour essayer de comprendre son propre code.

                          P.S : pour la vidéo, je les regarde en streaming via le lecteur proposé sur la page en question. Mais plus que la présentation des différentes techniques d'analyse statique, ce que je trouve intéressant c'est la discussion avec le public qui suit la présentation.

                          Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

                          • [^] # Re: Solution à base de types variants en ADA

                            Posté par  . Évalué à 3. Dernière modification le 02 février 2017 à 17:59.

                            Les cas pathologiques pour la complexité exponentielle, on les rencontres dans du « vrai » code ?

                            Ce ne sont pas des cas pathologiques, c'est bien le problème. La boucle en elle-même est peut-être « simplement » 2D ou 3D. Mais tout un tas d'applications scientifiques qui simulent des phénomènes naturels (différents aspects météo, dynamique moléculaire, etc., dont je ne maîtrise absolument pas la théorie derrière) utilisent des dizaines de variables, tableaux, etc., pour représenter divers paramètres et aspects du modèle. La complexité ne vient pas uniquement du nid de boucle, mais aussi de l'explosion du nombre de variables dans les systèmes d'(in)équations linéaires qui en résultent. Beaucoup de ces applications utilisent des tableaux à une, deux, ou trois dimensions, ce qui fait exploser le nombre d'états (car le problème des dépendances inter-itérations est qu'il faut maintenir un vecteur d'itération par tableau, plus ou moins, pour tracer les dépendances qui doivent être résolues, et celles qui peuvent être potentiellement « dynamiques » et malgré tout « calculables » par le compilateur pour déterminer si la forme de l'espace d'itération ET du réseau de dépendances constituent toujours un polyèdre convexe).

                            Enfin, pour paraphraser Feautrier lors d'une keynote sur le sujet, « le modèle polyédrique n'est que polyédrique ». Beaucoup de codes de la vie réelle font appel à des tableaux d'indirection (algèbre linéaire creux, méthodes par éléments finis, et en général pas mal d'algorithmes fonctionnant à partir de représentations par graphes). Le résultat est que dans le cas général le modèle polyédrique ne peut rien car il est impossible de savoir si on a bien un polyèdre convexe pour les dépendances de données1.

                            Cependant j'ai vu des gens montrer au cas par cas comment dépasser le problème de la convexité, au moins partiellement. Du coup peut-être que dans vingt ans on aura une théorie et des outils pour aller au-delà des limites actuelles du modèle. :)

                            EDIT: j'oubliais aussi un cas important : si on commence à avoir l'analyse polyédrique activable (genre Polly dans LLVM, qui est dans la branche principale je crois), il faut accepter que l'analyse va sans doute s'appliquer à TOUTES les boucles du programme. Ça risque de sérieusement rallonger le temps de compilation (du coup il faudra passer par des méthodes de ségrégation de certaines fonctions pour qu'elles soient isolées dans des fichiers spécifiques avec des options de compilation spécifiques). C'est déjà plus ou moins le cas dans pas mal de codes scientifiques optimisés, mais ça rajoute des contraintes sur le programmeur.


                            1. En pratique je connais des gens capables de faire tout un tas de trucs très cool malgré tout. Par exemple, si tu sais que malgré une indirection de type a[b[i]] par construction les valeurs de b sont monotones (croissantes ou décroissantes) tu peux quand même utiliser l'analyse polyédrique pour permettre la parallélisation. Mais du coup ça demande d'avoir un utilisateur qui le dit au compilateur. 

                  • [^] # Re: Solution à base de types variants en ADA

                    Posté par  . Évalué à 3.

                    Je réponds alors : le type checking (tache qui incombe au compilateur) c'est de l'analyse statique; et dans l'exemple donné il y a clairement un problème de typage qui peut être détecté statiquement, c'est-à-dire à la compilation. Puis j'illustre mon propos sur un exemple pour montrer en quoi cela peut être utile : réduire l'overhead à l'exécution. Comme la chose est vérifiée une

                    Deux choses:

                    1. La vérification de types peut se faire tout bêtement de façon sûre, mais à l'exécution. Voir par exemple Java (si on excepte les types primitifs): on a une garantie de ne pas se retrouver dans un état indéfini lorsqu'on passe par les classes et objets du langage, mais la plupart du temps ce sera détecté à l'exécution. Et pourtant, on peut parfaitement utiliser du lambda calcul pour définir le système de types de Java (voir par exemple le bouquin de Benjamin Pierce, « Types and Programming Languages »).
                    2. Il ne faut pas oublier que les spécifications des langages mais aussi les techniques d'analyse (sémantique, entre autres) évoluent avec le temps. ADA existe depuis un bout de temps (plus de 30 ans); C aussi. Mais on doit aussi faire face à ce qui n'est pas (et ne sera peut-être jamais) déprécié dans le langage, et qui du coup doit « passer » à la compilation, parce qu'à l'époque, on ne savait pas faire de détection efficace (parce que bon, si ton compilateur prend 3 heures pour te vérifier les types, personne ne l'utilisera sauf application ultra-critique et dont le code bougera peu). Idem avec C: n'importe quel compilateur moderne (Clang, GCC, ICC, XL/C, etc.) sait faire une analyse statique poussée du langage, malgré toutes les ambiguïtés qu'il embarque. Ces analyses vont bien plus loin que la norme, mais comme il y a des obligations de compatibilité ascendante, le compilateur ne peut émettre que des warnings. Ceci étant dit, si tu demandes à des développeurs expérimentés ce qu'il en est, ils te diront qu'il faut utiliser -Werror pour du code nouveau. Si ton code a un comportement particulier qui peut générer des avertissements du compilateur, mieux vaut le montrer explicitement sur la ligne de compilation avec des options de type -Wno-…. Si ton code est lié à des bibliothèques qui désormais génèrent des avertissements (qui n'étaient pas générés il y a 10 ans), alors évidemment il faut faire des exceptions.

                    Bref, ne pas oublier « l'existant », qui explique beaucoup de fois pourquoi un compilateur de « vieux » langage dit des choses qu'il faut « écouter » mais ne les force pas.

              • [^] # Re: Solution à base de types variants en ADA

                Posté par  (site web personnel) . Évalué à 3.

                D'une manière générale, le principe du typage statique se situe dans la question : comment refuser d'exécuter un code qui plantera nécessairement ? ou plutôt, comment savoir qu'un bout de code plantera nécessairement avant de le lancer ?

                Pour répondre au coup du Warning plutôt que de l'erreur pour le non respect du RANGE : Ada dispose d'une option pour forcer les Warning en Erreurs. Alors pourquoi laisser le choix ? Peut-être parce que le programmeur est un être libre :-) Non, blague à part, supposons que je souhaite écrire un test de couverture de code, car je m'interface avec un code en C qui ne dispose pas de ces vérifications de typage. Peut-être que cette option me facilitera l'écriture de mon cas de test.

                Dans le cas de l'attribut qui n'existe pas selon le discriminant, il n'y aura même pas de Waring à la compilation. Uniquement une Erreur au Runtime. Ça me semble difficile de détecter tous les mauvais usages d'un type variant, surtout si on peut récupérer le record depuis un contexte extérieur (non-Ada). Il faut bien que ça plante quelque part, au niveau de l'interface, si on fait de la programmation par contrat, ou plus loin dans le code si on ne teste pas à l'entrée.

                Après, on est d'accord, plus le compilateur englobe d'informations, plus il pourra nous aider à trouver les erreurs dans le code, voire dans sa sémantique. Mais si cette question était si simple, tout le monde coderait en COQ ! Comme ça tout serait toujours syntaxiquement et sémantiquement correct. Sauf que, si ce n'est pas le cas dans la pratique, c'est qu'il y a tout un tas de bonnes raisons de ne pas toujours le faire.

                Haskell représente certainement un très bon compromis sur cette échelle, bien que lorsqu'on pousse le curseur un peu loin, le noyau de codeurs, aptes à comprendre de quoi il retourne, se réduit à peau de chagrin (cf. multiples discussions ci-dessus).

                Ada, de son côté, a plein de limites, mais il a quand même été retenu pour bon nombre de projets dans des domaines tout à fait sérieux, et son système de typage (certes moins riche que celui de Haskell) n'y est sans doute pas étranger.

                Beaucoup de choses entrent en ligne de compte lorsqu'on choisit un langage. Haskell et Ada sont sans doute de très bons candidats, chacun dans leur domaine d'excellence.

                • [^] # Re: Solution à base de types variants en ADA

                  Posté par  . Évalué à 3. Dernière modification le 29 janvier 2017 à 02:47.

                  Dans le cas de l'attribut qui n'existe pas selon le discriminant, il n'y aura même pas de Waring à la compilation. Uniquement une Erreur au Runtime. Ça me semble difficile de détecter tous les mauvais usages d'un type variant, surtout si on peut récupérer le record depuis un contexte extérieur (non-Ada). Il faut bien que ça plante quelque part, au niveau de l'interface, si on fait de la programmation par contrat, ou plus loin dans le code si on ne teste pas à l'entrée.

                  Dans le cas où le code produit peut être utilisé via un autre langage qui ne permettrait pas de détecter statiquement l'erreur, assurément il faut bien alors mettre en place un contrôle dynamique avec émission d'une erreur. Cela relève du principe élémentaire dans le domaine réseau : « be conservative in what you send, be liberal in what you receive ». Ne sachant pas, a priori, ce que le code peut recevoir en entrée, il faut s'attendre à tout et être capable de gérer une erreur à l'exécution. Mais dans ton cas, le code est utilisé dans un contexte ADA et l'erreur est repérable statiquement. Détecter, dans ce cas, tous les mauvais usage d'un type variant à la compilation n'est pas une chose difficile : c'est le principe même du type checking, tâche qui incombe au compilateur dans les langages à typage statique.

                  Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

                  • [^] # Re: Solution à base de types variants en ADA

                    Posté par  (site web personnel) . Évalué à 1.

                    Détecter, dans ce cas, tous les mauvais usage d'un type variant à la compilation n'est pas une chose difficile : c'est le principe même du type checking, tâche qui incombe au compilateur dans les langages à typage statique.

                    Je pense que que pour ce type de vérifications, il faut activer d'autres mécanismes du langage, comme par exemple le sous-typage et polymorphisme qui permettent de distinguer des objets spécialisés dans différents contextes. Du coup, la non-vérification d'un contrat (utiliser un attribut spécialisé alors qu'on a une référence sur le type général) sera explicitement traquée par le compilateur et signalée comme erreur, comme dans n'importe quel langage objet.

                    Sur un simple enregistrement variant, l'information n'est pas portée avec le type dans la signature d'une fonction. Je peux comprendre qu'on puisse préférer que le compilateur refuse tout simplement de compiler lorsque la vérification est hors de portée. Cependant, Ada laisse toujours pour chaque mécanisme du langage le choix à l'utilisateur de décider s'il souhaite en avoir les avantages (expressivité, sécurité) mais aussi les inconvénients (complexité, interopérabilité, impact de performance, etc).

                    Par exemple, dans le cas de Ada objet, on peut choisir d'activer séparément différents mécanismes :
                    - de l'encapsulation (avec les PACKAGES)
                    - de l'héritage (avec l'utilisation de types dérivés : TYPE ... IS NEW ...)
                    - de l'extension de type (avec les types TAGGED PRIVATE)
                    - du polymorphisme (type ACCESS Object'Class)

                    Alors Ada est-il le meilleur langage objet pour autant ? Ce n'est pas mon avis, car on a vite fit d'écrire beaucoup de code pour faire des choses qui s'exprimeraient de manière beaucoup plus concise dans bien d'autres langages. Mais, peu de langages permettent une distinction aussi fine de ces mécanismes. Ça peut avoir éventuellement une vertu pédagogique : je pense que quiconque maîtrise l'objet en Ada, dispose de la maîtrise de tous les concepts nécessaires pour appréhender rapidement n'importe quel langage objet.

                    Oups, désolé, je ne sais plus comment on a réussi à dériver d'une discussion qui par du compilateur Haskell pour finir par parler des langages objets. Toute mes excuses pour des propos qui auraient pu être interprétés comme blasphématoires dans ce fil de discussion de conviction plutôt fonctionnelle.

                    • [^] # Re: Solution à base de types variants en ADA

                      Posté par  (site web personnel) . Évalué à 5.

                      Oups, désolé, je ne sais plus comment on a réussi à dériver d'une discussion qui par du compilateur Haskell pour finir par parler des langages objets. Toute mes excuses pour des propos qui auraient pu être interprétés comme blasphématoires dans ce fil de discussion de conviction plutôt fonctionnelle.

                      Aucune conviction ici, je ne sais toujours pas définir le fonctionnelle du "objet". Quand je présente Haskell, je ne parle pas d'un langage fonctionnel, parce que je ne sais toujours pas ce que cela veut dire. Même chose quand je parle de python.

                      Souvent les débats "fonctionel" versus "object" tournent autour de conneries sans nom à mon humble avis. J'entend souvent que python n'est pas objet parce que il y a le self explicite en premier argument ? C n'est pas objet parce qu'il n'y a pas de classes ? Haskell n'est pas objet parce qu'il y a des classes mais qu'elle n'ont rien à voir avec les classes en C++. Pour moi l'objet c'est avoir des "trucs" qui représentent des "bidules" métiers et pouvoir faire passer des "messages" entres les "trucs". En C++ on parlera de "méthodes" ou "fonctions membres" pour faire passer les messages, en Haskell on parlera de "fonctions". L'objet pousse aussi l'encapsulation, qui sera effectuée en C++ par le bias de public / private et en Haskell par le biais d'un module qui export une liste définie de fonction. Au final on exprime la même chose. Comparons le code haskell suivant permettant de définir un type Poulet :

                      module Poulet
                           (Poulet, -- Export le type `Poulet`, mais pas son constructeur, on ne peut pas crée de poulet avec un age arbitraire, on ne peut pas non plus dépacker un poulet en dehors de ce module pour changer son nom ou son age
                            cotcotcot, newPoulet, pouletAnniversaire)
                      where
                      
                      data Poulet = Poulet Int String
                      
                      -- | La fonction cot cot cot
                      -- fait faire cot au poulet autant de fois que son age.
                      -- Un poulet de 3 ans fera "cotcotcot"
                      cotcotcot :: Poulet -> String
                      cotcotcot (Poulet age _) = concat (replicate age "cot")
                      
                      -- | Un poulet tout neuf, d'age 0, avec un nom de poulet
                      newPoulet :: String -> Poulet
                      newPoulet s = Poulet 0 s
                      
                      pouletAnniversaire :: Poulet -> Poulet
                      pouletAnniversaire (Poulet age name) = Poulet (age + 1) name

                      Voici la version C++ :

                      class Poulet
                      {
                      private:
                         int age;
                         std::string name;
                      
                      public:
                         explicit Poulet(std::string newName):age(0), name(newName)
                         {}
                      
                         std::string cotcotcot() const
                         {
                               std::string ret;
                      
                               for(int i = 0; i < age; ++i)
                               {
                                   ret += "cot";
                               }
                               return ret;
                         }
                      
                         void anniversaire()
                         {
                             age++;
                         }
                      };

                      La seule différence ici c'est que pour la version Haskell j'ai fais le choix de faire un type non mutable et de renvoyer un nouveau Poulet lors de son anniversaire. La version C++ modifie le poulet en place. Note que on pourrait bien faire l'inverse cela ne poserait aucun problème à aucun des deux langages, c'est juste que Haskell est plus partisan de données non mutable alors que C++ est plus partisan des donnée mutable, mais c'est juste une orientation que donne le langage, rien d'obligatoire.

                      Bref, au final les différences entre les différents langages sont autres, par exemple, la présence ou non de pattern matching, que tu pourras trouver dans un langage objet ou dans un langage fonctionnel. Est-ce que le langage est plutôt orienté non mutable, ou mutable…

                      Le reste c'est juste des noms à la con mis sur des concepts mal défini. Je me rappel un étudiant qui dans un examen devait résoudre un problème en utilisant la programmation dynamique. Il m'a écrit :

                      Je ne sais pas ce qu'et la programmation dynamique parce que je ne suis pas venu en cours, mais je peux quand même résoudre votre problème avec une bonne complexité en utilisant un cache de résultat intermedaire, bla bla bla.

                      Sans le savoir, il avait fait de la programmation dynamique.

                      Tu ne sais pas ce qu'est un Functor, pas grave, tu l'a déjà utilisé sans le savoir. Pareil pour les Monad, Applicatives. Les opérateurs paresseux aussi. Le design pattern "visitor", c'est grosso modo du pattern matching.

                      Désolé pour ce petit coup de gueule ;)

                    • [^] # Re: Solution à base de types variants en ADA

                      Posté par  . Évalué à 5.

                      Sur un simple enregistrement variant, l'information n'est pas portée avec le type dans la signature d'une fonction. Je peux comprendre qu'on puisse préférer que le compilateur refuse tout simplement de compiler lorsque la vérification est hors de portée.

                      Si la vérification est hors de portée du compilateur (avec une pleine certitude), alors il ne doit pas refuser de compiler (tout au plus, peut-il émettre un avertissement pour signaler ce qu'il ne peut savoir au cas où cela pourrait poser un problème au développeur) mais prendre des précautions en plaçant un test à l'exécution (ce qui semble être le cas).

                      J'ai réfléchi, depuis, à cet exemple en ADA et l'impossibilité pour le compilateur de suivre le bon typage d'une telle valeur vient peut être de sa mutabilité. Dans ton exemple, on voit bien qu'il y a là un problème. Mais, de ce que j'ai compris, cette variable pourrait se voir attribuer une valeur connue dynamiquement (après calcul d'une fonction par exemple) qui serait du bon type et possédant, cette fois, le champ en question.

                      Avec les ADT (même avec des valeurs mutables, comme en OCaml) ce n'est pas possible, car l'existence du champ est marquée par le constructeur de type qu'il faut nécessairement déconstruire.

                      type politique =
                        | NbreFixe of int
                        | NbreMaxHardware
                        | PasDeThreading
                        | CasParticulier;;
                      
                      (* ici le terme est une variable mutable *)
                      let ma_politique = ref CasParticulier;;
                      let _ = ma_politique := NbreFixe 3;;
                      
                      let i = match !ma_politique with
                        | NbreFixe n -> n
                        | _ -> assert false
                      val i : int = 3

                      Oups, désolé, je ne sais plus comment on a réussi à dériver d'une discussion qui par du compilateur Haskell pour finir par parler des langages objets. Toute mes excuses pour des propos qui auraient pu être interprétés comme blasphématoires dans ce fil de discussion de conviction plutôt fonctionnelle.

                      Il n'y a rien de blasphématoires dans ce fil, c'est toujours intéressant de voir comment une problématique peut être abordée dans d'autres langages et paradigmes. Et comme je l'avais signalé dans la dépêche sur le compilateur 4.03 de OCaml, c'est du code ADA qui fait tourner les lignes automatiques du métro parisien ;-) (même s'il n'a pas été écrit à la main, mais généré à partir d'un langage plus haut niveau).

                      Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

                      • [^] # Re: Solution à base de types variants en ADA

                        Posté par  (site web personnel, Mastodon) . Évalué à 2.

                        même s'il n'a pas été écrit à la main, mais généré à partir d'un langage plus haut niveau

                        De mémoire, il s'agit de la Méthode B et l'outil qui était utilisé était l'Atelier B.
                        A l'époque, c'était Matra Transport International qui avait effectué une partie du boulot et du coup chez Matra Systèmes & Information où je bossais, des collègues l'avaient aussi utilisé pour un autre projet.
                        Je me souviens que cela ne semblait pas évident du tout :D

                        • [^] # Re: Solution à base de types variants en ADA

                          Posté par  . Évalué à 4.

                          Oui, c'est bien la méthode B et l'atelier B qui est derrière tout ça. C'est un successeur du formalisme Z qui a inspiré le langage Eiffel et sa programmation par contrat.

                          Son inventeur, Jean-Raymond Abrial, est revenu sur l'histoire de ces approches dans une conférence au Collège de France dont voici la présentation :

                          Cette présentation est celle d’un chercheur vieillissant qui porte un regard historique sur les trente dernières années de son travail.

                          Il y a deux sortes de chercheurs : les prolifiques et les monomaniaques. Je fais partie de la seconde catégorie, car j'ai toujours pratiqué le même genre d’investigations, à savoir la spécification et la construction vérifiée de systèmes informatisés.

                          Ce travail, autant théorique que pratique, s’est concrétisé au cours de toutes ces années dans trois formalismes voisins : Z, B et Event-B (dont je ne suis pas, loin de là, le seul contributeur). Je vais tenter d’expliciter comment les idées que contiennent ces formalismes et les outils correspondants ont lentement émergés de façon parfois erratique.

                          Je tenterai aussi de préciser les multiples influences qui ont participé à cette évolution. En particulier, je montrerai comment plusieurs réalisations industrielles ont permis de progresser dans ce domaine. Mais je soulignerai aussi les échecs et parfois les rejets de la part de communautés tant universitaires qu’industrielles.

                          Pour finir, je proposerai quelques réflexions et approches pour le financement de recherches telles que celle-ci.

                          Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

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

    Posté par  . É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.

    • [^] # Re: À propos du coté algébrique des ADT

      Posté par  . Évalué à 3. Dernière modification le 31 janvier 2017 à 13:59.

      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 :

      Pour celles et ceux qui ne font pas de Haskell foobarbazz parle du second "Somme". Il faut distinguer le constructeur de type (le 1er) du constructeur de valeur (le 2nd). En outre, les deux n'ont pas forcément le même nom.

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.