Journal EDSL et F-algèbres

Posté par . Licence CC by-sa
16
12
juin
2016

Bonjour,

J'ai récemment eu à concevoir un DSL et en recherchant quelques informations et bonnes pratiques je suis tombé sur ce lien contenant une vidéo youtube instructive.

L'idée est la suivante, pour intégrer un langage dédié dans un langage hôte (qui supporte des types algébriques), il y a au premier abord deux méthodes :

  1. Construire un type algébrique correspondant à la syntaxe des expressions du langage, et ensuite construire des fonctions d'évaluation qui produisent les valeurs attendues à partir de cette syntaxe
  2. Se passer de cette représentation intermédiaire et représenter directement l'évaluation (la sémantique) du langage

On constate facilement que la première méthode est au moins plus puissante que la seconde, mais que la seconde peut être beaucoup plus efficace (pas de construction de structure intermédiaire).

Le petit exemple en ocaml (pour changer) :

type expr = Add of expr * expr | Val of int ;;

let rec evaluate = function 
    | Val x -> x
    | Add (x,y) -> x + y;;

Ici, on sait quelle est la sémantique (c'est l'entier qui est calculé par l'expression) et on peut se passer de la représentation intermédiaire comme suit :

type expr = int;;

let add x y = x + y;;
let lit x   = x;;

Bien sûr cet exemple est trivial. La question que l'on peut se poser est la suivante : est-ce qu'il est rentable de faire cette élimination ? Les deux méthodes sont-elles équivalentes, quels sont les compromis ? Bien sûr, c'est dans la vidéo :p.

On termine par des concepts intéressants comme

  1. L'encodage de Böhm-Berarducci des types récursifs
  2. La notion de catamorphisme qui est lié à celui d'algèbre en général et d'objet initial en théorie des catégories. Un article en parle pour haskell et il a des jolies images

Cela donne lieu à des codes très génériques et concis, bien que performants. En revanche, cela introduit de la complexité dans les concepts que le code utilise, le rendant plus difficile à lire.

Par exemple à la fin de la vidéo on obtient pour les expressions avec des entiers et plus la « signature » F(A) = Int + A*A. Ce qui va donner le type de l'algèbre que l'on construit : (Int -> a, a -> a -> a). En effet, une F-algèbres, pour les gens qui n'ont pas le temps de cliquer sur le lien, c'est un foncteur F (comme celui précédent), et une fonction de « calcul » de type F A -> A. Or, ici le type F A est une union disjointe entre le type Int et le type A*A, donc la donnée de cette fonction est la donnée d'une paire de fonctions, une de type Int -> A, une autre de type A*A -> A.

type 'a algebre = (int -> 'a) * ('a -> 'a -> 'a);;
type 'a expr      = 'a algebre -> a;;

(* Les constructeurs sont des choses qui renvoient des expressions
 * donc te type blabla -> expr 
 *)
let lit  n   = (fun (f,g) -> f n);;
let sub x y  = (fun (f,g) -> g (x (f,g)) (y (f,g));;

(* faire une fonction qui évalue une expression en un entier, c'est facile !
 * int -> a ... on prend l'identité 
 * a -> a -> a ... on prend (-) 
 *)
let eval e = e (fun x -> x, (-));;

Attention, ce code ne fait pas ce que l'on veut. En effet, si on construit une autre manière d'évaluer, par exemple avec une paire (string_of_int, fun a b -> "(" ^ a ^ "+" ^ b ^ ")") qui permet de construire une chaine, on ne peut pas utiliser les deux évaluations sur une même structure. C'est parce que le système de type identifie le 'a dans le 'a expr avec le type de retour du éval utilisé … En haskell, le monsieur donne un type pour les expressions qui quantifie sur les 'a : type expr = forall 'a. 'a algebre -> 'a et il faudrait faire de même ici.

Pour un exemple plus détaillé (qui reprend en fait l'encodage de Böhm-Berarducci) en ocaml, qui lui utilise la quantification sur les types évoquée plus haut voilà où aller.

Voilà de la lecture pour le lundi qui arrive à grands pas !

  • # Lambda Akbar!

    Posté par (page perso) . Évalué à 5.

    (À lire sur le ton de « A monad is just a monoid in the category of endofunctors » :)

    Allons bon, pourquoi tant d'émerveillement devant la simple application du lemme de Yoneda à la catégorie des algèbres?

    • [^] # Re: Lambda Akbar!

      Posté par . Évalué à 3.

      Il y a des perles magnifiques dans cette histoire brève, incomplète et globalement erronée ! :-)

      1936 - Alonzo Church also invents every language that will ever be but does it better. His lambda calculus is ignored because it is insufficiently C-like. This criticism occurs in spite of the fact that C has not yet been invented.

      1970 - Niklaus Wirth creates Pascal, a procedural language. Critics immediately denounce Pascal because it uses "x := x + y" syntax instead of the more familiar C-like "x = x + y". This criticism happens in spite of the fact that C has not yet been invented.

      1972 - […] Lambdas are relegated to relative obscurity until Java makes them popular by not having them.

      1973 - Robin Milner creates ML, a language based on the M&M type theory. ML begets SML which has a formally specified semantics. When asked for a formal semantics of the formal semantics Milner's head explodes. Other well known languages in the ML family include OCaml, F#, and Visual Basic.

      1983 - Bjarne Stroustrup bolts everything he's ever heard of onto C to create C++. The resulting language is so complex that programs must be sent to the future to be compiled by the Skynet artificial intelligence. Build times suffer. Skynet's motives for performing the service remain unclear but spokespeople from the future say "there is nothing to be concerned about, baby," in an Austrian accented monotones. There is some speculation that Skynet is nothing more than a pretentious buffer overrun.

      Pour ceux qui ne sont pas allés lire le lien, ça vaut le coup pour se détendre et rire un bon coup.

      Néanmoins, Aluminium95 y est allé un peut fort sur ce journal et je peux comprendre la réaction de wolowizard. Je ne sais pas si ce sont mes messages de samedi dans la dépêche sur la sortie du dernier compilateur GHC Haskell qui l'ont inspiré, mais ils étaient humoristiques et dénoncés le jargon employé par les adeptes de la programmation fonctionnelle. J'y reprenais le fameux « une monade est un monoïde dans la catégorie des endofoncteurs » que je comparais à : il ne faut pas dire « la terres est ronde » mais « une équipotentielle du champ de gravitation terrestre est homéomorphe à la sphère S_2 », tout en montrant sur un exemple élémentaire le fait que ma nièce de 8 ans avait « compris » les notions d'anamorphisme, catamorphisme et hylomorphisme en appliquant l'algorithme élémentaire de la multiplication (bien qu'elle ignore tout de ce jargon qu'elle serait bien incapable de comprendre, Scratch est bien plus amusant pour elle ;-).

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

  • # Dans l'art voluptueuse de ne rien comprendre

    Posté par . Évalué à 10.

    BOOM j'ai pris une baffe!…

    bon, j'ai quand même un doctorat de physique et autres commodités (même si ça ne veut pas dire grand chose sur nos compétences, ça peut dire quelque chose sur la possibilité de compréhension) et j'aurais cru au moins comprendre un chouilla…ben non.
    Alors j'imagine d'autres…

    C'est gentil wikipedia…mais je pense qu'à ce niveau c'est un poil limité pour cerner tout le niveau intellectuel du bouzin. A mon humble avis, il faudrait donner un poil plus de références….
    Bien sûr on peut pratiquer le google-fu pour chercher des références adéquates en la matière…mais bon au bout d'un moment le temps alloué à cette recherche bibliographique devient non négligeable et par voie de conséquence on se désintéresse du sujet.

    J'en conclus (probablement à tord) des interprétations suivantes…
    Le but du post est
    - dédié à une élite intellectuelle (soit mais dans ce cas je ne comprends pas pourquoi l'objet du post, ici).
    - de balancer un certain nombre de mots clés qui fait genre je m'y connais (qui semble pour le moins vrai) mais dans ce cas je ne comprends pas le but du journal. Qui plus est ces mots sont couplés avec des liens wikipedia dans un souci plus moins maquillé de pédagogie pour le chalant. Je pense qu'il manque d'autres ref. bien sûr on peut chercher mais, comme dit juste au-dessus, il y a une certaine forme de chronophagie surtout à partir d'un certain niveau…

    Personnellement, je regarderais (ça m'intéresse et je cherche à comprendre)…mais je trouve le journal manquant "un chouilla" d'ouverture pédagogique même si on peut estimer que ce n'est ni le lieu, ni le but.

    Désolé…c'est lundi.

    • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

      Posté par . Évalué à 1.

      Le truc pour comprendre c'est qu'il faut simplement lire le code d'Oleg (le dernier lien) et après tout devient limpide, en admettons une certaine familiarité avec ocaml :P En fait j'apprécie l'effort que son auteur a fait pour rendre ce journal précis et didactique : en effet la terminologie utilisée correspond finalement à la doc officielle d'ocaml. Bref grâce à ce journal j'ai appris la technique de fold au lieu de l'éval récursif, le fameux codage de Böhm-Berarducci, Plus simplement c'est un évaluateur en style CPS. Au lieu d'avoir un évaluateur récusrif eval expr = case expr with App x y -> x (eval y) sur le type "expr" on a un type "expr" qui accepte un évaluateur sur X et retourne X: expr_app f x = fun evaluator -> evaluator.app f (x evaluator).

      L'astuce qu'Oleg utilise en fait en ocaml pour faire un type paramètrique sans fixer le paramètre, c'est qu'il faut embaler le type des fonctions constructrices d'expression dans un type du genre méthode polymorphique d'objet. En utilisant type expr = { expr : 'a . 'a algebre -> 'a } on arrive à exprimer "une fonction qui en reçevant une algèbre paramètré sur X s'évalue en X", sans fixer le type X au type de expr, i.e. le forall a. d'Haskell mentionné dans le journal. Si l'auteur du journal a trouvé une autre méthode pour exprimer le "forall" sans passer par cette indirection (donc ni par un objet, ni par un module first class), ça m'intéresse. Les GADT ne me semblent pas adaptés, mais, qui sait ?

      Par contre à la question de la performance, ben je crains que cette technique soit moins efficace parce que cela revient à construire un objet plus une closure pour chaque "expr" (closure = function partiellement appliqué).

      Btw, on pourrait traduire le code d'Oleg en Lua ou en javascript, j'imagine que ça rendrait ce journal plus compréhensible pour la majorité, ceci dit ça n'est pa la première fois que l'on cause ocaml sur ce site :-) Cela donnerait quelque chose comme ceci (note j'y connais pas grand chose en javascript, ça compile probablement pas tel quel).

      function expr_substraction(e1,e2) {
      return function(evaluator) evaluateur.substraction(e1(evaluator), e2(evaluator)
      }
      ...
      var e = expr_substraction(expr_lit("1"), expr_list("3")
      var string_evaluator = { substraction : function (v1,v2) { return "("+v1+"-"+v2+")"}; literal : function (s) { return s}}
      
      e(string_evaluator) -> "(1-3)"
      • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

        Posté par . Évalué à 7.

        J'ai toujours rien compris non plus. Mais je tente de comprendre pour simplifier une fonction de vérification du modèle et pas seulement d’exécution (ou alors une exécution qui rend vrai/faux). Le modèle récursif est élégant, mais devient vite imbitable avec des arbres.

        "La première sécurité est la liberté"

        • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

          Posté par . Évalué à 1. Dernière modification le 13/06/16 à 15:07.

          Je connais pas ton code, mais (il me semble que) la transformation revient à transformer tous les constructeurs des nodes de ton arbre en un fonctions sur un évaluateur. Par exemple si tu avais:

          type arbre = NodeTerm | ...
          let node (e1,e2,e3) = NodeTerm(e1,e2,e3)
          ...

          Tu le changes en

          type 'a evaluator = { node : ('a,'a,'a) -> 'a; ...}
          let node (e1,e2,e3) evaluator = evaluator.node (e1 evaluator, e2 evaluator, e3 evaluator)

          Et tu changes tes evals

          let eval_string = function
          | NoteTerm(e1,e2,e3) -> "NodeTerm("^(eval_string e1)^...")"
          
          let eval_bool = function
          | NodeTerm(_) -> true/false

          comme ceci

          let eval_string = {node = function (v1,v2,v3) -> "NodeTerm("^v1^","^v2^","^v3^")" (*pas de récursion, v1-v3 déja évalués! *)
          let eval_bool  = {node = function _ -> true/false}

          Chaque match de ton eval devient une fonction différente dans ton évaluateur (ça n'est pas pour rien qu'Oleg l'appelle expr_dict dans son exemple…) Par contre ce journal a utilisé un tuple, mais bon ça n'est pas très pratique à utiliser amha.

          Donc en gros tu changes tes constructeurs en closures sur l'évaluateur. Tu construits ton abre en faisant une application partielle des tes fonctions de construction. Donc toutes tes expressions deviennent des fonctions d'un évaluateur vers un résultat, soit le fameux type de ce journal type expr = forall 'a . 'a algebre -> 'a. C'est plus clair ? À toi de nous dire si cette réécriture t'apporte quelque chose de mieux ?

          • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

            Posté par . Évalué à 2.

            Si je reprend le code d'exemple :
            ça c'est bien un gadt ?
            type 'a exp_dic =
            {lit : int -> 'a;
            neg : 'a -> 'a;
            add : 'a * 'a -> 'a};;

            ça c'est la définition de la sémantique de "Lit" qui retourne une fonction de construction d'un type ?
            let lit : int -> exp = fun x ->
            {expi = fun d -> d.lit x}

            Que signifie la syntaxe : {expi = …} ? C'est la création d'un type avec un champs expi ?

            ça c'est l'éval :
            let eval1 : exp -> int = fun {expi = e} ->
            e {lit = (fun x -> x);
            neg = (fun e -> - e);
            add = (fun (e1,e2) -> e1 + e2)};;

            Que signifie la syntaxe "fun {expi = e}" ? et qu'est-ce que le terme "e {…}" ?

            "La première sécurité est la liberté"

            • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

              Posté par . Évalué à 1. Dernière modification le 13/06/16 à 16:06.

              Que signifie la syntaxe : {expi = …}

              C'est un "record" avec un champs expi. C'est juste pour contourner l'impossibilité de faire un "type exp = forall a.a algebre -> a", on "emballe" la fonction dans le champs expi d'un record, car dans ce cas on peut faire le forall en utilisant la syntaxe 'a. type-exp.

              Que signifie la syntaxe "fun {expi = e}"

              C'est la destruction par pattern-match, équivalent à "fun record -> let e = record.expi in …"

              "e {…}"

              On réemballe notre fonction dans un record. Encore une fois, ça aurait été mieux de passer une fonction directement ("la closure") mais parce qu'on ne sait pas exprimer son type sans passer par ce contournement. On aurait pu utiliser un objet normalement¸ca aurait été pareil. C'est le même problème que tu as en faisait.
              CORRECTION: sorry m'est trompé la en fait je crois que t'évalue ton expression justement, ton e = expri. Tu évalue ta closure, ton {} c'est ton dictionaire avec tes fonction "lit", "sub", etc.

              type 'a valfun = 'a * ('a -> ())
              let maliste = [ (2, fun _ -> ()); ("string", fun _ -> ()) ]
              (* marche pas car tous les éléments de la liste n'ont pas le même type "string valfun" contre "int valfun" *)
              
              (* versus *)
              
              type valfun = {valfun : 'a. 'a * ('a -> unit)}
              let malist = [ {valfun = (2, fun _ -> ())}; {valfun = ("string", fun _ -> ())}]
              List.iter (fun {valfun=(v,f)} -> f v) malist (* OK *)
              • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                Posté par . Évalué à 1. Dernière modification le 13/06/16 à 16:17.

                CORRECTION: sorry m'est trompé la en fait je crois que t'évalue ton expression justement, ton e = expri. Tu évalue ta closure, ton {} c'est ton dictionaire avec tes fonction "lit", "sub", etc.

                C'est bien ton évaluateur. Par exemple "{lit = fun x -> x}" serait un évaluateur vers int. Ton évaluateur vers string, ça serait {lit= fun x -> string_of_int x}. Après tu appliques "mon_ast (eval_dict_string : string algebre)" tu obtiens un string, dans l'autre cas tu fais "mon_ast (eval_dict_int : int algebre)", l'idée c'est que ton type de résultat d'évaluation/valeur n'est pas explicité dans ton type "expr/ast/arbre" mais juste dans ton expr_dict/algebre/evaluateur. Tu utilises donc l'encoding de Böhm-Berarducci, cqfd :p

                • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                  Posté par . Évalué à 2.

                  ok, je comprend mieux. Mais cela ne simplifie pas grand chose par rapport à un AST "classique" ("deep").

                  En fait, tu ne fais pas grand chose avec juste une composition structurelle. Un truc que tu as souvent besoin, c'est une référence vers un autre nœud de l'arbre et de pouvoir avoir accès à son contenu (typage, association, connecteur,…).

                  "La première sécurité est la liberté"

                  • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                    Posté par . Évalué à 1.

                    En fait, tu ne fais pas grand chose avec juste une composition structurelle.

                    Cela dépend sur quelle structure, un des trucs intéressants c'est justement que l'on peut transformer une information contextuelle, en un couple d'informations non-contextuel.

                    L'exemple dans la vidéo est celui du pretty-printing, mais en pratique on peut imaginer plein de choses où ça marche, d'ailleurs, un argument évident pour dire que c'est systématiquement aussi expressif : tu peux toujours dire que ta sémantique c'est la valeur que tu calcules et l'arbre lui-même (une paire). C'est un peu un cas dégénéré toutefois.

                    Pour un système de type par exemple, on peut faire remonter le type de chaque expression, ainsi que toutes les contraintes de types qui sont dans les sous-expressions, et l'ensemble des variables libres. Ces informations devraient normalement être suffisantes pour pouvoir déterminer tous les types.

                    • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                      Posté par . Évalué à 3.

                      "Pour un système de type par exemple, on peut faire remonter le type de chaque expression, ainsi que toutes les contraintes de types qui sont dans les sous-expressions, et l'ensemble des variables libres. Ces informations devraient normalement être suffisantes pour pouvoir déterminer tous les types."

                      Oui, mais tu as besoin de l'ast, dans ce cas, pour aller chercher tous les types en question.

                      "La première sécurité est la liberté"

                      • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                        Posté par . Évalué à 1.

                        Je ne comprend pas ce que tu veux dire par là.

                        Prenons par exemple un langage très simple de fonctions sur les entiers, qui prennent un certain nombre d'arguments, et retournent un certain nombre de valeurs. Le type est alors simplement le couple d'entiers (nbr_entrees, nbr_sorties). On peut imaginer des fonctions polymorphes, comme id, qui est de type (n,n) quelque soit le n.

                        Comme on demande du code, voilà un AST classique (sans construction qui utilise des fonctions) :

                        type expr = Id | Fonction of int * int * string | Compose of expr * expr ;;
                        
                        let exemple = Compose (Id, Fonction (2,3,"une fonction"));;

                        Tu peux décider que pour des raisons quelconques la seule chose qui t'intéresse, c'est le type de l'expression, dans ce cas, si on met de côté le cas de Id, on peut écrire la chose suivante :

                        type expr_type = int * int;;
                        
                        let fonction i j nom = (i,j);;
                        let compose (i,j) (k,l) = if j = k then (i,l) else failwith "erreur";;
                        
                        let exemple = compose id (fonction 2 3 "une fonction");;

                        On a toujours un langage intégré, mais au lieu de construire l'AST puis donner sa sémantique, on traite directement la sémantique. Maintenant, pour traiter le cas de id … On a un petit problème, parce qu'on ne peut pas déterminer directement son type sans regarder autour ! Mais on peut enrichir la sémantique, pour ne pas inclure simplement le type de l'expression, mais plutôt un moyen de la calculer …

                        L'exemple est assez chiant, mais en faisant un truc moche et peu efficace on a le code suivant :

                        type variable = int (*  les variables de types sont identifiées à des entiers *)
                        type semantique = {
                           equations  : equation list;
                           nbr_input   : variable;
                           nbr_output : variable
                        };;
                        
                        let new_variable () = ... ;; (* crée un nouvel identifiant unique *)
                        
                        let id = 
                            let v = new_variable () in 
                            { equations = []; nbr_input = v; nbr_output = v };;
                        
                        let compose f g = 
                            { equations = egalite_variable f.nbr_output g.nbr_input :: (f.equations @ g.equations) ; nbr_input = f.nbr_input; nbr_output = g.nbr_output };;
                        
                        let fonction i j nom = 
                            let vin = new_variable () in 
                            let vout = new_variable () in 
                            { equations = [ egalite_entier vin i ; egalite_entier vout j ] ; nbr_input = vin; nbr_output = vout};;

                        On part du principe que à partir des équations obtenues, on sait résoudre pour déterminer les valeurs des variables, et donc le type total de l'expression. Ici c'est assez simple à traiter.

                        Il faut remarquer que si on écrit une fonction qui prend l'AST et qui doit retourner un type, il faudra quand même traiter le cas de Id tout seul … Et donc on soit on échoue sur certains arbres, soit on utilise aussi un type de retour plus riche.

                        On constate aussi qu'il n'y a pas d'allocations liées à l'AST, en fait, si le compilateur inline tout, on a juste les calculs de construction de sémantique (incompressibles à priori, vu que c'est ce qu'on veut calculer).

                        La construction présentée plus tard permet (enfin, c'est ce que j'ai compris) de conserver une certaine capacité à pouvoir être inliné, à être tail-récursif, tout en permettant d'avoir plusieurs interprétations sans avoir à changer le code de tous les constructeurs.

                        • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                          Posté par . Évalué à 3.

                          Par type, je disais que tu as une définition dans un coin de ton arbre, qui a un nom "type_t".

                          Ailleurs, dans ton arbre, tu as un machin qui fait référence à "type_t". Pour vérifier que l'expression est juste, il faut aller chercher "type_t", ce qui empèche un simple parcourt d'arbre. Il faut le parcourt d'arbre, plus une fonction qui recherche le type dans l'arbre depuis la racine. C'est plus lent, et plus complexe, surtout si l'arbre est énorme.

                          Je pensais vraiment à un model, de l'ingénierie des modèles, c'est à dire une ensemble de classe qui respecte un diagramme de classe type UML. Donc, qui réutilise des définitions pour créer de nouveaux objets.

                          Pour ton explication, j'ai compris ton typage de fonction comme ayant simplement un nombre d'argument local sur une fonction, et non la réutilisation d'une définition qui est "ailleurs". La deuxième partie de l'explication, je suis vraiment passé à coté par contre…:/

                          "La première sécurité est la liberté"

                          • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                            Posté par . Évalué à 2.

                            Je ne comprends pas bien encore … En gros ce que tu dis c'est que tu as un arbre dans lequel les informations peuvent faire référence à des objets éloignés dans l'arbre ?

                            Si tu veux vérifier que l'expression est valide (ne fait référence qu'à des noeuds qui existent), ta sémantique c'est « l'expression est valide » (un booléen). Seulement, comme tu peux faire référence à des objets éloignés, cette information est contextuelle. La solution pour faire un unique parcours est de dé-contextualiser cette information en ajoutant plus de choses. Par exemple, un Set représentant tous les noms accessibles dans le sous arbre (ce qui change la complexité du parcours). Tu ne peux pas dire si une expression est correcte, mais tu peux dire à qui elle fait référence. Ainsi, ta sémantique serait un couple (variable_referencees, variables_declarees).

                            À la fin du calcul, on peut regarder si les variables référencées sont incluses dans les variables déclarées. Ce qui détermine si c'est bien typé ou non.

                            L'idée c'est d'ajouter suffisamment d'information dans le domaine de sortie pour construire l'information qui nous intéresse après en une seule étape et de manière indépendante de la structure qui l'a engendrée.

                            Si l'insertion dans ton set est en log n, comme tu fais autant d'insertions (dans le pire des cas) que la taille de l'arbre tu obtiens un truc dans le style du O( n log n)n est le nombre de noeuds dans l'arbre. Ensuite une petite inclusion d'ensembles ce qui n'est normalement pas trop méchant (un peu plus que linéaire ?).

                            • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                              Posté par . Évalué à 2.

                              Si tu as un :

                              typedef int toto_t;
                              ...
                              toto_t toto = 1;
                              Tu va construire 2 listes, avec ([toto_t -> int, toto -> toto_t],[ toto -> 1]) et ensuite comment tu fais de façon performante le lien "1 <- toto <- toto_t <- int" pour vérifier que c'est bon ?

                              "La première sécurité est la liberté"

                              • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                Posté par . Évalué à 1.

                                Il faudrait que je regarde à nouveau la vidéo de l'article, mais il me semble bien que la technique présentée concerne les Embedded Domain Specific Languages (EDSL). Là, tu prends l'exemple d'un compilateur C.

                                Néanmoins, je n'ai pas souvenir (je l'ai juste survolée) de l'avoir vu aborder le problème du bon typage du DSL en utilisant le système de type du langage hôte. Historiquement, c'est ainsi qu'ont étés introduis les types fantômes qui sont devenus par la suite les first-class phantom types ou GADT. Comment on gère le typage avec la méthode du shallow embedding ?

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

                                • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                  Posté par . Évalué à 2.

                                  L'exemple ressemble à du C, mais tu peux le voir aussi simplement comme une description de donné.

                                  Un DSL, sans référence, c'est vraiment un gros jouet inutile. En gros, cela veut dire que tu ne peux pas définir un truc dans ton langage, pour le réutiliser ensuite.

                                  (pour info, je bosse dans le domaine, autour des objet EMF d'eclipse, et des stéréotypes de sysml)

                                  à propos des type fantômes j'ai retrouvé ça : https://linuxfr.org/users/montaigne/journaux/les-types-fantomes.

                                  Si tu réutilises ton système de typage de ton langage hote, tu ne peux pas faire "autre chose", ce qui est très limitant.

                                  "La première sécurité est la liberté"

                                  • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                    Posté par . Évalué à 1.

                                    Je ne comprend toujours pas. Je dois être un peu lent, ou alors je n'ai pas eu affaire aux mêmes cas d'utilisation.

                                    Parce que, en pratique, comment tu fais « mieux » avec ton arbre ?
                                    Quand tu dis « comment tu fais le lien 1 <- toto <- toto_t <- int » …. je te retourne la question avec un arbre : cela n'a rien à voir avec la structure des expressions, c'est simplement ton système de type dans l'absolu qui demande ce genre de résolutions …
                                    Ce que j'ai dit, c'est simplement que je peux trouver toutes les contraintes de type, exactement comme tu le ferais avec un arbre, et avec une complexité pas trop dramatique …

                                    De ce que j'ai compris, toi tu vas parcourir l'arbre … Et à chaque expression inconnue, tu vas retraverser pour trouver ce que cela vaut ? Mais qui te prouve qu'il suffit d'une autre passe ? Qui te dis que tu n'as pas une chaine de contraintes très longue ? Mon algo marche pareil si tu ne fais que des alias tout le long

                                    typedef toto1 int
                                    typedef toto2 toto1
                                    typedef ... 
                                    
                                    totoN toto = 1
                                    

                                    Comment tu fais en parcourant l'arbre ? Mon algorithme débile trouve une chaine de contraintes … et après il faut résoudre, mais en tout cas il la trouve.

                                    En pratique, pour ocaml, ils récupèrent les contraintes de types, et font un algorithme d'unification un peu amélioré pour résoudre le problème du polymorphisme et trouver les types minimaux des expressions. Mais ils récupèrent « d'un coup » toutes les contraintes (en éliminant peut-être celles qui sont triviales localement).

                                    • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                      Posté par . Évalué à 2.

                                      Je ne comprend toujours pas. Je dois être un peu lent, ou alors je n'ai pas eu affaire aux mêmes cas d'utilisation.

                                      Je me dis la même chose en lisant les pattern de code plus haut :)

                                      Comment tu fais en parcourant l'arbre ? Mon algorithme débile trouve une chaine de contraintes … et après il faut résoudre, mais en tout cas il la trouve.

                                      En fait, c'est ton algo débile que je n'ai pas compris. Est-ce que tu peux reprendre mon exemple, et montrer ce qui il y aurait dans les listes, et comment se fait la vérification ?

                                      En pratique, pour ocaml, ils récupèrent les contraintes de types, et font un algorithme d'unification un peu amélioré pour résoudre le problème du polymorphisme et trouver les types minimaux des expressions. Mais ils récupèrent « d'un coup » toutes les contraintes (en éliminant peut-être celles qui sont triviales localement).

                                      Euh…

                                      "La première sécurité est la liberté"

                                      • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                        Posté par . Évalué à 1.

                                        Visiblement on est pas très fort pour communiquer :-).

                                        Je vais faire du pas à pas sur un exemple :-p.

                                        typedef toto int;
                                        int a = 1;
                                        toto b = 2;

                                        L'arbre pourrait ressembler à ça :

                                        expr = SEQ (TYPEDEF ("toto", "int"), (SEQ (VARDEF ("int", "a", INT 1), VARDEF ("toto", "b", INT 2))))

                                        Mon algorithme fait son petit fold et accumule les contraintes. Alors, comme on parle d'un langage assez compliqué, on admet qu'on ne peut pas mettre d'expressions à droite d'une égalité (c'est vraiment nul, mais sinon il faut plus de travail pour déterminer le type, c'est pénible, et cela n'est que « local » à l'expression).

                                        On peut donc écrire un bout de code dans ce genre là dans une disjonction de cas
                                        ocaml
                                        VARDEF (le_type, le_nom, (INT x)) -> { references = construire_un_singleton le_nom ; contraintes = construire_un_singleton (EQ "int" le_nom) ; declarations = empty_set }

                                        On peut aussi écrire un truc qui dit : ah bah oui, c'est bien défini

                                        TYPEDEF (a,b) -> { references = construire_un_singleton b ; contraintes = construire_un_singleton (EQ a b) ; declarations = construire_un_singleton a }

                                        On doit aussi écrire le cas où on tombe sur un SEQ, pour cela, on se contente de fusionner les contraintes et les références avec union_set.

                                        SEQ (a,b) -> { references = union_set a.references b.references ; contraintes = union_set a.contraintes b.contraintes }

                                        Je n'écris pas la fonction en entier, mais voilà comment ça tourne :

                                        evalue_type expr (* entre dans la fonction *)
                                        SEQ (x,y) (* fait l'appel récursif droit *)
                                        TYPEDEF ("toto","int") (* c'est un truc « final » : on applique la fonction de calcul *)
                                        { references = { "int" }; contraintes = { EQ ("int", "toto") }; declarations = { "toto" } }
                                        (* on a terminé l'appel récursif droit, on fait l'appel récursif gauche *)
                                        SEQ (z,t) (* fait l'appel récursif droit *)
                                        VARDEF ("int", "a", INT 1) (* c'est un truc « final » : on applique la fonction de calcul *)
                                        { references = { "int" }; contraintes = { EQ ("int", "int") }; declarations = {} }
                                        (* on a terminé l'appel récursif droit, on fait l'appel récursif gauche *)
                                        VARDEF ("toto", "b", INT 2) (* c'est un truc « final » : on applique la fonction de calcul *)
                                        { references = { "toto" }; contraintes = { EQ ("toto", "int") }; declarations = {} } 
                                        (* on a terminé gauche et droite, on fusionne les deux résultats car c'est ce qu'il faut faire avec un SEQ *)
                                        { references = { "toto", "int" }; contraintes = { EQ ("toto", "int") ; EQ ("int", "int") }; declaration {} }
                                        (* on a terminé gauche et droite pour la grosse expression, on fusionne les deux résultats car c'est encore un SEQ *)
                                        { references = { "toto", "int" }; contraintes = { EQ ("int", "toto") ; EQ ("toto", "int") ; EQ ("int", "int") }; declarations = {"toto"} }

                                        Alors j'ai très mal choisi la notation EQ qui correspond à ta flèche -> … Mais après, une fois qu'on a ce résultat, on peut regarder si tout ce qui est référencé est déclaré : ici ce n'est pas le cas, car on devrait dire que « int » est toujours déclaré. Ensuite, on peut éventuellement regarder si le graphe est bien fait au niveau des contraintes.

                                        • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                          Posté par . Évalué à 2.

                                          Je comprend beaucoup mieux. L'idée est que le fold retourne une liste complexe d'éléments qui sont analysé ensuite. Au lieu de tout faire en même temps, ce qui est très pénible, si le fold retourne juste vrai ou faux.

                                          Merci.

                                          "La première sécurité est la liberté"

                                  • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                    Posté par . Évalué à 1.

                                    pour info, je bosse dans le domaine, autour des objet EMF d'eclipse, et des stéréotypes de sysml

                                    Je sais que c'est le domaine dans lequel tu travailles; mais je voulais surtout insisté sur le côté embedded du DSL : à la fin on code dans le langage hôte (Haskell, ici OCaml, où le langage que tu veux peu importe) et non dans le DSL.

                                    Jeremy Gibbons (qui n'est pas né de la dernière pluie non plus) dans son exposé (c'est la vidéo) commence par cette classification :

                                    Programming Language
                                     |
                                     |-- General Purpose
                                     |
                                     |-- Domain Specific
                                           |
                                           |-- standalone
                                           |
                                           |-- embedded
                                                 |
                                                 |-- deep
                                                 |
                                                 |-- shallow
                                    

                                    La technique avec construction de l'AST puis interprétation via un fold sur celui-ci c'est du deep, et la technique qu'il présente et qui est le sujet du journal c'est du shallow.

                                    En regardant à nouveau la vidéo, j'ai vu le passage où il aborde la manière de gérer un type checker : en passant d'une interprétation conctextualisée (avec environnement) à une interprétation non-contextualisée via un flip (dans la vidéo, il ne l'illustre pas sur un type checker mais sur une fonction de pretty printing avec paranthésage minimal) ce qui ramène à la situation d'un fold.

                                    à propos des type fantômes j'ai retrouvé ça : https://linuxfr.org/users/montaigne/journaux/les-types-fantomes.

                                    Si tu réutilises ton système de typage de ton langage hôte, tu ne peux pas faire "autre chose", ce qui est très limitant.

                                    L'idée des types fantômes puis des GADT est de réutiliser le type checker du langage hôte pour s'assure que les termes de l'EDSL sont bien typés. Le principe général de faire de l'embedding est que cela évite d'avoir à coder un lexer et un type checker : on réutilise les outils fournis par la langage hôte. Comme dans l'exemple suivant :

                                    type _ term =
                                    | Lit : int -> int term
                                    | Bool : bool -> bool term
                                    | Add : int term * int term -> int term
                                    | Neg : int term -> int term
                                    | If : bool term * 'a term * 'a term -> 'a term
                                    
                                    let rec eval : type a. a term -> a = function
                                    | Lit n -> n
                                    | Bool b -> b
                                    | Add (t,t') -> (eval t) + (eval t')
                                    | Neg t -> -(eval t)
                                    | If (b,t,t') -> if (eval b) then (eval t) else (eval t')
                                    
                                    let lit n = Lit n
                                    let true_ = Bool true and false_ = Bool false
                                    let add t t' = Add (t,t')
                                    let neg t = Neg t
                                    let if_ b t t' = If (b,t,t');;
                                    
                                    let t1 = if_ true_ (lit 1) (add (lit 2) (lit 3));;
                                    val t1 : int term = If (Bool true, Lit 1, Add (Lit 2, Lit 3))
                                    
                                    let t2 = if_ false_ (lit 1) (add (lit 2) (lit 3));;
                                    val t2 : int term = If (Bool false, Lit 1, Add (Lit 2, Lit 3))
                                    
                                    eval t1, eval t2;;
                                    - : int * int = (1, 5)
                                    
                                    if_ (lit 2) (lit 1) (lit 3);;
                                    Error: This expression has type int term but an expression was expected of type
                                           bool term
                                           Type int is not compatible with type bool

                                    Enfin, il ne présente pas la méthode shallow comme un remplacement mais comme un approche complémentaire de la méthode deep. Il donne deux exemples intéressants à la fin de la conf', dont un où le shallow language a pour sémantique des termes de l'AST d'un langage plus petit pour, par exemple, compiler vers une architecture very Risc où l'addition add x y est interprétée par Sub x (Sub (Lit 0) y).

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

                                    • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                      Posté par . Évalué à 2.

                                      J'ai vu la vidéo. En plus des truc EMF, pour moi-même, j'ai codé un mini langage EDSL en ocaml pour éviter de devoir réinventer la roue. Mais le typage est différente de celui de ocaml, cela ne peut pas s'exprimer avec un gadt. Je l'ai donc recodé à la main.

                                      D'ailleurs, est-ce que dans les gadt, on peut mettre no propre type fantome ?

                                      J'ai toujours vu des trucs comme ça :

                                      type _ term =
                                      | Lit : int -> int term
                                      | Bool : bool -> bool term
                                      | Add : int term * int term -> int term
                                      | Neg : int term -> int term
                                      | If : bool term * 'a term * 'a term -> 'a term

                                      int/bool et jamais des type définit, qui n'ont d'utilité que pour ajouter un "tag" sur le résultat. (imagine un type "neverzero int" uniquement accepté par la division). L'idéal serait de pouvoir jouer avec des ensembles de variant, mais je ne crois pas que c'est possible.

                                      "La première sécurité est la liberté"

                                      • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                        Posté par . Évalué à 1.

                                        D'ailleurs, est-ce que dans les gadt, on peut mettre no propre type fantome ?

                                        Je ne vois pas trop ce que tu veux, les GADT sont des types fantômes : on les appelle aussi first-class phantom type.

                                        Tu veux un truc dans le genre ?

                                        module GADT = struct
                                          type _ term =
                                            | Lit : int -> int term
                                            | Add : int term * int term -> int term
                                            | Div : 'a term * [`NZ] term -> 'b term
                                            | Nz : 'a term -> [`NZ] term
                                        
                                          let rec eval:type a. a term -> int = function
                                            | Lit n -> n
                                            | Nz t -> eval t
                                            | Add (t,t') -> (eval t) + (eval t')
                                            | Div (t,t') -> (eval t ) / (eval t')
                                        
                                          let lit n = Lit n
                                          let add t t' = Add (t,t')
                                          let div t t' = Div (t,t')
                                          let nz t = assert (eval t <> 0); Nz t
                                        end
                                        
                                        open GADT;;
                                        
                                        let t1 = add (lit 3) (lit 2);;
                                        val t1 : int GADT.term = Add (Lit 3, Lit 2)
                                        
                                        let t2 = lit 3;;
                                        val t2 : int GADT.term = Lit 3
                                        
                                        let t3 = div t2 t1;;
                                        Error: This expression has type int GADT.term
                                               but an expression was expected of type [ `NZ ] GADT.term
                                               Type int is not compatible with type [ `NZ ]
                                        
                                        let t3 = div t2 (nz t1);;
                                        val t3 : '_a GADT.term = Div (Lit 3, Nz (Add (Lit 3, Lit 2)))
                                        
                                        eval t1, eval t2, eval t3;;
                                        - : int * int * int = (5, 3, 0)
                                        
                                        nz t3;;
                                        Exception: Assert_failure ("gadt.ml", 17, 13).

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

                                        • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                          Posté par . Évalué à 2.

                                          ok, je n'avais pas du utiliser la bonne syntaxe quand j'avais essayé. Va falloir que je reprennes mon code :)

                                          "La première sécurité est la liberté"

                                          • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                            Posté par . Évalué à 2.

                                            Où sinon, plutôt que de mettre un constructeur en plus dans ton langage (qui ne correspond sans doute à rien dans ta grammaire), il y a peut être moyen de mixer les GADT avec un usage plus « standard » des types fantômes. Comme dans cet exemple :

                                            module GADT = struct
                                              type (_,_) term =
                                                | Lit : int -> (int,_) term
                                                | Add : (int,_) term * (int,_) term -> (int,_) term
                                                | Mult : (int,_) term * (int,_) term -> (int,_) term
                                                | Div : (int,_) term * (int,[`NZ]) term -> (int,_) term
                                            
                                              let rec eval:type a b. (a,b) term -> int = function
                                                | Lit n -> n
                                                | Add (t,t') -> (eval t) + (eval t')
                                                | Mult (t,t') -> (eval t) * (eval t')
                                                | Div (t,t') -> (eval t ) / (eval t')
                                            
                                              let lit n = Lit n
                                              let add t t' = Add (t,t')
                                              let mult t t' = Mult (t,t')
                                              let div t t' = Div (t,t')
                                              let square_add_one t:(int,[`NZ]) term = (add (mult t t) (lit 1))
                                            end
                                            
                                            open GADT;;
                                            
                                            let t1 = square_add_one (lit (-3));;
                                            val t1 : (int, [ `NZ ]) term = Add (Mult (Lit (-3), Lit (-3)), Lit 1)
                                            
                                            let t2 = lit 23;;
                                            val t2 : (int, '_a) term = Lit 23
                                            
                                            let t3 = div t2 t1;;
                                            val t3 : (int, '_a) term = Div (Lit 23, Add (Mult (Lit (-3), Lit (-3)), Lit 1))
                                            
                                            eval t1, eval t2, eval t3;;
                                            - : int * int * int = (10, 23, 2)
                                            
                                            (* et si tu veux convertir au bon type dans la REPL, tu peux faire *)
                                            ((lit 4):>(int, [`NZ]) term);;
                                            - : (int, [ `NZ ]) term = Lit 4

                                            Ainsi tu n'obtiendras des termes non nuls qu'à partir de fonctions dont tu es certain que c'est ce qu'elles produisent.

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

                                        • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                          Posté par . Évalué à 2.

                                          Est-ce que tu connais un moyen d'exprimer un "ou" avec un gadt?

                                          Du style :
                                          | Or : 'a term * 'b term -> ('a| 'b) term

                                          Et est-ce qu'il existe un moyen de faire une égalité structurelle, par exemple pour considérer de même type, une structure ou une liste qui contient le même nombre d'argument de type compatible entre eux ?

                                          "La première sécurité est la liberté"

                                          • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                            Posté par . Évalué à 1.

                                            Pour ta première question la première idée qui me vient à l'esprit c'est les variants polymorphes :

                                            type _ term = Or: [`A] term * [`B] term -> [`A|`B] term

                                            Pour la deuxième, tu commences à vouloir pousser le système des types bien loin (j'aime bien l'idée ,c'est amusant :-). Il faudrait sans doute jeter un œil du côté de l'encodage du principe des indiscernables de Leibniz : à voir si tu trouves ton bonheur dans cette liste de liens.

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

                                            • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                              Posté par . Évalué à 2.

                                              Le principe même de mon langage était de pousser le principe du typage le plus loin possible, car si il est impossible de "prouver" un code dans le cas général, tu peux prouver beaucoup de choses structurellement. Donc, l'idée était de voir jusqu'où on pouvait aller dans le typage statique.

                                              On peut rajouter que je détestais le principe même du metamodèle UML qui empêche de faire des trucs aussi simple que de fixer la valeur d'une propriété dans un raffinement. Donc, j'ai mis les littéraux au même niveau que leur type.

                                              L'idée est de pouvoir écrire un truc comme :

                                              Struct=
                                                name= String "1"
                                                id= long
                                                fils= (Struct | 0)
                                              
                                              MyStruct= Struct
                                                name=
                                                id= 120000
                                                fils=
                                                   name=
                                                   id= 1000
                                                   fils= plop 
                                              
                                              plop Struct
                                                 name=
                                                 id=3
                                                 fils= 0
                                              

                                              La syntaxe n'est pas fixé, l'idée était plutôt un truc manipulable par des commandes externes (editeur texte ou graphique) ou un format de fichier type XML mais qui permet de définir des graphs acyclique avec le même langage pour le schéma.

                                              type t  = 
                                              (*Literals*)
                                              | LInt of int
                                              | LString of string 
                                              | LFloat of float 
                                              (*Internal type*)
                                              | Integer 
                                              | Float 
                                               | String 
                                              (*Op*)
                                              | And of t * t
                                              | Or  of t * t
                                              | Xor of t list
                                              (* Nommé *)
                                              | Name of string 
                                              (* Pointeur avec un path *)
                                               | Ref of string list (* TODO: adding integer index ref *)
                                              (* Multiplicité *)
                                              | Mult of int * int
                                              

                                              https://github.com/nicolasboulay/cherry-lang/blob/master/src/grape.ml

                                              J'avais tenté le gadt, mais j'avais vraiment du mal :

                                              type _ term =
                                              (*Literals*)
                                              | LInt : int -> int term
                                              | LString : string -> string term
                                              | LFloat : float -> float term
                                              (*Internal type*)
                                              | Integer : int term
                                              | Float : float term
                                              | String : string term
                                              (*Op*)
                                              | And : 'a term * 'a term -> 'a term
                                              | Or : _ term * _ term -> _ term
                                              | Xor : 'a term list-> _ term (*agregation also used for array*)
                                              (*Nommé *)
                                              | Name : string -> _ term
                                              (*Pointeur avec un path*)
                                              | Ref : string list -> _ term
                                              (*Multiplicité*)
                                              | Mult : int * int -> 'a term
                                              J'avais aussi envie d'ajouter un "Not" pour faire l'inverse de "And", cela permet de faire une logique plus complète (j'y ai pensé après avoir lu logicomix). Mais le "And" n'est pas un "and" (je l'ai appelé comme ça par rapport à "|" du type sum), c'est plus un "Sont du même type" genre un "~", c'est un blanc dans ma mini syntaxe. Le "Xor" c'est le "*" de ocaml (définit par le retour à la ligne et la tabulation). Le moyen de faire les tuples et les array.

                                              "La première sécurité est la liberté"

                                              • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                                Posté par . Évalué à 1.

                                                Le principe même de mon langage était de pousser le principe du typage le plus loin possible, car si il est impossible de "prouver" un code dans le cas général, tu peux prouver beaucoup de choses structurellement. Donc, l'idée était de voir jusqu'où on pouvait aller dans le typage statique.

                                                On peut aller très loin dans le typage statique : Coq !. Mais là, c'est du lourd et c'est violent. :-) En Coq, l'égalité n'est même pas une primitive du langage mais est définie… par le principe des indiscernables de Leibniz.

                                                type 'a leibniz = L of 'a
                                                
                                                let i = L  1 and j = L 1;;
                                                
                                                i = j;;
                                                - : bool = true
                                                
                                                i == j;;
                                                - : bool = false

                                                Le problème de l'égalité structurelle en OCaml c'est qu'elle peut être indécidable, et partir dans un calcul sans fin :

                                                let rec l = 1 :: l;;
                                                
                                                let rec l = 1 :: l;;
                                                val l : int list = [1; <cycle>]
                                                
                                                (* là on attend la fin des temps :-P *)
                                                l = l;;

                                                Le principe du typage et de l'inférence de types dans les langages fonctionnels viennent de la théorie de la démonstration, et l'inférence de types c'est de la preuve automatique. Selon le système de types (sa « puissance » expressive) l'existence d'une preuve d'une assertion peut devenir indécidable (c'est déjà le cas avec les GADT où il faut parfois rajouter des annotations pour que le système d'inférence fonctionne). En Coq, le système est si expressif qu'il faut faire les preuves à la main, le cas général étant indécidable.

                                                Comme on est quand même trolldi et que cette question du principe d'idendité résonne chez moi, je ne peux m'empêcher de citer mon maître :

                                                Unité et diversité. Quand un objet se présente à nous plusieurs fois, mais à chaque fois avec les mêmes déterminations intérieures (qualitas et quantitas), il est, si on le considère comme un objet de l'entendement pur, le même, toujours le même, non pas plusieurs, mais une seul chose (numerica identitas); si au contraire il est phénomène, il ne s'agit plus de comparer des concepts, mais quelque identique que tout puise être à ce point de vue, la diversité des lieux qu'occupe ce phénomène dans un même temps est un principe suffisant de la diversité numérique de l'objet même (des sens). Ainsi, dans deux gouttes d'eau, peut-on faire complétement abstraction de toute diversité intérieure (de qualité et de quantité), et il suffit de les intuitionner en même temps dans des lieux différents pour les regarder comme numériquement diverses. Leibniz prenait les phénomènes pour des choses en soi, par conséquent pour des intelligiblia, c'est-à-dire pour des objets de l'entendement pur (bien qu'il leur donnât le nom de phénomènes, à cause du caractère confus de leur représentation), et alors son principe des indiscernables (principium identitatis indescernabilium) était certainement inattaquable; mais comme ce sont des objets de la sensibilité, et comme l'entendement par rapport à eux n'a pas d'usage pur, mais un usage simplement empirique, la pluralité et la diversité numériques sont déjà indiqué par l'espace même comme condition des phénomènes extérieurs. En effet, un partie de l'espace, quoique parfaitement semblable et égale à une autre, est cependant en dehors d'elle, et elle est précisément par là, par rapport à la première partie, une partie diverse, qui s'ajoute à la précédente pour constituer un espace plus grand, et il doit en être de même, par suite, pour tout ce qui est en même temps en différents de l'espace, quelque semblable et quelque égale que cela puisse être par ailleurs.

                                                Kant, Critique de la raison pure.

                                                D'où la distinction entre les deux prédicats d'égalité en OCaml : égalité structurelle = et égalité physique ==, où la première peut être longue voire ne pas répondre tandis que la seconde répond toujours en temps constant. Cette même distinction, qui a grandement son importance, pourrait même être utile pour fournir une sémantique plus « propre » à la physique quantique de telle sorte que l'on ne dise plus qu'un objet peut être en deux lieux au même instant (soit disant en vertu du principe de superposition).

                                                j'y ai pensé après avoir lu logicomix

                                                J'avais dans l'idée de faire un journal un jour sur cette BD, faudrait peut être que je m'y colle. Si tu l'as lu, il y a un passage dans un restaurant à Paris où Poincaré se moque de Hilbert qui veut fabriquer une machine à faire des théorèmes parce qu'il « aime trop les saucisses » :-P (ce passage vaut bien les gros troll de DLFP ;-). Leibniz en avait eu l'idée et Frege, Russel, Hilbert voulaient mener le programme à bout. Mais Kant, à son époque, avait déjà saisi l'impossibilité de la chose, et Poincaré qui l'avait bien lu était fort sceptique sur la réussite du projet… jusqu'à ce que Gödel mette tout le monde d'accord et donne raison à Kant sur Leibniz ! \o/

                                                Cela étant toutes ces recherches ne furent pas vaines, et c'est pour cela que l'on a l'ordinateur, les langages de programmations, et les théories des types.

                                                Pour revenir à ton problème particulier et ton code, je jetterais peut être un œil dessus si j'ai le temps pour comprendre un peu mieux ce que tu cherches à faire.

                                                c'est plus un "Sont du même type" genre un "~", c'est un blanc dans ma mini syntaxe

                                                Cet article sur le blog de Jane Street te donnera peut être des idées.

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

                                                • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

                                                  Posté par . Évalué à 2.

                                                  "Le problème de l'égalité structurelle en OCaml c'est qu'elle peut être indécidable, et partir dans un calcul sans fin :"

                                                  On dirait que la principale raison du coté indécidable est la récursion. C'est pour cela que je parle de graphe acyclique. Il suffit de traiter les références différemment des définitions, cela permet de transformer la plus part des codes/données en graphes acycliques.

                                                  Selon le système de types (sa « puissance » expressive) l'existence d'une preuve d'une assertion peut devenir indécidable

                                                  Oui, d'où la recherche d'un sous-ensemble dans lequel il est possible de prouver quelques choses d'utile, et ne surtout pas regarder le cas général.

                                                  "La première sécurité est la liberté"

      • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

        Posté par . Évalué à 1. Dernière modification le 13/06/16 à 19:42.

        Les GADT ne me semblent pas adaptés, mais, qui sait ?

        Je ne pense pas. La meilleure solution, en OCaml, pour faire de l'abstraction sur les types (higher-kinded polymorphism) reste de passer par le système des modules. C'est la solution retenue par Jeremy Yallop, Léo White et Frédéric Bour pour implémenter du polymorphisme ad-hoc (ou surchage d'opérateur, les type class en Haskell) en OCaml (voir la partie 2.4 pour la discussion sur le choix d'utiliser le système de module).

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

        • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

          Posté par . Évalué à 1.

          La meilleure… c'est discutable, non ? Pourquoi pas avec des objets ou avec la méthode ci-dessus utilisée ? Il me semble qu'avec les first class modules tu payes un certain overhead aussi, donc j'imagine aussi avec les "implicit module" (qui ne font pas encore partie du lanague iianm) ?

          • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

            Posté par . Évalué à 1. Dernière modification le 14/06/16 à 01:07.

            Je ne vois pas comment faire autrement. Et ça méthode ne marche pas, il le dit lui même dans le journal et en redonne la raison dans ce commentaire. Sa solution fait une quantification existentielle sur le type, alors qu'il cherche une quantification universelle (higher-kinded polymorphism)-> les modules et les foncteurs; et il le dit lui même dans son journal :

            En effet, une F-algèbres, pour les gens qui n'ont pas le temps de cliquer sur le lien, c'est un foncteur F (comme celui précédent), et une fonction de « calcul » de type F A -> A.

            alors pourquoi ne pas utiliser le système des modules et des foncteurs du langage ?

            J'ai regardé rapidement la vidéo, et je n'ai pas encore bien saisi l'intérêt du shallow embedding par rapport au deep embedding. D'après Alluminium cela évite l'allocation de l'AST mais on peut imaginer une implémentation en CPS qui produit et consomme l'AST de concert pour éviter des allocations. Je trouve l'approche en shallow étrange et verbeuse.

            Pour l'overhead des frist class modules cela s'inline avec flambda, il me semble.

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

          • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

            Posté par . Évalué à 1.

            La meilleure… c'est discutable, non ? Pourquoi pas avec des objets ou avec la méthode ci-dessus utilisée ?

            J'ai l'impression que dans mon message du dessus je me suis trompé, et que tu fais référence à la méthode que tu as décrite dans ton message, c'est cela ? Il faut que j'y réfléchisse à tête reposée (pour le choix des objets, je ne les utilise jamais et je me suis toujours demandé ce que cela faisait dans le langage si ce n'est pour le défi théorique d'en comprendre le typage :-P).

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

    • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

      Posté par . Évalué à 4.

      C'est juste une question de culture (pas culture générale, la culture "environnementale"). Ça fait un petit moment que je baigne un peu la dedans (programmation fonctionnelle, théorie des catégories, algèbre générale, etc.) je suis encore loin d'être à l'aise. Mais ça a du sens tout ça.

      Je comprend parfaitement que ça puisse laisser cette impression : C'est très abstrait, il y a un formalisme super lourd, et les choses décrites sont généralement super simples.
      Et les matheux aiment bien les formalismes imbitables… Et là c'est des maths faites par des informaticiens, qui culturellement vont plus volontiers faire des grosse impasse sur la rigueur dans un but pédagogique.

      Ça me fait un peu l'effet que tu décris quand je lis un article sur WTF.js, le super framework whatever-oriented qui permet de mettre à genoux une machine dernier cri avec un hello world.

      Je connaissais pas cette présentation, et je vais la regarder avec grand plaisir :-)

    • [^] # Re: Dans l'art voluptueuse de ne rien comprendre

      Posté par . Évalué à 2.

      bon, j'ai quand même un doctorat de physique et autres commodités (même si ça ne veut pas dire grand chose sur nos compétences, ça peut dire quelque chose sur la possibilité de compréhension)

      bon j'ai quand même un doctorat en informatique et autres commodités mais dès que des physiciens commencent à parler de relativité, mécanique quantique, etc je suis largué ;) Les facultés de compréhension n'y sont pour rien. Son article est en fait très bien écrit. Il n'est tout simplement pas un cours sur les domaines cités mais une invitation les découvrir.

  • # C'est bien la peine !

    Posté par (page perso) . Évalué à 3.

    (* faire une fonction qui évalue une expression en un entier, c'est facile !
    * int -> a … on prend l'identité
    * a -> a -> a … on prend (-)
    *)

    Attention, ce code ne fait pas ce que l'on veut.

    Alors,
    1. Pourquoi tu prends "-" ?
    2. Si ça ne fait pas ce qu'on veut, c'était bien la peine de le présenter…

    Pourquoi ne pas montrer ce que donnerait "eval (Mul (Add (Int 3) (Int 3)) (Add (Int 5) (Int 2)))" ou un truc du genre avec ta représentation ? On veut du concret !

    • [^] # Re: C'est bien la peine !

      Posté par . Évalué à 1.

      Pourquoi tu prends "-" ?

      Pour montrer qu'on peut interpréter comme on veut le symbole, l'interprétation attendue était en effet "+", mais on peut aussi prendre la concaténation, et dire que la fonction de « int -> a » c'est « string_of_int ». Cela fait une autre manière d'interpréter la même construction.

      Si ça ne fait pas ce qu'on veut, c'était bien la peine de le présenter…

      Il fait ce qu'on veut, mais « une seule fois ». En fait, la définition ne permet pas assez de polymorphisme. Ce n'était peut-être pas très clair, mais voici comment le système d'ocaml réagit :

      1. On lui donne cette définition, il est content
      2. On construit une expression avec les deux constructeurs donnés, il est content.
      3. Quand on lui demande le type, il dit 'a expr : parfait !! Seulement, il ne dit pas vraiment ça. Il dit 'a expr pour une certaine valeur de 'a
      4. Quand on évalue l'expression avec (id,+), le gentil compilateur dit : « ok j'ai compris, en fait 'a = int ! ».
      5. Quand on essaie ensuite d'évaluer avec (string_of_int, ^) il dit … ohlala. 'a = int mais 'a = string … or string /= int … je suis perdu !!!

      Je trouve que cela valait le coup de le présenter parce qu'en voulant refaire ce que présente la vidéo, je suis tombé dans ce piège parce que je ne connaissait pas la syntaxe en ocaml qui traduirait le forall a. de haskell et je me suis demandé si l'oublier marcherait.

      • [^] # Re: C'est bien la peine !

        Posté par (page perso) . Évalué à 3.

        Nan, mais ma question principales est un niveau plus haut… Je ne parle pas du système de types d'OCaml (maintenant que j'ai compris que le polymorphisme t'avais surpris). Quand tu passes "(id,-)", veux-tu dire que c'est un programme qui fait la soustraction? Tu n'as jamais écrit l'exemple que tu cherchais à écrire avec ta méthode…

        Donc, considérant qu'avec mon DSL de base, si je veux faire "1+(1-2)" je dois écrire "(Add (Int 1) (Substract (Int 1) (Int 2)))", que dois-je écrire avec ton DSL?

        • [^] # Re: C'est bien la peine !

          Posté par . Évalué à 1. Dernière modification le 14/06/16 à 08:56.

          Je n'ai toujours pas saisi la finalité de la méthode décrite dans le journal, il va falloir que je médite la vidéo et le code donné en lien à la fin pour mieux saisir.

          J'ai l'impression qu'il veut faire de la quantification universelle sur du constructeur (forall a.) ce qui s'appelle du higher-kinded polymorphism et en OCaml on a tendance à utiliser le système des modules pour cela.

          D'un autre côte, il semblerait que l'objectif soit aussi d'éviter de construire explicitement l'AST du langage cible pour éviter de l'allocation. Si l'on met de côté cette contrainte, on peut obtenir le résultat qu'il souhaite ainsi sans même passer par les modules :

          type expr = Val of int | Op of expr * expr
          let rec fold f g e =
            match e with
            | Val i -> f i
            | Op (e1,e2) -> g (fold f g e1) (fold f g e2)
          ;;
          type expr = Val of int | Op of expr * expr
          (* oh le joli type de fold ;-) *)
          val fold : (int -> 'a) -> ('a -> 'a -> 'a) -> expr -> 'a = <fun>
          
          let e = Op(Val 1, Op(Val 1, Val 2));;
          let eval1 = fold (fun i -> i) ( + );;
          let eval2 = fold (fun i -> i) ( - );;
          let eval3 = fold string_of_int (fun a b -> Printf.sprintf "(%s+%s)" a b);;
          
          (* 1 + (1+2) *)
          eval1 e;;
          - : int = 4
          
          (* 1 - (1-2) *)
          eval2 e;;
          - : int = 2
          
          eval3 e;;
          - : string = "(1+(1+2))"

          Le terme technique pour la fonction fold est bien celui d'un catamorphisme sur la structure d'AST du langage d'experession, que l'on spécialise selon différentes interprétations pour donner eval1, eval2 et eval3.

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

          • [^] # Re: C'est bien la peine !

            Posté par . Évalué à 3.

            J'ai du mal à comprendre l’intérêt d'une fonction générique comme fold(). Le nombre d'argument est égal au nombre d'argument du type expr. Cela permet ici de pouvoir gérer plus facilement des "exécutions" différente.

            Mais le problème concerne surtout l'ajout d'élément au type. Cela implique à chaque fois l'ajout d'un argument au fold, non ?

            "La première sécurité est la liberté"

            • [^] # Re: C'est bien la peine !

              Posté par . Évalué à 1. Dernière modification le 14/06/16 à 11:08.

              L'utilité du fold est bien de pouvoir coder un principe général pour pouvoir faire varier les interprétations; ce qui me semblait être le problème d'Aluminium. Sinon pourquoi aurait-il parlé de catamorphisme, et donner l'exemple de réutilisation de son code pour varier l'interprétation afin de faire du pretty printing ? C'est cela la fonction fold.

              Pour ce qui est de rajouter des opérateurs au type des expressions, c'est pour cela qu'il y a des variants polymorphes : code reuse through polymorphic variants.

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

              • [^] # Re: C'est bien la peine !

                Posté par . Évalué à 3.

                Il faut que je relise plus doucement l'article. Mais les variants ont été critiqué, car ils ne permettent plus le principal avantage des types sommes : l’exhaustivité de leur usage.

                Il suffit de rajouter un élément pour que tous les filtres soient en erreur à la compilation. Ce n'est plus toujours le cas avec des variants, le compilo n'arrive pas à évaluer tous les cas. Pour le refactoring, c'est très puissant.

                C'était un gars de ocaml pro qui m'avait dit que beaucoup d'usagers de variants pour des AST avaient changé d'avis.

                "La première sécurité est la liberté"

          • [^] # Re: C'est bien la peine !

            Posté par . Évalué à 1. Dernière modification le 14/06/16 à 11:55.

            Je n'ai toujours pas saisi la finalité de la méthode décrite dans le journal

            Cette méthode utilise un encoding qui permet de se passer de la récursion.

            let rec fold f g e =

            raté :p

            ce qui s'appelle du higher-kinded polymorphism

            Apparemment le higher-kinded polymorphisme serait un autre nom de "type constructor polymorphism". Dans notre cas, on peut parler simplement de higher-order polymorphisme, non ?

            OCaml on a tendance à utiliser le système des modules pour cela.

            Je ne vois pas en quoi le répèter le rend plus vrai… Avec Obj.magic nous sommes même maintenant à une 4e technique ;-)

            D'un autre côte, il semblerait que l'objectif soit aussi d'éviter de construire explicitement l'AST du langage cible pour éviter de l'allocation.

            Remarques qu'il semblerait que le language cible soit le language hôte (E-DSL). Aussi que nous construisons un AST directement, ou que nous passions par des constructeurs—sans (val op : expr -> expr -> expr) ou avec (val op : 'a. 'a expr -> 'a expr -> 'a algebre -> 'a) l'encoding illustré dans ce journal --,dans tous les cas nous avons des allocations (en tout cas en ocaml), je ne vois pas comment on pourrait s'en passer ??

            (* oh le joli type de fold ;-) *)
            val fold : (int -> 'a) -> ('a -> 'a -> 'a) -> expr -> 'a =

            C'est simplement du first-order polymorphism, d'une fonction sur un type monomorphique. Le but du journal c'est de se passer de la récursion et utiliser le fameux encoding, et donc passer par un polymorphisme d'un plus grand genre (sic).

            Maintenant que tout ça a été re-dit, la question—que nous semblons tous aussi déjà avoir soulevée—c'est de montrer quels sont les avantages une fois qu'on a passé cette étape. Là je botte en touche… (Sans doute faudrait-il partir d'un exemple qui ne soit pas un jouet.)

            • [^] # Re: C'est bien la peine !

              Posté par . Évalué à 1. Dernière modification le 14/06/16 à 13:06.

              Cette méthode utilise un encoding qui permet de se passer de la récursion.

              Je n'avais pas lu le code d'Oleg. ;-)

              Apparemment le higher-kinded polymorphisme serait un autre nom de "type constructor polymorphism". Dans notre cas, on peut parler simplement de higher-order polymorphisme, non ?

              Oui, le higher-kinded polymophisme c'est du type constructor polymorphisme. Dans ce cas, c'est du higher-rank polymorphisme (ce que précise Oleg dans un de ses commentaires).

              Je ne vois pas en quoi le répèter le rend plus vrai… Avec Obj.magic nous sommes même maintenant à une 4e technique ;-)

              J'étais parti sur du higher-kinded, et j'admets que ce n'est pas la seule approche. Mais passer par Obj.magic quand on peut l'éviter, il faut aimer jouer avec le feu ;-)

              Remarques qu'il semblerait que le language cible soit le language hôte (E-DSL). Aussi que nous construisons un AST directement, ou que nous passions par des constructeurs—sans (val op : expr -> expr -> expr) ou avec (val op : 'a. 'a expr -> 'a expr -> 'a algebre -> 'a) l'encoding illustré dans ce journal --,dans tous les cas nous avons des allocations (en tout cas en ocaml), je ne vois pas comment on pourrait s'en passer ??

              Je me suis mal exprimé, j'avais bien vu que le langage cible était le langage hôte : je voulais parler du langage interprété (le DSL). Pour ce qui est de l'absence d'allocation, je faisais réfèrence au contenu du journal :

              On constate facilement que la première méthode est au moins plus puissante que la seconde, mais que la seconde peut être beaucoup plus efficace (pas de construction de structure intermédiaire).

              et comme tu le soulignes, avec l'encodage du journal les allocations sont juste « déplacées ».

              Maintenant que tout ça a été re-dit, la question—que nous semblons tous aussi déjà avoir soulevée—c'est de montrer quels sont les avantages une fois qu'on a passé cette étape. Là je botte en touche…

              Maintenant que j'ai lu le code d'Oleg à tête reposée, je comprends mieux pourquoi tu disais que c'était un évaluateur en style CPS. Par contre, je botte aussi en touche sur l'utilité pratique du système. Dans quels cas d'usage s'avère-t-il intéressant ? Qui gagne-ton, vis à vis des problèmes soulevés par Aluminium dans son journal (diversifier les interprétations), par rapport à la solution avec un fold générique sur la structure de l'AST?

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

            • [^] # Re: C'est bien la peine !

              Posté par (page perso) . Évalué à 3.

              Maintenant que tout ça a été re-dit, la question—que nous semblons tous aussi déjà avoir soulevée—c'est de montrer quels sont les avantages une fois qu'on a passé cette étape. Là je botte en touche… (Sans doute faudrait-il partir d'un exemple qui ne soit pas un jouet.)

              Je peux témoigner que dans le cas d'OCaml, cette représentation libre est beaucoup plus efficace sous l'hypothèse qu'on ne traverse l'arbre qu'une fois, et est de plus tail-récursive par construction. Cette technique est utilisée dans Coq pour représenter des listes paresseuses dans la monade du moteur de preuve.

              • [^] # Re: C'est bien la peine !

                Posté par . Évalué à 1.

                Merci pour l'exemple d'utilisation. Pour le côté tail-recursive cela vient de son côté CPS, ce qui permet sans doute d'éviter le stackoverflow sur de grands arbres (là où mon fold, qui ne l'est pas, risque d' « exploser ») ?

                J'ai néanmoins une question sur la source de l'efficacité de la construction dans le cas où l'on ne parcours l'arbre qu'une seule fois. L'AST semble être représenté par des fermetures sur ses « constructeurs », ce qui en fait une sorte de construction paresseuse, et quand on l'évalue on le construit pour le consommer de concert, c'est cela ? Si je vois à peu près ce que l'on gagne en temps (ça évite de construire l'arbre d'abord, puis de le parcourir ensuite pour l'interpréter), quel est le coût en espace de toutes ces fermetures ?

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

                • [^] # Re: C'est bien la peine !

                  Posté par (page perso) . Évalué à 3.

                  J'ai néanmoins une question sur la source de l'efficacité de la construction dans le cas où l'on ne parcours l'arbre qu'une seule fois. L'AST semble être représenté par des fermetures sur ses « constructeurs », ce qui en fait une sorte de construction paresseuse, et quand on l'évalue on le construit pour le consommer de concert, c'est cela ? Si je vois à peu près ce que l'on gagne en temps (ça évite de construire l'arbre d'abord, puis de le parcourir ensuite pour l'interpréter), quel est le coût en espace de toutes ces fermetures ?

                  D'après nos tests, c'est en pratique toujours plus efficace en mémoire que de construire l'arbre d'un coup. En effet, la taille des clôtures est plus généralement petite que la taille de l'arbre en cours de création qui est garbage collectée au fur et à mesure, ce qui n'est pas le cas quand l'arbre est construit à priori.

          • [^] # Re: C'est bien la peine !

            Posté par (page perso) . Évalué à 2.

            Mais c'est alors encore moins intéressant !
            J'ai pas le temps de jouer avec le code, mais ce concept se limite-t-il au FOLD, ou s'appliquerait-il aussi à un évaluateur complet ? Car bon, tes opérateurs n'ont pas d'opérateur… Si c'est juste pour le fold, je préfère payer le prix de mon DSL de base et garder mon code simple.

            • [^] # Re: C'est bien la peine !

              Posté par . Évalué à 1.

              Car bon, tes opérateurs n'ont pas d'opérateur

              Je ne comprend pas cette phrase, que veux-tu dire ?

              Si c'est juste pour le fold

              En fait il faudrait faire une preuve rigoureuse, mais en regardant les différents liens, on constate que au moins sur des exemples, on arrive à transformer une évaluation contextuelle sur un AST en une évaluation non-contextuelle qui utilise juste un fold (quitte à dire plus de chose quand on évalue). Si on admet ce résultat alors faire un fold est suffisant pour tout construire …

              • [^] # Re: C'est bien la peine !

                Posté par (page perso) . Évalué à 2.

                Op of expr * expr

                Je m'attendais à "Op of string * expr * expr" par example, où la chaîne serait "+" ou "-". Ou bien "Op of (expr -> expr) * expr * expr". C'est pour ça que je disais que les opérateurs n'avaient pas d'opérateurs. C'était pas clair, bon.

                J'ai pas encore lu les liens, mais je sais pas si on gagne forcément en lisibilité à tout écrire en terme de FOLDs…

            • [^] # Re: C'est bien la peine !

              Posté par . Évalué à 2.

              J'ai joué un peu avec le code, surtout l'encodage de Bohem-Berarducci, pour comprendre un peu ce qu'il faisait et comment cela marchait. Je vais l'illustrer sur un langage simple : un opérateur binaire sur les entiers (un semi-groupe pour les adeptes de l'algèbre ;-).

              On commence de manière classique avec un type exp pour l'AST du langage :

              type exp = Lit of int | Op of exp * exp

              on se donne des smart constructors pour notre langage et une fonction fold générique sur son AST :

              let lit n = Lit n
              
              let op e e' = Op (e,e')
              
              let rec fold f g = function
                | Lit n -> f n
                | Op (e, e') -> g (fold f g e) (fold f g e')

              à partir de là, on peut définir tout un tas d'interprétations différentes de l'AST et on colle le tout dans un module Ast :

              module Ast = struct
                (* l'AST du langage à un opérateur binaire sur les entiers *)
                type exp = 
                  | Lit of int
                  | Op of exp * exp
              
                (* smart constructors *)
                let lit n = Lit n
              
                let op e e' = Op (e,e')
              
                (* fold générique sur l'AST *)
                let rec fold f g = function
                  | Lit n -> f n
                  | Op (e, e') -> g (fold f g e) (fold f g e')
              
                (* interprétation en tant qu'addition *)
                let plus = fold (fun i -> i) ( + )
              
                (* interprétation en tant que soustraction *)
                let moins = fold (fun i -> i) ( - )
              
                (* profondeur de l'arbre *)
                let depth = fold (fun i -> 0) (fun d d' -> 1 + max d d')
              
                (* conversions en chaîne de caractères *)
                let show = fold string_of_int (fun s s' -> Printf.sprintf "(op %s %s)" s s')
                let show_p= fold string_of_int (fun s s' -> Printf.sprintf "(%s + %s)" s s')
                let show_m= fold string_of_int (fun s s' -> Printf.sprintf "(%s - %s)" s s')
              end

              Il s'utilise simplement dans une boucle REPL :

              open Ast;;
              let t = op (lit 1) (op (lit 2) (lit 3));;
              val t : exp = Op (Lit 1, Op (Lit 2, Lit 3))
              
              plus t, show_p t;;
              - : int * string = (6, "(1 + (2 + 3))")
              
              moins t, show_m t;;
              - : int * string = (2, "(1 - (2 - 3))")
              
              show t;;
              - : string = "(op 1 (op 2 3))"
              
              depth t;;
              - : int = 2

              Maintenant, on passe à l'encodage de Bohem-Berarducci. L'idée est de faire du type exp une « linéarisation » de l'arbre d'éxecution du fold de l'AST précédent. La fonction fold avait pour type (int -> 'a) -> ('a -> 'a -> 'a) -> exp -> 'a, le nouveau type sera donc :

              type exp = {expi : 'a. (int -> 'a) -> ('a -> 'a -> 'a) -> 'a}

              Le champ expi prend deux fonctions f et g et renvoie un objet de type 'a qui constitue l'interprétation de l'expression pour les fonctions f et g, comme le faisait le fold pour l'AST.

              On retrouve ensuite nos smart constructors qui mime les deux branches du fold :

              let lit n = {expi = (fun f g -> f n)}
              
              let op {expi=e} {expi=e'} = {expi = fun f g -> g (e f g) (e' f g)}

              La seule différence notable est dans le cas de op ou l'expression fold f g e devient e f g, étant donné que e est son « propre » fold et n'a pas besoin d'être rementionné comme argument.

              Pour les différentes interprétations c'est identique, en remplaçant fold par le champ expi du type des expressions; et on obtient le module :

              module Bohem = struct
                (* le type des expressions est une linéarisation de son propre fold *)
                type exp = {expi : 'a. (int -> 'a) -> ('a -> 'a -> 'a) -> 'a}
              
                (* smart constructors *)
                let lit n = {expi = (fun f g -> f n)}
              
                let op {expi=e} {expi=e'} = {expi = fun f g -> g (e f g) (e' f g)}
              
                (* interprétation en tant qu'addition *)
                let plus {expi = e} = e (fun i -> i) ( + )
              
                (* interprétation comme soustraction *)
                let moins {expi = e} = e (fun i -> i) ( - )
              
                (* profondeur de l'arbre *)
                let depth {expi = e} = e (fun i -> 0) (fun d d' -> 1 + max d d')
              
                (* conversions en chaîne de caractères *)
                let show {expi = e} =
                  e string_of_int (fun s s' -> Printf.sprintf "(op %s %s)" s s')
                let show_p {expi = e} =
                  e string_of_int (fun s s' -> Printf.sprintf "(%s + %s)" s s')
                let show_m {expi = e} = 
                  e string_of_int (fun s s' -> Printf.sprintf "(%s - %s)" s s')
              end

              Il s'utilise comme le précédent :

              open Bohem;;
              
              let t = op (lit 1) (op (lit 2) (lit 3));;
              val t : Bohem.exp = {expi = <fun>}
              
              plus t, show_p t;;
              - : int * string = (6, "(1 + (2 + 3))")
              
              moins t, show_m t;;
              - : int * string = (2, "(1 - (2 - 3))")
              
              show t;;
              - : string = "(op 1 (op 2 3))"
              
              depth t;;
              - : int = 2

              L'intérêt que je vois de prime abord et le côté récursif terminal des évaluations dans cette encodage ce qui permet d'éviter des stackoverflow sur des arbres grands ou fortement déséquilibrés. Pour ce qui est des performances, j'ai fait un benchmark du pauvre en le comparant à l'approche par AST et la méthode AST mais avec un fold récursif terminal en appliquant la transformation CPS décrite ici par gasche, ce qui donne ce module :

              module Astk = struct
                (* l'AST du langage à un opérateur binaire sur les entiers *)
                type expr =
                  | Lit of int
                  | Op of expr * expr
              
                (* smart constructors *)
                let lit n = Lit n
              
                let op e e' = Op (e,e')
              
                (* fold en CPS via CPS conversion trick *)
                let fold f g e =
                  let rec loop e k = match e with
                   | Lit n -> k (f n)
                   | Op (e, e') -> 
                       loop e (fun ie -> loop e'(fun ie' -> k (g ie ie')))
                  in loop e (fun e -> e)
              
                (* interprétation en tant qu'addition *)
                let plus = fold (fun n -> n) ( + )
              
                (* interprétation en tant que soustraction *)
                let moins = fold (fun n -> n) ( - )
              
                (* profondeur de l'arbre *)
                let depth = fold (fun n -> 0) (fun d d' -> 1 + max d d')
              
                (* conversions en chaîne de caractères *)
                let show = fold string_of_int (fun s s' -> Printf.sprintf "(op %s %s)" s s')
                let show_p= fold string_of_int (fun s s' -> Printf.sprintf "(%s + %s)" s s')
                let show_m= fold string_of_int (fun s s' -> Printf.sprintf "(%s - %s)" s s')
              end

              Pour le pseudo-bench cela donne :

              (* la liste des entiers [1; ...; n] *)
              let range n =
                let rec loop acc n = if n=0 then acc else loop (n::acc) (pred n)
                in loop [] n;;
              
              (* op (lit 0) (op (lit 1) op(... (lit n)) *)
              let ast n = let open Ast in List.fold_left (fun e i -> op e (lit i)) (lit 0) (range n);;
              
              let bohem n = let open Bohem in List.fold_left (fun e i -> op e (lit i)) (lit 0) (range n);;
              
              let astk n = let open Astk in List.fold_left (fun e i -> op e (lit i)) (lit 0) (range n);;
              
              (* la fonction de mesure approximative du temps de calcul *)
              let time f = fun () ->
              let before = Unix.gettimeofday() in
              for i = 1 to 100 do f () done;
              let after = Unix.gettimeofday() in
              after -. before;;
              
              (* trois mesures pour se faire une idée *)
              time (fun () -> Ast.plus (ast 100_000)) ();;
              - : float = 3.21051192283630371
              
              time (fun () -> Bohem.plus (bohem 100_000)) ();;
              - : float = 4.11348295211792
              
              time (fun () -> Astk.plus (astk 100_000)) ();;
              - : float = 5.08448696136474609

              Il reste encore à investiguer sur les cas où cet encodage offre un avantage sur la méthode usuelle.

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

              • [^] # Re: C'est bien la peine !

                Posté par . Évalué à 2.

                Essayes de prendre un arbre plus grand, l'idéal serait de faire une courbe en fonction de n, tu pourrais voir si les coubres sont parallèle ou si elles vont se croiser, ou encore, si il y a un cout d'init très élevé pour un cas particuliers.

                "La première sécurité est la liberté"

                • [^] # Re: C'est bien la peine !

                  Posté par . Évalué à 2.

                  J'ai fait quelques tests supplémentaires en utilisant la bibliothèque Core_bench (ce qui au passage m'a permis de me familiariser avec, elle est plutôt bien faite même si je n'ai pas encore fouillé assez pour voir comment générer des graphes avec les mesures).

                  Après études du comportement des différentes implémentations, il s'est avéré que l'encodage de Boehm-Berrarduci ne produit pas de fold « recursif terminal » (quoi qu'à lire le code, j'aurais du le voir) : le seuil qui déclenche un stack overflow est juste un peu plus élevé.

                  Néanmoins, dans le cas des semi-groupes implémentés, contrairement à ce qu'avait dit Perthmâd, cet encodage peut s'avérer plus performant que la version avec type inductif pour l'AST dans le cas où l'on parcours l'arbre plusieurs fois. En effet, la construction est plus lente mais le parcours plus rapide dans certain cas.

                  De plus, pour avoir un encodage plus performant il s'est avéré qu'il valait mieux utiliser la version avec dictionnaire (comme celle du code d'Oleg Kyseliov donné dans le journal) que la version currifiée que j'ai donnée pus haut. La version avec dictionnaire ressemble à cela :

                  module Boehmdic = struct
                    type 'a algebra = {
                      lit : int -> 'a;
                      op : 'a -> 'a -> 'a;
                      }
                  
                    type exp = {expi:'a. 'a algebra -> 'a}
                  
                    let lit n = {expi = fun alg -> alg.lit n}
                  
                    let op {expi=e} {expi=e'} = {expi= fun alg -> alg.op (e alg) (e' alg)}
                  
                    let plus {expi=e} =
                      e {lit = (fun n -> n);
                         op = ( + );}
                  end

                  Pour des résultats partiels de benchs, j'obtiens ce qui suit. Les résultats sont donnés en microseconde (us), les arbres sont des arbres binaires parfaits dont la profondeur est indiquée sur chaque ligne (de 7 à 10) et les test sont : construction+parcours (One) et parcours uniquement (Trav). Pour le temps de chauffe : faire la soustraction ;-). Les autres colonnes indiquent le nombre de collections mineures, de collections majeures et de promotions par exécution de la fonction (ici, je teste l'interprétation comme addition), ainsi que le pourcentage par rapport au temps le plus long.

                   Name                   Time/Run   mWd/Run    mjWd/Run    Prom/Run   Percentage  
                   ---------------------- ---------- --------- ----------- ----------- ------------ 
                    One/Ast-Perf:7           5.45us    1.28kw       3.16w       3.16w        5.14%  
                    One/Ast-Perf:8          11.30us    2.56kw      12.54w      12.54w       10.65%  
                    One/Ast-Perf:9          23.91us    5.12kw      50.40w      50.40w       22.54%  
                    One/Ast-Perf:10         51.03us   10.24kw     203.75w     203.75w       48.12%  
                    One/Astk-Perf:7          9.55us    4.60kw      12.72w      12.72w        9.00%  
                    One/Astk-Perf:8         19.72us    9.21kw      46.70w      46.70w       18.59%  
                    One/Astk-Perf:9         42.56us   18.42kw     184.04w     184.04w       40.13%  
                    One/Astk-Perf:10        96.38us   36.86kw     734.24w     734.24w       90.87%  
                    One/Boehm-Perf:7         8.91us    3.83kw      20.76w      20.76w        8.40%  
                    One/Boehm-Perf:8        19.13us    7.67kw      85.63w      85.63w       18.04%  
                    One/Boehm-Perf:9        42.86us   15.35kw     334.80w     334.80w       40.41%  
                    One/Boehm-Perf:10      106.06us   30.71kw   1_354.19w   1_354.19w      100.00%  
                    One/Boehmdic-Perf:7      7.33us    3.32kw      14.65w      14.65w        6.91%  
                    One/Boehmdic-Perf:8     16.33us    6.65kw      58.92w      58.92w       15.40%  
                    One/Boehmdic-Perf:9     35.82us   13.31kw     235.10w     235.10w       33.78%  
                    One/Boehmdic-Perf:10    86.27us   26.62kw     939.71w     939.71w       81.34%  
                  
                  Name                    Time/Run      mWd/Run   mjWd/Run   Prom/Run   Percentage  
                   ----------------------- ---------- ------------ ---------- ---------- ------------ 
                    Trav/Ast-Perf:7           2.44us                                           4.79%  
                    Trav/Ast-Perf:8           4.88us                                           9.58%  
                    Trav/Ast-Perf:9           9.78us                                          19.20%  
                    Trav/Ast-Perf:10         19.56us                                          38.40%  
                    Trav/Astk-Perf:7          6.08us    3_321.17w      0.61w      0.61w       11.94%  
                    Trav/Astk-Perf:8         12.30us    6_649.33w      1.37w      1.37w       24.15%  
                    Trav/Astk-Perf:9         24.82us   13_305.66w      3.11w      3.11w       48.74%  
                    Trav/Astk-Perf:10        50.93us   26_618.33w      6.88w      6.88w      100.00%  
                    Trav/Boehm-Perf:7         2.89us                                           5.67%  
                    Trav/Boehm-Perf:8         5.99us                                          11.76%  
                    Trav/Boehm-Perf:9        12.40us                                          24.34%  
                    Trav/Boehm-Perf:10       24.98us                                          49.04%  
                    Trav/Boehmdic-Perf:7      2.22us        3.00w                              4.36%  
                    Trav/Boehmdic-Perf:8      4.50us        3.00w                              8.84%  
                    Trav/Boehmdic-Perf:9      9.07us        3.00w                             17.81%  
                    Trav/Boehmdic-Perf:10    18.43us        3.00w                             36.20%  
                  

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

                  • [^] # Re: C'est bien la peine !

                    Posté par . Évalué à 3.

                    Pour faire des graph rapidement, j'utilise gnuplot. Mais je n'ai pas le script type sous la main, pour tracer n courbe à partir d'un fichier de donné type csv.

                    Boehmdic-Perf semble le plus intéressant au final. Tracer les courbes permettrait de voir si l'écart se creuse ou devient négligeable.

                    "La première sécurité est la liberté"

                    • [^] # Re: C'est bien la peine !

                      Posté par . Évalué à 1.

                      L'écart de performance diminue quand on augmente la taille de la structure, et la version avec type inductif devient plus performante sur la traversée également. Voilà un bench uniquement sur la traversée de la structure avec des arbres parfaits dont la profondeur varie de 10 à 20 avec un pas de 2 :

                       Name                       Time/Run   mWd/Run   Percentage  
                       ----------------------- ------------- --------- ------------ 
                        Trav/Ast-Perf:10            20.46us                  0.08%  
                        Trav/Ast-Perf:12            82.03us                  0.31%  
                        Trav/Ast-Perf:14           326.56us                  1.23%  
                        Trav/Ast-Perf:16         1_436.95us                  5.42%  
                        Trav/Ast-Perf:18         5_867.21us                 22.12%  
                        Trav/Ast-Perf:20        23_295.92us                 87.81%  
                        Trav/Boehmdic-Perf:10       18.40us     3.00w        0.07%  
                        Trav/Boehmdic-Perf:12       78.27us     3.00w        0.30%  
                        Trav/Boehmdic-Perf:14      326.51us     3.00w        1.23%  
                        Trav/Boehmdic-Perf:16    1_669.57us     3.00w        6.29%  
                        Trav/Boehmdic-Perf:18    6_665.36us     3.00w       25.13%  
                        Trav/Boehmdic-Perf:20   26_528.52us     3.00w      100.00% 
                      

                      Pour les arbres en forme de peigne (qui s'apparente à des listes, ceux que je construisais dans mes premières mesures), que le peigne parte vers la droite ou vers la gauche, la version « classique » est toujours plus performante que l'encodage de Boehm-Berarducci. Comme c'est une traversée en profondeur qui prend le sous-arbre gauche en premier, c'est plus lent sur des peignes qui partent à gauche. Mais dans les deux cas, la version « classique » avec type inductif est la plus performante. Avec des peignes vers la gauche, par exemple :

                        Name                      Time/Run   mWd/Run   Percentage  
                       ------------------------- ---------- --------- ------------ 
                        Trav/Ast-Left:500           5.28us                  6.76%  
                        Trav/Ast-Left:1000         11.54us                 14.78%  
                        Trav/Ast-Left:1500         17.67us                 22.64%  
                        Trav/Ast-Left:2000         23.99us                 30.73%  
                        Trav/Ast-Left:2500         30.99us                 39.70%  
                        Trav/Ast-Left:3000         36.98us                 47.38%  
                        Trav/Ast-Left:3500         43.60us                 55.85%  
                        Trav/Ast-Left:4000         51.75us                 66.30%  
                        Trav/Ast-Left:4500         58.19us                 74.56%  
                        Trav/Ast-Left:5000         64.97us                 83.23%  
                        Trav/Boehmdic-Left:500      5.68us     3.00w        7.27%  
                        Trav/Boehmdic-Left:1000    12.59us     3.00w       16.13%  
                        Trav/Boehmdic-Left:1500    19.81us     3.00w       25.38%  
                        Trav/Boehmdic-Left:2000    27.60us     3.00w       35.36%  
                        Trav/Boehmdic-Left:2500    34.10us     3.00w       43.69%  
                        Trav/Boehmdic-Left:3000    41.66us     3.00w       53.37%  
                        Trav/Boehmdic-Left:3500    51.37us     3.00w       65.81%  
                        Trav/Boehmdic-Left:4000    59.99us     3.00w       76.86%  
                        Trav/Boehmdic-Left:4500    68.38us     3.00w       87.61%  
                        Trav/Boehmdic-Left:5000    78.05us     3.00w      100.00% 
                      

                      et vers la droite pour de petites tailles :

                        Name                        Time/Run   mWd/Run   Percentage  
                       ------------------------- ------------ --------- ------------ 
                        Trav/Ast-Right:10           104.64ns                  5.82%  
                        Trav/Ast-Right:30           310.75ns                 17.28%  
                        Trav/Ast-Right:50           490.14ns                 27.26%  
                        Trav/Ast-Right:70           655.54ns                 36.46%  
                        Trav/Ast-Right:90           828.10ns                 46.05%  
                        Trav/Ast-Right:110          996.24ns                 55.40%  
                        Trav/Ast-Right:130        1_229.26ns                 68.36%  
                        Trav/Ast-Right:150        1_340.23ns                 74.53%  
                        Trav/Ast-Right:170        1_515.82ns                 84.30%  
                        Trav/Ast-Right:190        1_717.04ns                 95.49%  
                        Trav/Boehmdic-Right:10      125.31ns     3.00w        6.97%  
                        Trav/Boehmdic-Right:30      323.75ns     3.00w       18.00%  
                        Trav/Boehmdic-Right:50      508.61ns     3.00w       28.29%  
                        Trav/Boehmdic-Right:70      696.69ns     3.00w       38.74%  
                        Trav/Boehmdic-Right:90      879.47ns     3.00w       48.91%  
                        Trav/Boehmdic-Right:110   1_069.22ns     3.00w       59.46%  
                        Trav/Boehmdic-Right:130   1_245.08ns     3.00w       69.24%  
                        Trav/Boehmdic-Right:150   1_442.02ns     3.00w       80.19%  
                        Trav/Boehmdic-Right:170   1_620.29ns     3.00w       90.11%  
                        Trav/Boehmdic-Right:190   1_798.15ns     3.00w      100.00%  
                      

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

                      • [^] # Re: C'est bien la peine !

                        Posté par . Évalué à 2.

                        Ok, donc le bête AST est le plus rapide dans la plus part des cas.

                        Est-ce que tu peux faire un essai avec un arbre de taille semblable à un bon code, genre qq millions de noeuds ? Ici, on parle de quelques us d'écart, ce n'est pas significatif.

                        "La première sécurité est la liberté"

                        • [^] # Re: C'est bien la peine !

                          Posté par . Évalué à 1.

                          En réalité, j'ai mal nommé mes modules : dans tous les cas on a un AST, c'est juste la structure de données pour le représenter qui change. L'encodage de Boeham-Berarducci permet de les représenter dans un langage qui ne possède pas de types inductifs.

                          Sinon, la différence de performance semble également dépendre de la complexité des fonctions d'interprétations impliquées. Dans les tests précédents les fonctions étaient simples : l'identité pour les litéraux et l'addition pour les nœuds. En prenant la fonction de pretty printing cela change un peu la donne :

                            Name                    Time/Run    mWd/Run   mjWd/Run   Prom/Run   Percentage  
                           ----------------------- ---------- ---------- ---------- ---------- ------------ 
                            Trav/Ast-Perf:22           9.66s   581.74Mw   308.01Mw   543.01kw      100.00%  
                            Trav/Boehmdic-Perf:22      8.57s   581.74Mw   308.01Mw   544.31kw       88.69%  
                          

                          Là l'arbre a environ 8 millions de nœuds. Pour des arbres parfaits de 2000 à 500_000 nœuds, cela donne :

                            Name                    Time/Run       mWd/Run      mjWd/Run     Prom/Run   Percentage  
                           ----------------------- ---------- ------------- ------------- ------------ ------------ 
                            Trav/Ast-Perf:10          1.07ms      141.98kw       16.83kw      138.88w        0.25%  
                            Trav/Ast-Perf:12          4.91ms      568.06kw      106.25kw      556.69w        1.15%  
                            Trav/Ast-Perf:14         22.33ms    2_272.39kw      580.68kw    2_255.60w        5.22%  
                            Trav/Ast-Perf:16         99.55ms    9_089.71kw    2_945.12kw    8_802.56w       23.26%  
                            Trav/Ast-Perf:18        428.06ms   36_359.03kw   14_270.78kw   35_135.02w      100.00%  
                            Trav/Boehmdic-Perf:10     1.05ms      141.98kw       16.83kw      141.82w        0.24%  
                            Trav/Boehmdic-Perf:12     4.79ms      568.06kw      106.25kw      561.63w        1.12%  
                            Trav/Boehmdic-Perf:14    21.06ms    2_272.40kw      580.67kw    2_246.01w        4.92%  
                            Trav/Boehmdic-Perf:16    91.97ms    9_089.74kw    2_945.06kw    8_749.15w       21.48%  
                            Trav/Boehmdic-Perf:18   415.97ms   36_359.08kw   14_270.81kw   35_170.54w       97.18%  
                          

                          Et encore, ici il s'agit d'une structure simple : une seule opération binaire. Sur des langages plus riches, si les transformations sur l'arbre sont un peu plus complexes qu'une simple addition, il se peut bien que cette représentation soit plus performante comme le disait Perthmâd pour l'usage qui en est fait dans Coq.

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

              • [^] # Re: C'est bien la peine !

                Posté par (page perso) . Évalué à 2.

                Sympa.
                Ca me fait penser à la différentiation automatique ("AD"). N'est pas le genre d'approche programmatique qui est utilisée pour implanter l'AD?

              • [^] # Re: C'est bien la peine !

                Posté par . Évalué à 2.

                Intéressant ce bench, ce que j'y vois c'est que ça coûte super cher les fermetures.
                Sauf erreur de ma part lors d'une évaluation avec dans ASTk il y a deux fois plus de fermetures créée que dans Bohem (c'est Boehm à propos ;-))
                et dans AST il n'y en a pas, le tout pour autant de calculs utiles.

                Avec Bohem tu paye cher le fait d'avoir des fermetures à gogo, mais ma peut être intéressant si tu veux faire plein d'évaluation, genre tu as une algèbre paramétrée par des trucs et tu veux trouver des paramétrés qui font que ton expression a certaines propriétés ?

                le truc à remarquer c'est que si l'on deux expression identiques ea:ast et eb:bohem, alors en gros eb == fun f g -> fold f g ea,
                le lambda terme eb c'est le même que celui qui code fold appliqué partiellement sur ea, et donc pour chaque évaluation tu peux économiser le prix de ce fold.

                • [^] # Re: C'est bien la peine !

                  Posté par . Évalué à 1. Dernière modification le 15/06/16 à 23:48.

                  Sauf erreur de ma part lors d'une évaluation avec dans ASTk il y a deux fois plus de fermetures créée que dans Bohem (c'est Boehm à propos ;-))
                  et dans AST il n'y en a pas, le tout pour autant de calculs utiles.

                  Oui j'ai vu après pour le nom, j'espère qu'il ne m'en voudra pas trop. Dans la vidéo, il est même orthographié « Böhm ». C'est parce que j'écoute trop de jazz manouche, alors quand je lis « boehm », je fais inconsciemment la transformation en « bohem » (et puis sur une structure syntaxique donnée, on pose l'interprétation que l'on veut, non mais ! :-P); en plus musicalement c'est d'une qualité nettement supérieur au banana split1 de l'abominable homme des neiges (qui, soit dit en passant, abuse de la candeur d'une jeune adolescente). :-D

                  Pour le nombre de fermetures, je n'ai pas l'impression qu'il y en a plus dans le module Astk; c'est juste que l'on construit l'arbre avant de construire les fermetures, alors que dans le module Bohem ce sont les smart constructors qui construisent les fermetures. Tu devrais lire le lien que j'ai donné où gasche présente la transformation en CPS. Les enregistrements du premier module forme un réification sous forme de listes chaînées de fermetures du code en CPS.

                  Tout ces codes sont des façons différentes, au fond, d'implémenter un parcours en profondeur (depth-first search) de l'AST en commençant toujours par le sous-arbre gauche.


                  1. c'est une technique introduite dans la vidéo pour multiplier les interprétations avant de présenter l'encodage de Böhm-Berarducci, qui consiste à dire que si f:'a -> 'b et g: 'a -> 'c sont des fold alors h: 'a -> 'b * 'c = (f,g) est un fold

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

            • [^] # Re: C'est bien la peine !

              Posté par (page perso) . Évalué à 2.

              Je peux te prouver que c'est complet pour une raison bien simple : c'est exactement le fameux (et notoirement incompréhensible) visitor pattern de la programmation objet, mais typé de manière raisonnable…

              • [^] # Re: C'est bien la peine !

                Posté par . Évalué à 3.

                Je ne peux qu'appuyer ce commentaire. On trouve sur le blog d'un des membres de l'équipe de F# chez Microsoft toute une série d'articles sur les fold (dont le terme technique est catamorphisme) dont le troisième est consacré à l'application sur l'interprétation d'un AST, ce qui en POO serait fait via un visitor pattern.

                Il y a même eu un journal ici récemment où l'auteur explique comment faire un EDSL d'algèbre linéaire via les visitor pattern et les expressions template C++14.

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

Suivre le flux des commentaires

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