Merci ! Ça répond exactement à ma question. J'aurais du regarder directement là
Ma réponse du dessous tombe à l'eau, maintenant. :-P
Cependant on peut quand même se poser quelques questions parce que ce n'est pas vraiment rassurant de lire ensuite :
So, I conjecture that OCaml will not miscompile any Malfunction program, or at least that when it does, it will also miscompile a sufficiently contrived OCaml program.
Cela montre surtout qu'il reste encore du travail à faire dessus, mais tout comme lui, sa conjecture me semble plus que vraisemblable. Et il ajoute qu'en cas de problème cela révélerai surtout un bug dans le compilateur OCaml : ce qui est fort possible, il n'a pas été certifié.
Cela étant, il me semble que dans la famille des compilateurs C, seul CompCert est certifié et a résisté aux tests Csmith.
La question était : pourquoi ocaml ? […] Juste pourquoi le mec qui fait malfunction utilise ocaml. C'est tout.
En même temps, si tu ne lis pas les raisons données par le principal intéressé :
Why re-use OCaml's back-end specifically, when there are plenty of other compilers available? The central issues are efficiency and garbage collection.
Il aborde même la solution de Scheme à laquelle il objecte :
Dynamic languages, such as Scheme, Smalltalk or Javascript, are easy to compile to and have reasonably fast implementations. However, when running statically typed functional programs, time is wasted on runtime type checks.
Malfunction s'adresse aux personnes qui veulent obtenir rapidement un compilateur performant pour des langages fonctionnels statiquement typé (ce pourquoi ce langage est essentiellement du lambda-calcul non typé). Les systèmes de typage statique semble être le sujet d'étude de l'auteur, et l'exemple qu'il fournit pour Idris (écrit en Haskell) correspond à un langage avec types dépendants. Le développeur du langage peut alors se concentrer uniquement sur son type checker et sa compilation vers Malfunction qui se chargera alors de passer la main au back-end OCaml.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Oui, donc il faut encore plus une syntaxe spécifiée, c'est à dire, avec une spécification. Parce que bon, dépendre d'un truc qui peut casser à tout moment je trouve que c'est pas super. Ou alors il faut que ocaml puisse garantir une certaine stabilité de cette représentation intermédiaire, ce qui apparement n'est pas à l'ordre du jour.
La syntaxe (et la sémantique !) de Malfunction est spécifiée.
Pour le reste de tes interrogations, la lecture de sa présentation pour le ML Workshop t'éclairera peut être.
Malfunction is an untyped program representation intended as a compilation target for functional languages, consisting of a thin wrapper around OCaml's Lambda intermediate representation.
Compilers targeting Malfunction convert programs to a simple s-expression-based syntax with clear semantics, which is then compiled to native code using OCaml's back-end, enjoying both the optimisations of OCaml's new flambda pass, and its battle-tested runtime and garbage collector.
J'ai l'impression que Malfunction, dans l'esprit de son auteur, est dans la lignée d'un LLVM mais pour des langages fonctionnels statiquement typés avec gestion automatique de la mémoire. Scheme comme langage cible, par exemple, est exclus à cause de ses vérifications dynamiques de typage ce qui est une perte de temps pour des langages dont le bon typage est déjà vérifié à la compilation.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Je suis allé faire un tour sur le site du jeu, cela me semble prometteur ! :-) Une bonne pastiche d'une série genre X-Files.
J'avais suivi les jeux Lucas Arts jusqu'à Grim Fandago, on y retrouvait l'humour et les délires propres de cet éditeur mais j'ai été déçu du choix d'abandonner le principe du pur point&click (dans ce type de jeu, on s'en fout de pouvoir se déplacer comme on le souhaite dans un univers 3D à la manière d'un FPS).
Dans le genre aventure en mode point&click avec une bonne dose d'humour, j'ai également bien aimé la série des Chevaliers de Baphomet1 ou celle des Runaway. Et dans le genre casse-tête point&click en vue à la première personne, mais sans la touche humoristique, il y a l'inégalée — et inégalable ! — série des Myst.
Par exemple, et de mémoire, dans le deuxième volet il y a une énigme où il faut compter en base… 20 :-D ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
En fouillant bien dans mon bordel, je devrais pouvoir retrouver les disquettes 3''1/2 de certains d'entre eux. Sinon, je suppose qu'ils ne sont pas passés en abandonware ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Lucas Arts Games a sorti une série des jeux splendides sur SCUMM : les monkey island, maniac mansion, dott, sam & max… j'ai passé des heures sur ces jeux, ils étaient à mourir de rire entre leur scénario foldingue et les combinaisons improbables d'objets à effectuer. Ce type de jeu manque aujourd'hui.
Ils ont sorti une version remasterisée de Day of the tentacle cette année. Elle est sur steam mais seulement pour Windows, et la configuration matérielle minimale a bien évoluée :
Minimum:
Système d'exploitation : Windows 7
Processeur : 1.7 GHz Dual Core
Mémoire vive : 2 GB de mémoire
Graphiques : NVIDIA GeForce GTX 260, ATI Radeon 4870 HD, Intel HD 3000, or equivalent card with at least 512 MB VRAM
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
$ apt-cache search teapot
libglu1-mesa - Mesa OpenGL utility library (GLU)
$ apt-cache show libglu1-mesa
[...]
Description-en: Mesa OpenGL utility library (GLU)
GLU offers simple interfaces for building mipmaps; checking for the
presence of extensions in the OpenGL (or other libraries which follow
the same conventions for advertising extensions); drawing
piecewise-linear curves, NURBS, quadrics and other primitives
(including, but not limited to, teapots); tesselating surfaces; setting
up projection matrices and unprojecting screen coordinates to world
coordinates.
.
On Linux, this library is also known as libGLU or libGLU.so.1.
.
This package provides the SGI implementation of GLU provided by the
Mesa project (ergo the "-mesa" suffix).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
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 :
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.
Le séquoia ? :-D Cette espèce de conifère est issue de Californie, je ne suis pas certain qu'elle supporte une implantation sur le sol africain.
Je ne vois pas d'autre explication, bien que le rapport entre des « ateliers créatifs qui renforcent le lien social » et une langue de séquoia me semble toujours obscur (peut être une histoire de Pinocchio ?). :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
je suis entrain de me demander si je ne ferai pas mieux de changer de crémerie pour aller là où l'on respecte la communauté.
Mais là pour éviter toute possibilité de trolll à rallonge, il va falloir que tu trouves une distribution qui ne change pas de système d'init sans obtenir un consensus à l'unanimité. :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
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 :
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 :
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 :
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.
Cela étant, il n'est pas nécessaire que l'accès au code soit gratuit pour que le logiciel soit libre, de même que la gratuité de l'accès aux sources ne fait pas nécessairement du logiciel un logiciel libre. Même si je t'accorde que c'est la norme (l'accès aux sources d'un logiciel libre est généralement gratuite), il est tout à fait possible de faire payer l'accès aux sources tout en faisant du logiciel libre (vendre des logiciels libres par RMS). Le modèle économique par la vente de services étant bien sûr le plus répandu.
Autrement dit : l'accès gratuit aux sources d'un logiciel n'est ni une condition nécessaire, et encore moins une condition suffisante, pour en faire un logiciel libre.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
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.
Le problème de l'égalité structurelle en OCaml c'est qu'elle peut être indécidable, et partir dans un calcul sans fin :
letrecl=1::l;;letrecl=1::l;;vall:intlist=[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.
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.
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 :
moduleGADT=structtype(_,_)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,_)termletreceval:typeab.(a,b)term->int=function|Litn->n|Add(t,t')->(evalt)+(evalt')|Mult(t,t')->(evalt)*(evalt')|Div(t,t')->(evalt)/(evalt')letlitn=Litnletaddtt'=Add(t,t')letmulttt'=Mult(t,t')letdivtt'=Div(t,t')letsquare_add_onet:(int,[`NZ])term=(add(multtt)(lit1))endopenGADT;;lett1=square_add_one(lit(-3));;valt1:(int,[`NZ])term=Add(Mult(Lit(-3),Lit(-3)),Lit1)lett2=lit23;;valt2:(int,'_a)term=Lit23lett3=divt2t1;;valt3:(int,'_a)term=Div(Lit23,Add(Mult(Lit(-3),Lit(-3)),Lit1))evalt1,evalt2,evalt3;;-:int*int*int=(10,23,2)(* et si tu veux convertir au bon type dans la REPL, tu peux faire *)((lit4):>(int,[`NZ])term);;-:(int,[`NZ])term=Lit4
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.
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.
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.
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 :
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.
Posté par kantien .
En réponse au journal EDSL et F-algèbres.
Évalué à 1.
Dernière modification le 15 juin 2016 à 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.
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.
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.
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.
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 :
typeexp=Litofint|Opofexp*exp
on se donne des smart constructors pour notre langage et une fonction fold générique sur son AST :
à 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 :
moduleAst=struct(* l'AST du langage à un opérateur binaire sur les entiers *)typeexp=|Litofint|Opofexp*exp(* smart constructors *)letlitn=Litnletopee'=Op(e,e')(* fold générique sur l'AST *)letrecfoldfg=function|Litn->fn|Op(e,e')->g(foldfge)(foldfge')(* interprétation en tant qu'addition *)letplus=fold(funi->i)(+)(* interprétation en tant que soustraction *)letmoins=fold(funi->i)(-)(* profondeur de l'arbre *)letdepth=fold(funi->0)(fundd'->1+maxdd')(* conversions en chaîne de caractères *)letshow=foldstring_of_int(funss'->Printf.sprintf"(op %s %s)"ss')letshow_p=foldstring_of_int(funss'->Printf.sprintf"(%s + %s)"ss')letshow_m=foldstring_of_int(funss'->Printf.sprintf"(%s - %s)"ss')end
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 :
typeexp={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 :
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 :
moduleBohem=struct(* le type des expressions est une linéarisation de son propre fold *)typeexp={expi:'a.(int->'a)->('a->'a->'a)->'a}(* smart constructors *)letlitn={expi=(funfg->fn)}letop{expi=e}{expi=e'}={expi=funfg->g(efg)(e'fg)}(* interprétation en tant qu'addition *)letplus{expi=e}=e(funi->i)(+)(* interprétation comme soustraction *)letmoins{expi=e}=e(funi->i)(-)(* profondeur de l'arbre *)letdepth{expi=e}=e(funi->0)(fundd'->1+maxdd')(* conversions en chaîne de caractères *)letshow{expi=e}=estring_of_int(funss'->Printf.sprintf"(op %s %s)"ss')letshow_p{expi=e}=estring_of_int(funss'->Printf.sprintf"(%s + %s)"ss')letshow_m{expi=e}=estring_of_int(funss'->Printf.sprintf"(%s - %s)"ss')end
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 :
moduleAstk=struct(* l'AST du langage à un opérateur binaire sur les entiers *)typeexpr=|Litofint|Opofexpr*expr(* smart constructors *)letlitn=Litnletopee'=Op(e,e')(* fold en CPS via CPS conversion trick *)letfoldfge=letrecloopek=matchewith|Litn->k(fn)|Op(e,e')->loope(funie->loope'(funie'->k(gieie')))inloope(fune->e)(* interprétation en tant qu'addition *)letplus=fold(funn->n)(+)(* interprétation en tant que soustraction *)letmoins=fold(funn->n)(-)(* profondeur de l'arbre *)letdepth=fold(funn->0)(fundd'->1+maxdd')(* conversions en chaîne de caractères *)letshow=foldstring_of_int(funss'->Printf.sprintf"(op %s %s)"ss')letshow_p=foldstring_of_int(funss'->Printf.sprintf"(%s + %s)"ss')letshow_m=foldstring_of_int(funss'->Printf.sprintf"(%s - %s)"ss')end
Pour le pseudo-bench cela donne :
(* la liste des entiers [1; ...; n] *)letrangen=letrecloopaccn=ifn=0thenaccelseloop(n::acc)(predn)inloop[]n;;(* op (lit 0) (op (lit 1) op(... (lit n)) *)letastn=letopenAstinList.fold_left(funei->ope(liti))(lit0)(rangen);;letbohemn=letopenBoheminList.fold_left(funei->ope(liti))(lit0)(rangen);;letastkn=letopenAstkinList.fold_left(funei->ope(liti))(lit0)(rangen);;(* la fonction de mesure approximative du temps de calcul *)lettimef=fun()->letbefore=Unix.gettimeofday()infori=1to100dof()done;letafter=Unix.gettimeofday()inafter-.before;;(* trois mesures pour se faire une idée *)time(fun()->Ast.plus(ast100_000))();;-:float=3.21051192283630371time(fun()->Bohem.plus(bohem100_000))();;-:float=4.11348295211792time(fun()->Astk.plus(astk100_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: Représentations intermédiaires du compilateur OCaml
Posté par kantien . En réponse au journal Malfunction: réutiliser la représentation intermédiaire du compilateur OCaml. Évalué à 1. Dernière modification le 26 juin 2016 à 22:25.
Ma réponse du dessous tombe à l'eau, maintenant. :-P
Cela montre surtout qu'il reste encore du travail à faire dessus, mais tout comme lui, sa conjecture me semble plus que vraisemblable. Et il ajoute qu'en cas de problème cela révélerai surtout un bug dans le compilateur OCaml : ce qui est fort possible, il n'a pas été certifié.
Cela étant, il me semble que dans la famille des compilateurs C, seul CompCert est certifié et a résisté aux tests Csmith.
Pour ce qui est de la famille des compilateurs de la famille ML, j'ai cru comprendre que Jacques Garrigue avait certifié certaines implémentations.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Représentations intermédiaires du compilateur OCaml
Posté par kantien . En réponse au journal Malfunction: réutiliser la représentation intermédiaire du compilateur OCaml. Évalué à 3. Dernière modification le 26 juin 2016 à 22:07.
En même temps, si tu ne lis pas les raisons données par le principal intéressé :
Extrait de son abstract de présentation pour le ML Workshop, seconde partie : Why OCaml ?. ;-)
Il aborde même la solution de Scheme à laquelle il objecte :
Malfunction s'adresse aux personnes qui veulent obtenir rapidement un compilateur performant pour des langages fonctionnels statiquement typé (ce pourquoi ce langage est essentiellement du lambda-calcul non typé). Les systèmes de typage statique semble être le sujet d'étude de l'auteur, et l'exemple qu'il fournit pour Idris (écrit en Haskell) correspond à un langage avec types dépendants. Le développeur du langage peut alors se concentrer uniquement sur son type checker et sa compilation vers Malfunction qui se chargera alors de passer la main au back-end OCaml.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Représentations intermédiaires du compilateur OCaml
Posté par kantien . En réponse au journal Malfunction: réutiliser la représentation intermédiaire du compilateur OCaml. Évalué à 1. Dernière modification le 26 juin 2016 à 18:39.
La syntaxe (et la sémantique !) de Malfunction est spécifiée.
Pour le reste de tes interrogations, la lecture de sa présentation pour le ML Workshop t'éclairera peut être.
J'ai l'impression que Malfunction, dans l'esprit de son auteur, est dans la lignée d'un LLVM mais pour des langages fonctionnels statiquement typés avec gestion automatique de la mémoire. Scheme comme langage cible, par exemple, est exclus à cause de ses vérifications dynamiques de typage ce qui est une perte de temps pour des langages dont le bon typage est déjà vérifié à la compilation.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: 18 ans de DLFP
Posté par kantien . En réponse au journal Quake. Vingt ans déjà. Évalué à 1.
Je suis allé faire un tour sur le site du jeu, cela me semble prometteur ! :-) Une bonne pastiche d'une série genre X-Files.
J'avais suivi les jeux Lucas Arts jusqu'à Grim Fandago, on y retrouvait l'humour et les délires propres de cet éditeur mais j'ai été déçu du choix d'abandonner le principe du pur point&click (dans ce type de jeu, on s'en fout de pouvoir se déplacer comme on le souhaite dans un univers 3D à la manière d'un FPS).
Dans le genre aventure en mode point&click avec une bonne dose d'humour, j'ai également bien aimé la série des Chevaliers de Baphomet1 ou celle des Runaway. Et dans le genre casse-tête point&click en vue à la première personne, mais sans la touche humoristique, il y a l'inégalée — et inégalable ! — série des Myst.
Par exemple, et de mémoire, dans le deuxième volet il y a une énigme où il faut compter en base… 20 :-D ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: 18 ans de DLFP
Posté par kantien . En réponse au journal Quake. Vingt ans déjà. Évalué à 1.
En fouillant bien dans mon bordel, je devrais pouvoir retrouver les disquettes 3''1/2 de certains d'entre eux. Sinon, je suppose qu'ils ne sont pas passés en abandonware ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: 18 ans de DLFP
Posté par kantien . En réponse au journal Quake. Vingt ans déjà. Évalué à 3.
Lucas Arts Games a sorti une série des jeux splendides sur SCUMM : les monkey island, maniac mansion, dott, sam & max… j'ai passé des heures sur ces jeux, ils étaient à mourir de rire entre leur scénario foldingue et les combinaisons improbables d'objets à effectuer. Ce type de jeu manque aujourd'hui.
Ils ont sorti une version remasterisée de Day of the tentacle cette année. Elle est sur steam mais seulement pour Windows, et la configuration matérielle minimale a bien évoluée :
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: 18 ans de DLFP
Posté par kantien . En réponse au journal Quake. Vingt ans déjà. Évalué à 3.
Mon premier jeu sur PC : castle adventure, et la machine : IBM PC et ses disquettes molles 5''1/4. Putain, j'suis vieux !
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Mais moi aussi je veux jouer !
Posté par kantien . En réponse au journal Coup de boost sur le pilote graphique Intel. Évalué à 3.
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 kantien . En réponse au journal EDSL et F-algèbres. É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 :
Là l'arbre a environ 8 millions de nœuds. Pour des arbres parfaits de 2000 à 500_000 nœuds, cela donne :
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: la langue de bois !!!
Posté par kantien . En réponse à la dépêche Jerry Do-It-Together assembler un ordinateur dans un bidon de 20 litres. Évalué à 1.
Le séquoia ? :-D Cette espèce de conifère est issue de Californie, je ne suis pas certain qu'elle supporte une implantation sur le sol africain.
Je ne vois pas d'autre explication, bien que le rapport entre des « ateliers créatifs qui renforcent le lien social » et une langue de séquoia me semble toujours obscur (peut être une histoire de Pinocchio ?). :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Javascript
Posté par kantien . En réponse au journal Lettre à mon copain Errol. Évalué à 1.
Dans ce cas, rien ne vaut un navigateur quantiquement intriqué avec le serveur ! \o/
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Mise à jour d l'article sur Clubic
Posté par kantien . En réponse au journal UBUNTU vs OVH : ça vous choque ?. Évalué à 2.
Mais là pour éviter toute possibilité de trolll à rallonge, il va falloir que tu trouves une distribution qui ne change pas de système d'init sans obtenir un consensus à l'unanimité. :-P
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 kantien . En réponse au journal EDSL et F-algèbres. É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 :
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 :
et vers la droite pour de petites tailles :
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 kantien . En réponse au journal EDSL et F-algèbres. É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 :
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.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Mise à jour d l'article sur Clubic
Posté par kantien . En réponse au journal UBUNTU vs OVH : ça vous choque ?. Évalué à 8.
Canonical aurait du passer un contrat etherum avec la communauté. :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Non
Posté par kantien . En réponse à la dépêche Pour sauver AbulÉdu, nous lançons une campagne de financement participatif. Évalué à 1.
Cela étant, il n'est pas nécessaire que l'accès au code soit gratuit pour que le logiciel soit libre, de même que la gratuité de l'accès aux sources ne fait pas nécessairement du logiciel un logiciel libre. Même si je t'accorde que c'est la norme (l'accès aux sources d'un logiciel libre est généralement gratuite), il est tout à fait possible de faire payer l'accès aux sources tout en faisant du logiciel libre (vendre des logiciels libres par RMS). Le modèle économique par la vente de services étant bien sûr le plus répandu.
Autrement dit : l'accès gratuit aux sources d'un logiciel n'est ni une condition nécessaire, et encore moins une condition suffisante, pour en faire un logiciel libre.
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 kantien . En réponse au journal EDSL et F-algèbres. Évalué à 1.
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.
Le problème de l'égalité structurelle en OCaml c'est qu'elle peut être indécidable, et partir dans un calcul sans fin :
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 :
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'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.
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 kantien . En réponse au journal EDSL et F-algèbres. Évalué à 1.
Pour ta première question la première idée qui me vient à l'esprit c'est les variants polymorphes :
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 kantien . En réponse au journal EDSL et F-algèbres. É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 :
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 kantien . En réponse au journal EDSL et F-algèbres. Évalué à 1.
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 ?
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 kantien . En réponse au journal EDSL et F-algèbres. Évalué à 1.
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 :
La technique avec construction de l'AST puis interprétation via un
foldsur 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'unfold.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 :
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 yest interprétée parSub x (Sub (Lit 0) y).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 kantien . En réponse au journal EDSL et F-algèbres. Évalué à 1. Dernière modification le 15 juin 2016 à 23:48.
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.
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 -> 'betg: 'a -> 'csont desfoldalorsh: 'a -> 'b * 'c = (f,g)est unfold. ↩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 kantien . En réponse au journal EDSL et F-algèbres. É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.
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par kantien . En réponse au journal EDSL et F-algèbres. É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: C'est bien la peine !
Posté par kantien . En réponse au journal EDSL et F-algèbres. É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
exppour l'AST du langage :on se donne des smart constructors pour notre langage et une fonction
foldgénérique sur son AST :à 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:Il s'utilise simplement dans une boucle REPL :
Maintenant, on passe à l'encodage de Bohem-Berarducci. L'idée est de faire du type
expune « linéarisation » de l'arbre d'éxecution dufoldde l'AST précédent. La fonctionfoldavait pour type(int -> 'a) -> ('a -> 'a -> 'a) -> exp -> 'a, le nouveau type sera donc :Le champ
expiprend deux fonctionsfetget renvoie un objet de type'aqui constitue l'interprétation de l'expression pour les fonctionsfetg, comme le faisait lefoldpour l'AST.On retrouve ensuite nos smart constructors qui mime les deux branches du
fold:La seule différence notable est dans le cas de
opou l'expressionfold f g edeviente f g, étant donné queeest 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
foldpar le champexpidu type des expressions; et on obtient le module :Il s'utilise comme le précédent :
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
foldrécursif terminal en appliquant la transformation CPS décrite ici par gasche, ce qui donne ce module :Pour le pseudo-bench cela donne :
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.