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 :
- 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
- 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
- L'encodage de Böhm-Berarducci des types récursifs
- 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 Perthmâd (site web personnel) . É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 kantien . Évalué à 3.
Il y a des perles magnifiques dans cette histoire brève, incomplète et globalement erronée ! :-)
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 wolowizard . É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 benja . É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).
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . É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 benja . Évalué à 1. Dernière modification le 13 juin 2016 à 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:
Tu le changes en
Et tu changes tes evals
comme ceci
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 Nicolas Boulay (site web personnel) . É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 benja . Évalué à 1. Dernière modification le 13 juin 2016 à 16:06.
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.
C'est la destruction par pattern-match, équivalent à "fun record -> let e = record.expi in …"
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.
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par benja . Évalué à 1. Dernière modification le 13 juin 2016 à 16:17.
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 Nicolas Boulay (site web personnel) . É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 Aluminium95 . Évalué à 1.
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 Nicolas Boulay (site web personnel) . Évalué à 3.
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 Aluminium95 . É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, commeid, qui est de type(n,n)quelque soit len.Comme on demande du code, voilà un AST classique (sans construction qui utilise des fonctions) :
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 :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 :
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
Idtout 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 Nicolas Boulay (site web personnel) . É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 Aluminium95 . É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
Setrepré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 duO( n log n)oùnest 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 Nicolas Boulay (site web personnel) . Évalué à 2.
Si tu as un :
typedef int toto_t;
...
toto_t toto = 1;
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par kantien . É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 Nicolas Boulay (site web personnel) . É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 Aluminium95 . É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
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 Nicolas Boulay (site web personnel) . Évalué à 2.
Je me dis la même chose en lisant les pattern de code plus haut :)
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 ?
Euh…
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Aluminium95 . Évalué à 1.
Visiblement on est pas très fort pour communiquer :-).
Je vais faire du pas à pas sur un exemple :-p.
L'arbre pourrait ressembler à ça :
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
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 avecunion_set.Je n'écris pas la fonction en entier, mais voilà comment ça tourne :
Alors j'ai très mal choisi la notation
EQqui 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 Nicolas Boulay (site web personnel) . É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 Aluminium95 . Évalué à 1.
Exactement ! C'est ce que je voulais dire par « enrichir la sortie ».
De rien :-).
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par kantien . É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: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . É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 kantien . É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 Nicolas Boulay (site web personnel) . É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 kantien . É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 Nicolas Boulay (site web personnel) . É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 kantien . É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 Nicolas Boulay (site web personnel) . É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 :
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.
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
"La première sécurité est la liberté"
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par kantien . É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 Nicolas Boulay (site web personnel) . Évalué à 2.
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.
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 kantien . Évalué à 1. Dernière modification le 13 juin 2016 à 19:42.
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 benja . É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 kantien . Évalué à 1. Dernière modification le 14 juin 2016 à 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 :
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 kantien . Évalué à 1.
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 foobarbazz . É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 GTof . Évalué à 2.
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 Axioplase ıɥs∀ (site web personnel) . Évalué à 3.
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 Aluminium95 . Évalué à 1.
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.
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 :
'a expr: parfait !! Seulement, il ne dit pas vraiment ça. Il dit'a exprpour une certaine valeur de'a(id,+), le gentil compilateur dit : « ok j'ai compris, en fait'a = int! ».(string_of_int, ^)il dit … ohlala.'a = intmais'a = string… orstring /= 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 Axioplase ıɥs∀ (site web personnel) . É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 kantien . Évalué à 1. Dernière modification le 14 juin 2016 à 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 :
Le terme technique pour la fonction
foldest 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 donnereval1,eval2eteval3.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 Nicolas Boulay (site web personnel) . É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 kantien . Évalué à 1. Dernière modification le 14 juin 2016 à 11:08.
L'utilité du
foldest 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 fonctionfold.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 Nicolas Boulay (site web personnel) . É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 benja . Évalué à 1. Dernière modification le 14 juin 2016 à 11:55.
Cette méthode utilise un encoding qui permet de se passer de la récursion.
raté :p
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 ?
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 ;-)
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 ??
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 kantien . Évalué à 1. Dernière modification le 14 juin 2016 à 13:06.
Je n'avais pas lu le code d'Oleg. ;-)
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).
J'étais parti sur du higher-kinded, et j'admets que ce n'est pas la seule approche. Mais passer par
Obj.magicquand on peut l'éviter, il faut aimer jouer avec le feu ;-)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 :
et comme tu le soulignes, avec l'encodage du journal les allocations sont juste « déplacées ».
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
foldgé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 Perthmâd (site web personnel) . Évalué à 3.
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 kantien . É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 Perthmâd (site web personnel) . Évalué à 3.
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 Axioplase ıɥs∀ (site web personnel) . É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 Aluminium95 . Évalué à 1.
Je ne comprend pas cette phrase, que veux-tu dire ?
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
foldest suffisant pour tout construire …[^] # Re: C'est bien la peine !
Posté par Axioplase ıɥs∀ (site web personnel) . Évalué à 2.
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 kantien . É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.
[^] # Re: C'est bien la peine !
Posté par Nicolas Boulay (site web personnel) . É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 kantien . É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: C'est bien la peine !
Posté par Nicolas Boulay (site web personnel) . É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 kantien . É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 Nicolas Boulay (site web personnel) . É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 kantien . É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: C'est bien la peine !
Posté par Axioplase ıɥs∀ (site web personnel) . É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 foobarbazz . É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:asteteb:bohem, alors en groseb == fun f g -> fold f g ea,le lambda terme
ebc'est le même que celui qui code fold appliqué partiellement surea, et donc pour chaque évaluation tu peux économiser le prix de ce fold.[^] # Re: C'est bien la peine !
Posté par kantien . É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 Perthmâd (site web personnel) . É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 kantien . É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: C'est bien la peine !
Posté par Axioplase ıɥs∀ (site web personnel) . Évalué à 2.
Super liens. L'exemple du troisième article est ce que j'aurais voulu lire dans ce journal.
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.