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

    Posté par . En réponse à la dépêche Sortie de GHC 8.0.2 et une petite histoire de typage statique. É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.