Petite coquille ? "Lorsque l'on a supprimé les littéraux nuls, on a au fond transformer" J'ai un doute sur "transformer" qui me semblerait plus judicieux en "transformé".
Effectivement, petite faute d'accord. Si un modérateur pouvait corriger. J'en ai repéré une autre avec un seul « t » au lieu de deux à littéraux : « La première optimisation que l'on va voir est celle qui consiste à supprimer tous les litéraux nuls ».
J'avais lu l'article de Oleg Kiselyov à ce propos et je trouve l'approche tagless très élégante.
Sur son site on trouve également une lecture où il expose encore plus en détail toutes les possibilités de l'approche et en Haskell. Les fichiers de code sont accessibles ici.
Hormis dans le cas d'un arbre syntaxique pour évaluer des expression pour faire un compilateur, est-ce que tu vois un autre usage des GADTs ? Cela fait partie des fonctionnalités qui me frustrent car elles apparaissent très puissantes mais au final je ne trouve jamais l'occasion de m'en servir.
Les possibilités des GADT mériteraient plus d'un journal pour être présentées. La leçon de Jeremy Yallop sur le sujet illustre des cas d'usage qui vont bien au-delà de l'écriture de compilateur.
b) Est-ce que les modules OCaml peuvent être vu comme un sur-ensemble ou un sous-ensemble (ou rien à voir) des typeclasses d'Haskell.
Je dirais un sur-ensemble : tout ce que font les typeclasses peuvent être fait avec les modules, mais la réciproque ne marche pas — il me semble. Pour les différents niveaux d'abstraction accessibles en OCaml, il y a ces deux leçons de Leo White : abstraction et parametricty.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Justement, je voudrais les exemples de chaque étape, y compris le premier.
Je ne suis pas sur de comprendre. Tu voudrais par exemple un dépôt avec :
un fichier pour le langage sur les entiers avec AST codé par un variant ;
un fichier pour le langage étendu avec les booléens codé avec un GADT ;
des fichiers pour les mêmes langages mais codés selon la méthode tagless-final.
C'est cela ? Afin de pouvoir mieux comparer les codes et les méthodes ?
Les fichiers dont tu parles doivent être bien trop compliqué pour comprendre le principe.
C'est pas faux. Sans avoir besoin d'avoir bien compris le principe de la méthode — ils sont avant tout là pour l'illustrer sur un exemple — il vaut mieux en avoir une idée au moins approximative dans un premier temps.
J'ai codé pendant 2 ans en ocaml fonctionnel simple. Et tout ce qui est foncteur/module, et les opérateurs spécifiques (@@) me semblent bien étrange et peu lisible.
Je n'ai toujours pas compris en quoi un module est si différent d'un objet ou d'une classe.
Pour ce qui est de l'opérateur @@ c'est une question de goût personnel pour éviter d'avoir trop de parenthèses et séparer visuellement les fonctions de leurs arguments. Cela permet d'écrire :
f@@g@@h@@x(* au lieu de *)f(g(hx))(* comme dans ce bout de code issu du journal *)letlamf=fwd@@I.lam@@funx->bwd(f(fwdx))(* que j'aurai pu tout aussi bien écrire *)letlamf=fwd(I.lam(funx->bwd(f(fwdx))))(* ou encore avec plus de @@ *)letlamf=fwd@@I.lam@@funx->bwd@@f@@fwdx
Pour ce qui est des modules par rapport aux objets, ils ont un point commun : ce sont des enregistrements extensibles; et on aurait pu faire la même chose avec des objets. C'est ce qu'à fait Philipp Wadler en 1998 quand il a proposé sa solution au problème de l'extension sur la liste de diffusion Java Generics. Mais il faut utiliser le vistor pattern, et je préfère l'approche du fold qui dans cette solution est jouée par le rôle des foncteurs. Un foncteur est au fond une fonction des modules vers les modules, c'est plus « fonctionnel » dans le principe. On peut écrire une signature de foncteur ainsi :
moduletypeF=S1->S2(* ou S1 et S2 sont des signatures de modules *)
L'encodage de Böhm-Berarducci, qui utilise des enregistrements, marche bien tant que le langage que l'on plonge a un seul type de données, comme le premier exemple qui n'a que des int. Mais il devient lourd, voir impossible à utiliser quand ce langage a plus d'un type de données : int, bool, fonctions… Alors au lieu d'utiliser des enregistrements, on utilise des modules (ou des objets) qui sont une généralisation et une abstraction supplémentaire au-dessus des enregistrements.
Pour ce qui est du rapport entre le fold et le vistitor pattern de la POO, Perthmâd l'avait signalé dans la discussion et j'ai donné des liens en réponse à son commentaire.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Cela serait bien de proposer le code complet minimal par exemple (github ?). C'est parfois pas évident de comprendre les dépendances entre bout de code.
Pourquoi pas. Il faudrait par contre que j'apprenne à me servir git et github. Tu connais un tutoriel pour une prise en main rapide du système ?
Pour ce qui est du code que tu voudrais voir. Pourrais-tu être plus précis sur ce que tu attends ?
Il y a un tutoriel avec plusieurs fichiers de code sur le langage des circuits logiques. Le code est complet et commenté, c'est cela que tu veux ? Là, Oleg utilise en plus la bibliothèque higher de Jeremy Yallop et Leo White. Cela lui permet de faire du higher-kinded polymorphism pour « dissimuler » le paramètre 'a du type 'a obs, d'utiliser ainsi des modules de première classe et de manipuler les foncteurs comme des fonctions normales.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
De rien. Cela m"a pris aussi du temps pour bien comprendre les tenants et aboutissants de la méthode. Écrire ce journal m'a permis de mieux l'assimiler, et il a connu plusieurs versions en fonction de l'évolution de ma compréhension.
Si tu as des questions sur des points précis de code ou sur les principes méthodologiques, n'hésite pas. J'essaierai de clarifier la chose du mieux que je peux.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Je ne pense pas, tu risques d'obtenir le code d'une fonction qui est extentionnellement égale, mais dont le graphe d'évaluation des fermetures pendant le calcul correspond à un évaluateur (du programme après évaluation partielle). Mais il faut tester !
Exact ! J'ai bien aussi tenté avec le unbox-closure de flamba pour voir s'il avait assez d'infos pour s'en sortir mais ça n'a rien donné.
Quoi qu'il en soit ce n'est pas l'essentiel, ce qui m'intrigue c'est la ressemblance dans certains codages sur le plan syntaxique.
Par exemple dans leur article, pour le code de leur compilateur (le module qui interprète la signature en ayant recours à MetaOCaml) pour lam et app on a :
ce qui est au fond les fonctions back : ('a code -> 'b code) -> ('a -> 'b) code et forth : ('a -> 'b) code -> 'a code -> 'b code de la première leçon de Jeremy.
De l'autre côté, pour traiter le cas statique dans la méthode tagless final (ce qui est au fond une automatisation du binding-time analysis de la lecon 2) il m'a fallu utiliser les types suivants :
type_repr=|Dyn:'afrom->'arepr|Sta:'a*'afrom->'arepr|Fun:('arepr->'brepr)->('a->'b)repr(* le type de back *)
Avant d'arriver à ce choix, j'avais fait d'autres essais pour le cas des fonctions (dont un qui m'obligeait à utiliser l'option rectypes) mais rien ne fonctionnait. Il y a aussi le code correspondant :
(* pour le compilateur en MetaOCaml *)letlamf=.<funx->.~(f.<x>.)>.(* pour la branche du cas fonctionnel dans `bwd` *)Funf->I.lam(funx->bwd(f(fwdx)))
ce qui montre une similitude d'usage entre quote et escape d'un côté, puis bwd et fwd de l'autre.
Ensuite, dans le cadre de la correspondance de Curry-Howard, il semblerait que pour typer une fonction similaire au quote du LISP il faille recourir à l'axiome du choix ou une de ses variantes : Dependent choice, quote and the clcok. Je dois reconnaître que je n'ai pas tout saisi à l'article et aux techniques utilisées, mais je fais confiance à son auteur.
C'est aussi un sport en mathématique de chercher à prouver un énoncé avec le moins d'axiomes possibles et l'axiome du choix est un cas à part : c'est globalement le seul où on pourra trouver des énoncés qui précise explicitement que l'on en fait usage dans la preuve. Dans un dépêche récente présentant un projet d'ouvrage sous licence libre pouvant servir de référence aux candidats à l'agrégation, j'avais fait un commentaire répondant à une demande de preuve sans recourir à cet axiome. La demande était un peu étrange, cela portait sur une question de théorie de la mesure et habituellement quand on demande à un logicien ce qu'il entend par analyse, il répond tout de go : l'arithmétique du second ordre avec axiome du choix dénombrable. C'est la base qui permet de formaliser le calcul intégrale, la théorie de la mesure, l'analyse réelle et complexe… en gros toutes les mathématiques dont ont besoin les physiciens et ingénieurs.
De son côté Gödel avait montré que l'on pouvait l'ajouter aux autres axiomes de la théorie des ensembles sans contradiction en construisant inductivement un univers du discours qui le satisfaisait. Il a construit un univers stratifié où à chaque rang on ne peut parler que des objets de rangs inférieurs ou du rang actuel mais pas des rangs supérieurs encore à venir. L'analogie avec l'approche de MetaOCaml est ses strates ou stage suscite chez moi bien des interrogations.
Pour ce qui est de la possibilité d'utiliser les GADT et la technique du lift générique pour obtenir cette structure stratifiée, je reste dans l'interrogative. Bonne idée à explorer ? fausse piste ? je n'en sais rien. Faut-il adapter le niveau meta du compilateur comme à l'heure actuelle, ou sera-t-il possible de le ramener à une bibliothèque ? le futur le dira. Mais d'après Oleg :
It is now a distinct possibility that MetaOCaml becomes just a regular library or a plug-in, rather being a fork.
Wait and see, comme on dit.
Pour ce qui est de ta dernière remarque :
(Je trouve aussi que ta réponse à benja est trop sèche. C'est un sujet compliqué et c'est un peu normal que les gens se parlent un peu à travers.)
je le reconnais. Mais il y a un certain passif avec benja, cela a du influencé ma réaction. Il m'a enquiquiné sur des détails sans importance (que je n'ai toujours pas compris) en commentaire à ma dépêche de présenttaion du MOOC OCaml. Son ton de l'époque n'était pas des plus plaisant (dans le même genre que celui d'Aluminium dans ton journal de présentation de Malfunction) et il passait complètement à côté du sujet et de l'essentiel de mon propos.
afin de montrer l'analogie entre l'analyse de type et l'analyse grammaticale, en me focalisant sur l'analyse du groupe adverbiale « 5 fois ». Exemple qui m'avait été inspiré par des échanges au cours d'un dépêche sur le standard C++17 et un conférence de Gérard Huet. Conférence intitulée Fondements de l'informatique, à la croisée des mathématiques, de la logique et de la linguistique dont je cite ici in extenso un passage :
On nous dit « il faut inculquer aux jeunes l’esprit scientifique ». Très bien, mais qu’est ce que ça veut dire au juste, au-delà d’une incantation un peu creuse ? Inculquer l’esprit scientifique ne se fait pas à coup de bourrage de crâne de connaissances scientifiques rebutantes, ce qui est au contraire la meilleure manière de faire fuir les élèves. De toutes façons, la science moderne est trop vaste et trop complexe pour que quiconque puisse tout connaître, on n’aura plus de Pic de la Mirandole, et c’est aussi bien. Par contre, on peut susciter la curiosité des élèves en mettant en valeur les figures de rhétorique développées par la science pour acquérir ces connaissances. Pour avoir prononcé ce terme de rhétorique devant vous, je devrais m’excuser, c’est un terme vieillot. Autrefois, il y avait des classes de rhétorique, et la notion de débat intellectuel était valorisée. Maintenant c’est terminé, on inculque des connaissances prédigérées, et la Science est imposée comme un prêche. On apprend par cœur des formules que l’on fait réciter, les exercices sont calibrés pour être résolus par application mécanique d’un cours bien saucissonné, l’esprit critique n’est pas encouragé. Ouvrons la fenêtre, discutons des méthodes qui permettent de raisonner droit, de comprendre comment poser des hypothèses, d’élaborer des conjectures, de chercher des contre-exemples. Ces méthodes sont transversales à toutes les matières enseignées, littéraires comme scientifiques. Il y a là un lien important entre philosophie et informatique, car la méthodologie informatique prolonge la rhétorique traditionnelle en tant que moyen légitime d’acquérir des connaissances. Ce sont ces préoccupations qui ont développé la logique, qui a finalement quitté la philosophie pour s’intégrer aux mathématiques, mais a perdu en passant sa finalité argumentative, qui est l’essence de la démarche scientifique. […]
Je vais prendre un autre exemple dans un domaine complètement différent, c’est l’analyse grammaticale dans la classe de français. Je ne sais pas si on fait encore beaucoup ça, mais de mon temps on décortiquait les phrases : toute phrase doit avoir un verbe, tout verbe doit avoir un sujet. Là, il y a un petit bout de raisonnement aussi. Comment est-ce que l’on obtient une phrase à partir d’un verbe ? Prenons d’abord un verbe intransitif. Un verbe intransitif a besoin d’un sujet pour exprimer son action. Donc, vous pouvez voir le rôle fonctionnel de ce verbe comme utilisant le syntagme nominal représentant le sujet pour construire la phrase représentant l’action. De même, un verbe transitif peut être vu comme une fonction qui prend son complément d’objet pour construire un syntagme verbal, se comportant comme un verbe intransitif. Vérifier que « le chat mange la souris » est une phase correcte devient un petit raisonnement où le verbe « mange » prend la souris pour construire « mange la souris », objet fonctionnel qui peut maintenant manger le chat, si je puis dire, pour donner la phrase. Le petit arbre de raisonnement, qui exprime la composition des deux fonctions en vérifiant leurs types, hé bien, c’est ce qu’on appelle l’analyse grammaticale de la phrase. Regardez de près, vous vous rendez compte que c’est exactement le même raisonnement que celui pour la machine à laver du cours de physique, avec deux étapes de modus ponens. L’analyse dimensionnelle devient l’analyse grammaticale. C’est important, en exhibant les procédés rhétoriques similaires on abstrait le raisonnement commun, pour lequel les deux disciplines fournissent des exemples concrets. Les deux exemples s’éclairent l’un l’autre, et on retient un procédé cognitif général qui peut servir pour toutes sortes d’autres investigations. En exhibant le procédé rhétorique commun, et en le réifiant dans deux disciplines supposées étanches l’une à l’autre, on apprend aux élèves que l’esprit scientifique transcende les matières enseignées et les présente comme des aventures intellectuelles cohérentes. Et puis, cela peut donner des idées. En classe de français on faisait de l’analyse grammaticale, mais on n’en faisait pas en classe d’anglais. Pourquoi ? Le même type de raisonnement s’applique, et on montre deux exemples du même phénomène, qui est ainsi mieux mémorisé. Par contre il y a des détails de grammaire qui ne sont pas les mêmes. Par exemple, en introduisant les paramètres morphologiques, on va pouvoir exprimer l’accord du verbe avec son sujet comme une contrainte sur les arbres d’analyse. En français comme en anglais. Par contre, l’adjectif est invariable en anglais, et donc ne s’accorde pas avec le nom qu’il qualifie. En mettant en lumière ces différences structurelles fondamentales, on éclaire les difficultés rencontrées par les élèves, les faux amis, les analogies erronées qui sont difficiles à déraciner. C’est important de le montrer en contraste avec le français. Parce que si vous leur apprenez l’analyse grammaticale du français, il y a une grande partie qu’ils vont pouvoir appliquer à l’anglais aussi, et les parties où cela ne s’applique pas, c’est justement les endroits où il faut faire attention à ne pas calquer d’une langue sur l’autre.
Selon benja, dans mon exemple, mon intention était de « singer les normes du français » (sic). Dois-je lui préciser que Gérard Huet a eu pour thésard Thierry Coquand (à l'origine du langage Coq) et Xavier Leroy (à l'origine du langage OCaml) ? Cherche-t-il lui aussi à singer la grammaire française en comparant le typage des fonctions dans le lambda-calcul avec le fonctionnement des verbes transitifs et intransitifs ? Ou encore avec l'analyse dimensionnelle en physique ? Et de voir que le point commun formel entre tout cela est la forme des jugements hypothétiques et la règle du modus ponens. Dois-je aussi signaler, en passant, que cette forme des jugements hypothétiques et de son principe du modus ponens est le type que donna Kant au principe de causalité dans la Critique de la Raison Pure dans ce qu'il appela logique transcendantale ?
Pour sa seconde remarque sur son insistance à désapprouver le fait que j'appelle fold la fonction générique pour traverser une structure en remplaçant ses constructeurs par des applications de fonctions, je n'ai toujours pas compris.
L'attitude qu'il a eu à l'époque, non dans le faits de faire des remarques ou des critiques, mais dans le ton employé est justement ce qui à tendance à m'énerver sur ce site : c'est trop fréquent, pour tout et n'importe quoi. J'en ai ma claque ! Et là j'ai eu le sensation à demi-mot qu'il prenait le même chemin : j'ai dégainé direct. Oui je sais ce que fait MetaOCaml : pas besoin de chercher à me l'expliquer. Mon intention n'était pas tant d'affirmer que d'interroger. Jusqu'à quel point l'approche de MetaOCaml et de la méthode tagless final se ressemble-t-elle ? Cette dernière, qui a également été mise au point par Oleg Kiselyov auteur de BER MetaOcaml, est-elle un piste envisageable pour atteindre un objectif qu'il semble avoir lui-même ?
It is now a distinct possibility that MetaOCaml becomes just a regular library or a plug-in, rather being a fork.
source :A brief history of (BER) MetaOCaml
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Après, je ne suis pas développeur ni informaticien, mais mathématicien et logicien. Ce que j'aime c'est retrouver mes « petits », et là cela me parle. Pour l'intérêt pratique, ce n'est pas mon domaine.
Mais au delà du problème de l'extensibilité (c'est un des points), c'est la structure modulaire et composable des optimisations que je trouve élégante. Et comme via le lift générique on a bwf (fwd x) = x quand on ne touche pas à un terme dans une passe, on a une phénomène qui ressemble au cross-stage persistence de MetaOCaml. Ça titille ma curiosité théorique ! :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
1) le type "optimisé" est une conséquence de l'utilisation des GADT et ne présume en rien de l'efficacité de l'implémentation
Non rien à voir, là où les GADT sont absolument nécessaire c'est pour avoir un lift générique : Dyn : 'a from -> ' a term. Ce qui permet d'avoir une approche semblable à le réduction par évaluation (via les fonctions fwd et bwd qui assurent que bwd (fwd x) = x) et de rester coller à la sémantique dénotationnelle. C'est ce qui permet de réutiliser une passe dans les langages qui étendent celui pour lequel elle est faite.
Dans mes textes, j'ai un joli dessin en ASCII art qui pourra plaire aux catégoriciens :
(*
Pour le lecteur qui aime bien les graphes voici le processus général :
Domaine 'a from : terme t t optimisé ------> t observé : 'a obs
| ^ F.observe
| |
fwd | | bwd
| |
V passe |
Domaine 'a term : terme t' -------> t' optimisé
lit add
*)
2) de fait, tu as encore besoin d'un interprêteur, eval : 'a repr -> 'a.
Dans leur article, Kiselyov et al. appelle cet interprète metacirculaire, car on replonge le langage dans OCaml en interprétant un terme… par lui-même. ;-)
Si tu veux voir les différents stages à la façon de MetaOCaml voilà le type exact de la représentation interne :
Chaque passe d'optimisation crée un « stage » lié à la succession d'application de foncteur. Donc au lieu de voir toute la chaîne comme un graphe plan, tu peux le voir comme une succession de cube en profondeur :
j'en profite pour te conseiller la lecture du papier "module mania" qui explique comment faire un interpréteur "extensible" sans gadt et sans first-class module.
Merci, déjà lu.
Metaocaml joue dans une autre catégorie en permettant 1) de spécialiser/optimiser au niveau natif (vs au niveau de l'interpréteur) 2) d'avoir du multistage et de la fiabilité (ce que tu perdrais en transformant ton interpréteur en générateur de code).
C'est là qu'est toute mon interrogation. Ma fonction retournée par mon optimiseur est bien fun x y -> 3 + (x + (7 + (y + 11))). Bon le plus simple serait que je compile un exemple en natif et que je ragarde le dump cmm sur un cas genre :
pour voir si le code de f est bien celui que je pense. Ma question reste : que ne peut-on pas faire avec l'approche tagless final qui nécessite le recours à MetaOCaml ? Mon interrogation est : ne peut on pas voir le processus comme « avec un fwd je monte d'un étage et avec un bwd je reviens dans l'étage du dessous, jusqu'à revenir au niveau 0 'a = 'a » ?
Il y a un côté inception dans le processus, comme avec MetaOCaml, le tout étant de ne pas rester coincer dans les limbes. :-P
Mon instinct me dit que tu devrais pouvoir utiliser metaocaml pour implémenter ton "eval" de manière efficace tout en conservant ton architecture d'extension par modules.
Mon instinct est que tu n'a pas compris le sujet. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Comment fais-tu avec des variants et l'approche initiale si tu veux rajouter des int et l'opération d'addition add au langage jouet avec les booléens ?
Dans le cas de metaOCaml, le language est OCaml, donc tu as déjà tout ce qu'il te faut (modulo les limitations de MO).
Ma question portait sur comment faire en OCaml standard (donc sans MetaOCaml ;-) ce que permet de faire la méthode finale : c'est-à-dire étendre le langage par un processus d'héritage. L'exemple de mon premier message est un langage simple avec des booléens et des fonctions, si j'utilise un GADT je vais écrire :
Cette approche où on représente l'AST par un type de données est dite initiale, c'est du deep embedding. Maintenant si je veux rajouter des int et l'addition, je dois créer un nouveau GADT qui rajoute des cas et je ne pourrais pas réutiliser le code écrit pour celui-ci. C'est le problème de l'extension par héritage, ce qui se fait bien en POO. Là avec les modules il me suffit de faire :
C'est là le mécanisme « d'héritage » entre les modules, et je peux réutiliser facilement tout le code déjà écrit pour le modules de signature SymHO qui est un sous-type de cette signature étendue. En fait la méthode finale est une version étendue et plus poussé de l'encodage de Boehm-Berarducci présenté par Aluminium dans le journal EDSL et F-algèbre. Au lieu d'utiliser des enregistrements, comme dans le journal, on utilise des modules — et des foncteurs — qui sont des « enregistrements » qui permettent un plus haut niveau d'abstraction et que l'on peut étendre via la directive include. La méthode finale avec les modules est du shallow embedding. :-)
Si tu regardes ma passe d'optimisation pour réduire les additions et rentrer dans la pile comme dans la deuxième leçon de Jeremy, c'est un foncteur paramétrisé par une module de signature SYM_ADD :
Le code ci-dessus montre au passage comment on fait de l'héritage multiple entre module avec la définition de la signature SYM_ADD_COND.
pour être comparable en termes de performance, c'est d'utiliser ton "observateur" pour générer du code ocaml que tu vas compiler au run-time et ensuite charger dynamiquement
C'est ce qu'il fait en partie ;-) Si je reprends mon exemple avec Eopt :
Regarde son type : (int -> int -> int) Eopt.repr, il est isomorphe au type (int -> int -> int) code de MetaOCaml, et son code est bien optimisé sous la forme fun x y -> 3 + (y + (x + 11)) comme le montre la sortie du pretty printer. Et ma fonction observe me renvoie la fonction de type int -> int -> int sous sa forme optimisée comme le run de MetaOCaml. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
le principe de la recherche c'est souvent une discussion active sur des questions que personne ne comprend vraiment bien
C'est pour ça que c'est intéressant ! Il faut bien que l'on finisse par comprendre. :-)
je ne sais plus forcément ce qui est vraiment mieux qu'avec une approche initiale
Comment fais-tu avec des variants et l'approche initiale si tu veux rajouter des int et l'opération d'addition add au langage jouet avec les booléens ? Il faut redéfinir une nouvelle structure de données et réécrire le code (c'est une des raisons pour laquelle MetaOCaml est un fork, il étend le type Parsetree de l'AST du langage OCaml). Il y a bien les variants polymorphes mais comparé à l'approche initiale avec GADT il n'y a pas de vérification de typage : il faut écrire un type checker. Là dans mon langage jouet ça va, il n'y a qu'un seul type — les booléens — mais si on rajoute les int il faut vérifier statiquement que le premier paramètre de if_ est bien un booléen.
Avec l'approche finale on a de l'héritage multiple. Il suffit de définir différents sous-ensembles de langages, de construire le langage que l'on souhaite par héritage et on récupère tout le code de ses sous-langages. Dans mon journal en écriture j'ai trois langages : un avec des int, un autre avec des bool et un autre avec uniquement des fonctions (du pur lambda-calcul). Le langage jouet avec booléen et fonction est obtenu en combinant les deux derniers.
C'est juste un niveau d'abstraction au-dessus, comme avoir des fonctions en tant que valeur comme les autres dans les langages fonctionnels par rapport aux langages qui n'en ont pas. D'ailleurs j'ai commencé à lire le cours de Jeremy, et sa deuxième leçon m'a donné une idée. Sa leçon consiste à utiliser MetaOCaml pour optimiser le code d'une stack machine implémentée avec des fonctions plutôt qu'un GADT.
Avec l'approche final, on peut faire une chose similaire sans MetaOCaml. Je montrerai juste la sortie d'optimiseur que j'ai codé sur le langage complet qui hérite des trois dont j'ai parlé : entier, booléen et fonctions.
(* là ce sont les deux interprètes classiques *)moduleE=EvalAddCondHOmoduleS=ShowAddCondHO(* je les passe dans une chaîne d'optimisations *)moduleSopt=LinearizeAddHO(Static(SuppressZeroHO(S)))moduleS1opt=LinearizeAddHO(ReduceAddHO(Static(SuppressZeroHO(S))))moduleEopt=LinearizeAddHO(ReduceAddHO(Static(SuppressZeroHO(E))))(* le premier fait de l'application statique et linéarise l'addition * pour, par exemple, optimiser le calcul sur une stack machine ;-) *)letopenSoptinlet(+)=addinobserve@@lam@@funx->lam@@funy->lit1+lit2+x+lit3+lit4+y+lit5+lit6;;-:string="Lx. Ly. 1 + (2 + (y + (3 + (4 + (x + 11)))))"(* avec le second on peut simplifier le contenu de la pile comme dans la leçon de Jérémy *)letopenS1optinlet(+)=addinobserve@@lam@@funx->lam@@funy->lit1+lit2+y+lit3+lit4+x+lit5+lit6;;-:string="Lx. Ly. 3 + (y + (7 + (x + 11)))"(* Ainsi la fonction renvoyer par Eopt fait ce que le code écrit au-dessus dit *)letopenEoptinlet(+)=addinobserve@@lam@@funx->lam@@funy->lit1+lit2+y+lit3+lit4+x+lit5+lit6;;-:int->int->int=<fun>(* le code exécuté est fun x y -> 3 + (y + (7 + (x + 11))) *)letopenEoptinlet(+)=addin(observe@@lam@@funx->lam@@funy->lit1+lit2+x+lit3+lit4+y+lit5+lit6)1011;;-:int=42(* \o/ *)(* avec une application partielle *)letopenS1optinlet(+)=addinobserve@@app(lam@@funx->lam@@funy->lit1+lit2+y+lit3+lit4+x+lit5+lit6)(lit10);;-:string="Lx. 3 + (x + 28)"(* \o/ *)
Avec l'approche finale les optimiseurs sont assez simples à coder, on ne les fait que pour la partie du langage qui nous importe (addition, structure de contrôle, fonction…) et on les reprend telle quelle pour tous les langages qui en héritent. Là je montre la passe pour réduire les additions en rentrant dans la pile :
moduleReduceAddPass(F:SYM_ADD)=structmoduleX=structtype'afrom='aF.reprtype'aterm=|Dyn:'afrom->'aterm|Stv:(int*intfrom)->intterm|Add:(intterm*intterm)->inttermletfwdx=Dynxletrecbwd:typea.aterm->afrom=function|Dynx->x|Stv(_,x)->x|Add(x,y)->F.add(bwdx)(bwdy)endopenXmoduleIDelta=structletlitn=Stv(n,F.litn)(* le principe est là : dès que deux valeurs * statiques se suivent on calcule statiquement *)letadd:intterm->intterm->intterm=funxy->matchx,ywith|Stv(n,_),Stv(n',_)->lit(n+n')|Add(x,Stv(n,_)),Stv(n',_)->Add(x,lit@@n+n')|Stv(n,_),Add(Stv(n',_),y)->Add(lit(n+n'),y)|_,_->Add(x,y)endend
Dans le fond on écrit le code des fonctions comme d'habitude, il faut juste les passer dans la fonction lam et on peut définir de macros pour simplifier l'écriture :
J'attends ton journal avec curiosité (enfin bon je ne vais pas souvent sur LinuxFR où je ne me sens pas très bien, alors envoie-moi peut-être un mail quand tu le publieras).
Je vais essayer de le mettre au point dans la semaine. Je comprends que tu ne viennes pas souvent, l'ambiance est spéciale par moment. Si je ne te vois pas réagir au journal, je t'enverrai un mail.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
En fait, je vais arrêter là. Je me suis rendu compte, en réfléchissant plus, que je me suis fourvoyé. :-/
Dans leur article, pour gérer les évaluations partielles ils utilisent deux techniques : les types fantômes et MetaOCaml. Mon exemple avec les GADT remplace l'utilisation des types fantômes. Cela n'a rien d'étonnant, ils ont été introduits en partie pour cela : on les appelle aussi first-class phantom type. Par contre MetaOCaml et son type ('a,t) code joue le rôle de mon interprète ShowHO de pretty printing. Donc que je n'ai pas besoin de MetaOCaml dans mon code est normal : j'utilise un autre interprète. :-P
Pour ce qui est de faire une dépêche sur MetaOCaml, je ne le connais pas du tout, il faudrait que j'expérimente avec pour en savoir plus. Là la seule chose que je sache c'est le principe du dialecte : différer les calculs sous le contrôle du développeur (c'est proche des quote et unquote du LISP, il me semble).
Pour exposer plus en détail l'approche tagless, j'ai un journal en préparation mais il faut que je restructure. J'ai deux textes de 900 lignes : un sous forme de fichier .ml avec du code commenté et illustrant le principe tant des extensions de langage via héritage multiple que les optimisations, un autre plus dans la forme d'un journal avec moins de code et comparant la méthode « classique » avec variant pour l'AST et la méthode tagless.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
L'année dernière j'ai demandé à Oleg si ça l'intéresserait à terme, mais il a répondu qu'il restait encore selon lui des questions de conception en suspens et qu'il aimerait mieux les comprendre avant de pousser pour une intégration.
C'est ce que j'avais compris de ta présentation de BER MetaOCaml sur lambda-the-ultimate et des commentaires qui ont suivi. Son principe est sain : construire une tour dont on n'a pas assez étudié les fondements, cela mène à la tour de Pise et ensuite il faut coller des étais de tous le côtés pour que ça ne se casse pas la gueule. Cette dernière façon de procéder est une pratique architecturale douteuse et non recommandable. ;-)
Je ne me suis jamais penché vraiment sur MetaOCaml car bien que les primitives soient claires, je trouvais la syntaxe un peu lourde. Les liens de ton journal seront une occasion de regarder cela de plus près.
Pour la méthode tagless qu'il a mise au point conjointement avec Carette et Shan, elle donne une solution élégante au problème de l'extension : ajouter des cas aux variants et ajouter des traitements sur les données sans avoir à recompiler et avec la sécurité du typage statique. Wadler a développé les generics en Java pour cela, en C++ ils ont les templates mais dans les deux cas il faut utiliser le visitor pattern que je trouve étrange. De leur côté les langages fonctionnels ont la technique du fold, plus naturel, pour se substituer au visitor pattern mais pour réutiliser du code et ajouter des cas aux variants c'est compliqué. Là avec leur solution, on a de l'héritage multiple via le système « d'héritage » des modules et on n'a pas besoin de variants exotiques comme les variants polymorphes ou les GADT pour garantir le typage. Oleg l'avait signalé sur la discussion « GADT vs. Type Classes ».
Là où je vois une ouverture vers MetaOCaml en OCaml standard, c'est dans la combinaison de cette méthode avec les GADT pour l'évaluation partielle. Dans l'article dont j'ai donné le lien dans mon précédent message, ils utilisent MetaOCaml pour faire de l'évaluation partielle et jouer sur deux niveaux : statique et dynamique. Avec les GADT, on peut s'en passer ! :-)
Un exemple rapide. On prend un langage simple avec des booléens, la structure de contrôle if-then-else et des fonctions. Dans leur approche, le langage est défini par la signature suivante :
Ici chaque fonction mime les branches d'un variant avec GADT. Ainsi la signature exprime clairement la syntaxe et la sémantique du langage sans avoir besoin des GADT. Pour la structure if-then-else, on met chaque branche dans un thunk (unit -> 'x) car OCaml fait du call-by-value et cela permet de n'évaluer la branche que si l'on en a besoin. Ensuite plutôt que de faire un fold sur un variant avec GADT pour faire varier les interprétations, on implémente des modules qui satisfont cette interface.
Là je passe les détails pour deux interprétations classiques : eval pour évaluer les termes du calcul et show pour faire du pretty printing. Mais là où les GADT deviennent intéressants c'est pour faire des optimisations comme de l'évaluation partielle.
modulePE(F:SymHO)=struct(* on part d'une interprétation F du langage *)type'afrom='aF.repr(* on en construit une nouvelle qui évalue ce qui est statiquement connu *)type'arepr=|Dyn:'afrom->'arepr(* la valeur est connue dynamiquement *)|Stv:('a*'afrom)->'arepr(* elle est connue statiquement *)|Fun:('arepr->'brepr)->('a->'b)repr(* c'est une fonction *)(* la sortie de l'interprète partiel est la même que celui de départ *)type'aobs='aF.obs(* deux morphismes entre les domaines de représentations internes *)letfwdx=Dynxletrecbwd:typea.arepr->afrom=function|Dynx->x|Stv(_,x)->x|Funf->F.lam@@funx->bwd@@f(fwdx)(* un booléen est connu statiquement *)letbool_b=Stv(b,F.bool_b)(* si la condition est connue statiquement on évalue la branche adéquate * sinon on se rabat sur l'interprète F *)letif_bteee=matchbwith|Stv(b,_)->ifbthente()elseee()|_->fwd@@F.if_(bwdb)(fun()->bwd@@te())(fun()->bwd@@ee())(* pour les fonctions on les applique *)letlamf=Funfletappfx=matchfwith|Funf->fx|_->fwd@@F.app(bwdf)(bwdx)letobservex=F.observe(bwdx)end
Dans leur article de présentation, ils utilisaient un enregistrement avec un type 'a option pour la partie statique et une type ('c, t) code de MetaOCaml pour la partie dynamique. Avec les GADT, pas besoin de MetaOCaml. L'idée est reprise du tutoriel Modular, composable, typed optimizations in the tagless-final style sur le site de Oleg.
Maintenant pour les liens avec les macros et le recours à l'évaluation partielle :
Soit on se sert de OCaml pour rajouter la primitive not_ au langage sous forme de « macro », où on l'implémente dans le langage vu qu'il dispose des fonctions. À l'usage :
(* le module ShowHO fait du pretty printing *)moduleM=Macro(ShowHO)moduleC=Code(ShowHO)moduleCPE=(PE(ShowHO))(* la fonction not_ de M est une nouvelle primitive *)M.not_;;-:boolShowHO.repr->boolShowHO.repr=<fun>(* c'est bien une « macro » avec typage statique :-) *)M.observe@@M.not_M.true_;;-:string="if true then false else true"(* la version de C est une fonction de notre langage définie à partir de ses primitives *)C.not_;;-:(bool->bool)ShowHO.repr=<fun>(* on peut l'afficher et l'appliquer *)C.observe@@C.not_;;-:string="Lx. if x then false else true"C.observe@@C.appC.not_C.true_;;-:string="(Lx. if x then false else true) (true)"(* la même mais avec évaluation partielle *)CPE.not_;;-:(bool->bool)PE(ShowHO).repr=PE(ShowHO).Fun<fun>CPE.observe@@CPE.not_;;-:string="Lx. if x then false else true"CPE.observe@@CPE.appCPE.not_CPE.true_;;-:string="false"(* \o/ *)
En espérant n'avoir pas trop dévié du thème original du journal.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Tout d'abord merci pour ce journal et le lien vers la présentation de Jeremy Yallop. Ça va me faire de la lecture. :-)
J'ai une question à te poser. Il me semble que le développeur principal de MetaOCaml, et qui a repris le projet, est Oleg Kiselyov. J'ai cru lire sur son site qu'il avait grandement réduit la quantité de code qui le sépare du compilateur standard, et qu'il espère un jour pouvoir en faire une simple bibliothèque plutôt qu'un dialecte.
J'ai justement un journal en cours d'écriture pour présenter la méthode tagless final pour plonger un langage en OCaml et faire de l'évaluation partielle sans passer par des variants pour représenter l'AST mais en utilisant des modules et des foncteurs. Bon, il va falloir que j'élague un peu parce que là j'ai un pavé. :-P
Depuis que je joue avec cette méthode, j'en suis venu à voir OCaml comme un langage de macros typés pour le langage objet ce qui permet de faire de la méta-programmation intéressante sur celui-ci ainsi que des passes d'optimisations simples à réaliser, indépendantes, modulaires et facilement composables. Au final je me demande si cette méthode n'ouvre pas la voie vers la possibilité de ramener MetaOCaml à une simple bibliothèque ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Mais contre l'État, j'en doute, ni même contre les grandes entreprises du net comme les GAFAM qui eux peuvent avoir des moyens similaires aux États
Il y a bien un moyen que les GAFAM ne possèdent pas et qui reste la prérogative des États : celui de définir le droit (pouvoir législatif), de rendre la justice selon le droit (pouvoir judiciaire) et d'exécuter les sentences juridiques via son bras armé (pouvoir exécutif). C'est là le domaine (et le seul) qui doit relever du monopole de l'État et sur lequel se fonde sa souveraineté. Raison pour laquelle, la réponse du chiffrement face aux États n'est qu'un pis aller — révélateur d'un recul ou d'une absence de l'état de droit — et la seule réponse qui vaille est politique c'est-à-dire juridique et non technique.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
chouchou : j'trouve pas d'réseau wifi dans cette maison ?! C'est nul, y'a pas l'internet !!!! :-( moi : mais si ! faut juste que tu t'colles un fil à la patte : l'ethernet c'est le top pour l'internet ! \o/ chouchou : j'm'en fous d'ton fil, mets moi le wifi !!!!! :@
Voilà une situation qui me semble bien plus proche de la réalité pour la grande majorité de la population. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
les tournures utilisées sont différentes, typiquement faire avorter (en général un projet). […]
Reste que la langue principale de l'informatique est l'anglais, langue dans laquelle le verbe abort est le mot exact pour décrire l'interruption, volontaire ou non, mais souvent brutale, d'un processus, d'une applications, etc. en informatique. […]
En conséquence, j'en déduis que sans trop de difficultés que la proximité de la formulation anglaise est probablement plus qu'un vague cousinage avec l'usage qui est fait ici de avorter et avortement.
Il est vrai que si le verbe anglais to abort et le verbe français avorter sont issus d'une racine commune, l'évolution de l'usage anglais en a fait un verbe qui peut être intransitif ou transitif. Là où en français, lorsque le sujet de la proposition est l'agent qui pratique l'avortement, on préférera utiliser des formulations comme « faire avorter qqch. », « arrêter qqch. » ou « interrompre qqch. ». Comme le montre ces quelques exemples issus de linguee :
If something is wrong, abort the take off.
Si quelque chose ne va pas, arrêtez le décollage.
Foolish haste or laziness could abort a great hope-with consequences that we do not imagine.
Une hâte imbécile ou de l'indolence pourraient faire avorter un grand espoir, avec des conséquences que nous ne pouvons pas imaginer.
[…] have preprogrammed safety checks that will signal problems by means of error messages and will abort the testing procedure.
[…] de sécurité préprogrammés signaleront les problèmes au moyen de messages d'erreur et provoqueront l'interruption du test.
Malgré cela, le projet ourdi en secret par les grammar nazi afin de conquérir le monde n'a pas encore avorté. :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Certes mais, comme il t'a répondu, il l'utilise bien comme une verbe intransitif dans son journal. Du moins, on peut discuter ce dernier point. En dehors de son usage en titre de section, il écrit :
d’autres ont déjà fait le choix d’avorter en cas d’erreur
On peut soit considérer que les auteurs ont décidé d'avorter le programme (qui serait ici sous-entendu en fonction objet) ce qui en ferait bien un usage incorrect en tant que verbe transitif; soit, toujours dans une acception figurée du verbe, considérer que le programme représente le processus par lequel les auteurs veulent engendrer un résultat et ils décident d'avorter en cas d'erreur produisant ainsi quelque chose étant mort; ou encore on pourrait écrire, par métonymie, en substituant l'agent par l'instrument : le programme avorte en cas d'erreur.
Quoi qu'il en soit, je ne vois toujours pas en quoi un tel usage relève d'un affreux anglicisme (sic). ;-)
Aucun drosophile n'a été abusé sexuellement au cours de cet échange linguistique.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
C'est surtout un « affreux » latinisme au sens figuré ! Il y a aussi du latin dans la langue anglaise, et ce sens figuré se pratiquait déjà en France au XIIe siècle. ;-)
Article intéressant à plus d'un titre. Voici mon résumé de ce que j'en ai compris :
TP-link a écopé d'une amende de 200.00 $ parce qu'ils vendaient des routeurs permettant d'être utilisés à une puissance supérieure à la limite autorisée par les règles de la FCC. Mais cette infraction ne relevait pas de la nouvelle réglementation sur le 5 GHz, dont parle le journal, mais des règles sur la bande à 2.4 GHz : en changeant une option dans la configuration du routeur (le code du pays) celui-ci pouvait émettre à une puissance trop forte. Pour corriger le tir, TP-link a fait une mise à jour de son firmware qui au passage empêchait l'installation de tout autre firmware issu de tierce partie : telle fut la solution choisie pour satisfaire au passage à la nouvelle réglementation sur le 5 GHz. Ce en quoi le règlement du FCC ne stipule pas que l'on ne puisse installer d'autre firmware que ceux fournis par TP-link, mais seulement que ceux-ci ne doivent pas permettre d'utiliser le matériel en dehors des limites légales. Et finalement, pour ne pas payer une amende plus importante, la FCC et TP-link sont tombés sur un accord obligeant ce dernier a collaboré avec les fabricants de chipset Wi-Fi et la communauté open-source pour permettre aux utilisateurs d'installer le firmware de leur choix. On apprend de plus, en fin d'article, que Linksys, sans être contraint de le faire, a déjà travaillé avec Marvell et OpenWRT pour être certain que ses routeurs satisferont la nouvelle législation sans bloquer les firmwares libres.
Me vient donc deux questions :
en quoi cette nouvelle réglementation porte-t-elle réellement atteinte à la liberté des utilisateurs ?
Les coûts pour permettre l'installation de firmware libre tout en respectant la législation sont-ils bien de l'ordre du million de dollars, étant que donné que TP-link a accepté cette décision pour réduire le montant de son amende ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Et en Ocaml, il y a soit le type 'a option = None | Some of 'a soit le type ('a, 'b) result = Ok of 'a | Error of 'b.
Ce qui correspond à la classe std::expected<T,E> proposée pour le C++ :
Class template expected<T,E> proposed here is a type that may contain a value of type T or a value of type E in its storage space. T represents the expected value, E represents the reason explaining why it doesn’t contains a value of type T. The interface and the rational are based on std::optionalN3793. We can consider expected<T,E> as a generalization of optional<T>.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Dans la série liens intéressants et instructifs : Demystifying Type Classes sur le site de Oleg Kiselyov. D'une manière générale, son site est une véritable mine d'or ! :-)
Sur cette page, il y explique de manière didactique et complète le principe des type classes en étudiant trois implémentations possibles du système dans un langage : par passage de dictionnaire, par monomorphisation ou par analyse intentionnelle de type. La première étant la plus répandue et les deux secondes étant issues de l'article pionnier sur le sujet : Parametric overloading in polymorphic programming languages de Stephan Kaes en 1988 (un lien vers cet article est donné en bas de page).
On y trouve aussi une comparaison avec des techniques du C++, comme il le souligne en conclusion :
We have presented the intensional type analysis, the third way of compiling type classes. Whereas monomorphization is akin to C++ template instantiation and dictionary passing is similar to vtable, the intensional type analysis reminds one of resolving overloading by a large switch statement.
Traduction rapide :
Nous avons présenté l'analyse intentionnelle de type, la troisième façon de compiler les classes de type. Tandis que la monomorphisation est similaire à l'instantiation de template C++ et le passage de dictionnaire est similaire aux vtable, l'analyse intentionnelle de type fait penser à la résolution de surcharge comme à un grand switch.
La dernière technique m'a donné une idée un peu différente de la sienne, mais largement inspirée de son illustration en OCaml, en utilisant des types sommes ouverts et des GADT. Exemple avec la fonction show :
(* on définit un type somme ouvert dans lequel on peut rajouter des cas après coup *)type'ashowable=..(* on définit la fonction show pour ce type encore vide *)letshow:typea.ashowable->a->string=fun_x->failwith"failed overloading resolution";;valshow:'ashowable->'a->string=<fun>(* on rajoute des cas dans le type avec leur instance pour show *)type'ashowable+=Int:intshowable;;type'ashowable+=Int:intshowableletshow:typea.ashowable->a->string=function|Int->string_of_int|ty->showty;;valshow:'ashowable->'a->string=<fun>type'ashowable+=Bool:boolshowable;;type'ashowable+=Bool:boolshowableletshow:typea.ashowable->a->string=function|Bool->string_of_bool|ty->showty;;valshow:'ashowable->'a->string=<fun>type'ashowable+=List:'ashowable->'alistshowable;;type'ashowable+=List:'ashowable->'alistshowableletshow:typea.ashowable->a->string=function|Listty->funl->letrecloopfirst=function|[]->"]"|h::t->(iffirstthen""else", ")^showtyh^loopfalsetin"["^looptruexs|ty->showty;;valshow:'ashowable->'a->string=<fun>(* quelques exemples *)showInt1;;-:string="1"showBooltrue;;-:string="true"show(ListInt)[1;2;3];;-:string="[1, 2, 3]"(* limitations du système *)(* on définit une fonction print sur les showable *)letprinttyx=print_endline(showtyx);;valprint:'ashowable->'a->unit=<fun>(* cela marche bien... pour l'instant *)printInt1;;1-:unit=()print(ListInt)[1;2;3];;[1,2,3]-:unit=()(* maintenant on rajoute les float mais sans implémentation pour show *)type'ashowable+=Float:floatshowable;;type'ashowable+=Float:floatshowable(* la c'est normal, dans le grand switch le cas Float n'est pas encore géré *)print(Float)1.2;;Exception:Failure"failed overloading resolution".(* on rajoute le cas au switch *)letshow:typea.ashowable->a->string=function|Float->string_of_float|t->showt;;valshow:'ashowable->'a->string=<fun>showFloat1.2;;-:string="1.2"(* et là : pouf, ça marche pas pour print !!! *)print(Float)1.2;;Exception:Failure"failed overloading resolution".(* la raison en est que en OCaml lorsque l'on définit un terme, * sa définition ne doit dépendre que des termes déjà défini qui le précèdent * et donc rajouter un cas à show après avoir défini print ne change rien à son code : * il faut la redéfinir à chaque fois que l'on rajoute une instance :-/ *)letprinttyx=print_endline(showtyx);;valprint:'ashowable->'a->unit=<fun>printFloat1.2;;1.2-:unit=()(* au final cette implémentation n'est pas compatible avec la programmation * modulaire et les avantages des compilations séparées. *)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
La prise en compte de l'harmonie est intéressante, mais je crois qu'elle sert un objectif un peu différent.
C'est vrai mais cela peut être une piste intéressante à explorer pour les futures évolutions de la bibliothèque.
Lorsque l'on conçoit une set list pour un concert, ou même lorsque l'on réfléchit à l'ordre des chansons sur un album c'est une information que l'on prend en compte. Le principe ayant était poussé à l'extrême sur l'album concept Le fil de Camille qui tournait autour de la note si restant en bourdon.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
La publicité c'est du temps et des moyens = de l'argent.
Non, pas nécessairement.
Si tu contribue à un logiciel, c'est du temps = de l'argent.
Non, pas nécessairement.
Comme tu ne sembles toujours pas comprendre ce qu'est l'argent, je vais extraire la partie la plus importante sur le sujet du lien que j'ai donné plus haut (le texte est long, mais ça vaut le coup de le lire si tu veux bien comprendre de quoi tu parles lorsque tu parles d'argent).
Vous avez un écu. Que signifie-t-il en vos mains ? Il y est comme le témoin et la preuve que vous avez, à une époque quelconque, exécuté un travail, dont, au lieu de profiter, vous avez fait jouir la société, en la personne de votre client. Cet écu témoigne que vous avez rendu un service à la société, et, de plus, il en constate la valeur. Il témoigne, en outre, que vous n’avez pas encore retiré de la société un service réel équivalent, comme c’était votre droit. Pour vous mettre à même de l’exercer, quand et comme il vous plaira, la société, par les mains de votre client, vous a donné une reconnaissance, un titre, un bon de la République, un jeton, un écu enfin, qui ne diffère des titres fiduciaires qu’en ce qu’il porte sa valeur en lui-même, et si vous savez lire, avec les yeux de l’esprit, les inscriptions dont il est chargé, vous déchiffrerez distinctement ces mots : « Rendez au porteur un service équivalent à celui qu’il a rendu à la société, valeur reçue constatée, prouvée et mesurée par celle qui est en moi-même. »
Maintenant, vous me cédez votre écu. Ou c’est à titre gratuit, ou c’est à titre onéreux. Si vous me le donnez comme prix d’un service, voici ce qui en résulte : votre compte de satisfactions réelles avec la société se trouve réglé, balancé et fermé. Vous lui aviez rendu un service contre un écu, vous lui restituez maintenant l’écu contre un service ; partant quitte quant à vous. Pour moi je suis justement dans la position où vous étiez tout à l’heure. C’est moi qui maintenant suis en avance envers la société du service que je viens de lui rendre en votre personne. C’est moi qui deviens son créancier de la valeur du travail que je vous ai livré, et que je pouvais me consacrer à moi-même. C’est donc entre mes mains que doit passer le titre de cette créance, le témoin et la preuve de la dette sociale. Vous ne pouvez pas dire que je suis plus riche, car si j’ai à recevoir, c’est parce que j’ai donné. Vous ne pouvez pas dire surtout que la société est plus riche d’un écu, parce qu’un de ses membres a un écu de plus, puisqu’un autre l’a de moins.
Que si vous me cédez cet écu gratuitement, en ce cas, il est certain que j’en serai d’autant plus riche, mais vous en serez d’autant plus pauvre, et la fortune sociale, prise en masse, ne sera pas changée ; car cette fortune, je l’ai déjà dit, consiste en services réels, en satisfactions effectives, en choses utiles. Vous étiez créancier de la société, vous m’avez substitué à vos droits, et il importe peu à la société, qui est redevable d’un service, de le rendre à vous ou à moi. Elle s’acquitte en le rendant au porteur du titre.
L'argent n'apparaît que lors des échanges à titre onéreux et non à titre gracieux : autrement dit lorsqu'une personne dit à une autre « j'accepte de faire cela pour toi à la seule condition que tu fasses ceci pour moi ». On peut même dire que ce sont ces types de contrats qui créent l'argent : l'argent ce n'est que de la reconnaissance de dette. Il ne fait que représenter un troc suspendu, différé ou non finalisé.
Il y a une grande différence entre ces trois propositions :
tous les échanges doivent être onéreux ;
tous les échanges doivent être gracieux ;
les échanges peuvent être onéreux ou gracieux.
Ce que l'on te dit c'est que l'on ne peut exiger d'autrui qu'il échange avec nous à titre gracieux, c'est-à-dire sans contrepartie.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
L'important ce n'est pas les deux numéros, mais qu'ils correspondaient à deux lignes distinctes. Chez Orange, j'ai toujours eu une ligne branchée directement sur la prise et l'autre était branchée sur la box. Si tu appelais le numéro en 09, les téléphones connectés directement à la prise ne sonnaient pas. Dans ton cas, les numéros en 01 et 09 correspondent-ils à deux lignes distinctes ou sont-ce deux alias pour la même ligne ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Merci, mais ça ne parait pas techniquement possible ?
Cela doit bien être possible, étant donné que c'est réel : cela fonctionne comme cela chez moi. ;-) Pour les détails techniques, je n'ai aucune idée de la manière dont cela fonctionne.
Avant j'avais deux lignes : une avec le préfixe en 01-05 (selon la région) et une autre en 09. Maintenant je n'ai plus que la première avec la même offre que celle que j'avais avec la seconde, ce qui est tout de même plus simple pour l'usager : il ne fallait pas se tromper de ligne lorsque l'on appelait.
Edit : je parle de l'offre ADSL.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
To understand the concept, you should think of “free” as in “free speech,” not as in “free beer”. We sometimes call it “libre software,” borrowing the French or Spanish word for “free” as in freedom, to show we do not mean the software is gratis.
Traduction : « Pour comprendre le concept, vous devriez penser à « free » comme dans « liberté d'expression », non comme dans « bière gratuite ». Nous l'appelons parfois « logiciel libre », empruntant le mot français ou espagnol pour « free » comme dans « liberté », pour monter que nous ne signifions pas par là que le logiciel est gratuit. »
Le texte original est essentiellement destiné aux anglophones, car en anglais le mot « free » peut signifier aussi bien « libre » que « gratuit », ambiguïté qui n'existe pourtant pas dans la langue française.
Pour rebondir sur la remarque « l'argent n'est que du travail figé » de Marotte, je rajouterai que le principe de base de l'économie marchande c'est le troc : je te donne ça si tu me donnes ça en échange ou je fais cela pour toi si tu fais cela pour moi, i.e. échange de biens et services. L'argent c'est juste un troc non finalisé, et permet de recevoir en échange du service rendu un service de la part d'une autre personne que celle à qui l'on a rendu service : c'est un bien qui améliore grandement les échanges librement consentis de services, là où sans cela le système de ton village africain ne pourrait nullement passer à l'échelle. ;)
[^] # Re: Usage autre des GADTs ?
Posté par kantien . En réponse au journal Tagless-final ou l'art de l'interprétation modulaire.. Évalué à 1.
Effectivement, petite faute d'accord. Si un modérateur pouvait corriger. J'en ai repéré une autre avec un seul « t » au lieu de deux à littéraux : « La première optimisation que l'on va voir est celle qui consiste à supprimer tous les litéraux nuls ».
Sur son site on trouve également une lecture où il expose encore plus en détail toutes les possibilités de l'approche et en Haskell. Les fichiers de code sont accessibles ici.
Les possibilités des GADT mériteraient plus d'un journal pour être présentées. La leçon de Jeremy Yallop sur le sujet illustre des cas d'usage qui vont bien au-delà de l'écriture de compilateur.
Je dirais un sur-ensemble : tout ce que font les typeclasses peuvent être fait avec les modules, mais la réciproque ne marche pas — il me semble. Pour les différents niveaux d'abstraction accessibles en OCaml, il y a ces deux leçons de Leo White : abstraction et parametricty.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: chaud
Posté par kantien . En réponse au journal Tagless-final ou l'art de l'interprétation modulaire.. Évalué à 1.
Je ne suis pas sur de comprendre. Tu voudrais par exemple un dépôt avec :
C'est cela ? Afin de pouvoir mieux comparer les codes et les méthodes ?
C'est pas faux. Sans avoir besoin d'avoir bien compris le principe de la méthode — ils sont avant tout là pour l'illustrer sur un exemple — il vaut mieux en avoir une idée au moins approximative dans un premier temps.
Pour ce qui est de l'opérateur
@@c'est une question de goût personnel pour éviter d'avoir trop de parenthèses et séparer visuellement les fonctions de leurs arguments. Cela permet d'écrire :Pour ce qui est des modules par rapport aux objets, ils ont un point commun : ce sont des enregistrements extensibles; et on aurait pu faire la même chose avec des objets. C'est ce qu'à fait Philipp Wadler en 1998 quand il a proposé sa solution au problème de l'extension sur la liste de diffusion Java Generics. Mais il faut utiliser le vistor pattern, et je préfère l'approche du fold qui dans cette solution est jouée par le rôle des foncteurs. Un foncteur est au fond une fonction des modules vers les modules, c'est plus « fonctionnel » dans le principe. On peut écrire une signature de foncteur ainsi :
Si tu te souviens des échanges sur le journal d'Aluminium qui présentait l'encodage de Böhm-Berarducci, celui de ce journal en est une généralisation. Voici le lien vers mon commentaire qui comparait cet encodage avec l'approche classique.
L'encodage de Böhm-Berarducci, qui utilise des enregistrements, marche bien tant que le langage que l'on plonge a un seul type de données, comme le premier exemple qui n'a que des int. Mais il devient lourd, voir impossible à utiliser quand ce langage a plus d'un type de données :
int,bool, fonctions… Alors au lieu d'utiliser des enregistrements, on utilise des modules (ou des objets) qui sont une généralisation et une abstraction supplémentaire au-dessus des enregistrements.Pour ce qui est du rapport entre le
foldet le vistitor pattern de la POO, Perthmâd l'avait signalé dans la discussion et j'ai donné des liens en réponse à son commentaire.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: chaud
Posté par kantien . En réponse au journal Tagless-final ou l'art de l'interprétation modulaire.. Évalué à 1.
Désolé. :-P
Pourquoi pas. Il faudrait par contre que j'apprenne à me servir
gitet github. Tu connais un tutoriel pour une prise en main rapide du système ?Pour ce qui est du code que tu voudrais voir. Pourrais-tu être plus précis sur ce que tu attends ?
Il y a un tutoriel avec plusieurs fichiers de code sur le langage des circuits logiques. Le code est complet et commenté, c'est cela que tu veux ? Là, Oleg utilise en plus la bibliothèque
higherde Jeremy Yallop et Leo White. Cela lui permet de faire du higher-kinded polymorphism pour « dissimuler » le paramètre'adu type'a obs, d'utiliser ainsi des modules de première classe et de manipuler les foncteurs comme des fonctions normales.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Merci pour l'effort.
Posté par kantien . En réponse au journal Tagless-final ou l'art de l'interprétation modulaire.. Évalué à 3.
De rien. Cela m"a pris aussi du temps pour bien comprendre les tenants et aboutissants de la méthode. Écrire ce journal m'a permis de mieux l'assimiler, et il a connu plusieurs versions en fonction de l'évolution de ma compréhension.
Si tu as des questions sur des points précis de code ou sur les principes méthodologiques, n'hésite pas. J'essaierai de clarifier la chose du mieux que je peux.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
Posté par kantien . En réponse au journal Découvrir MetaOCaml dans son navigateur. Évalué à 0.
Exact ! J'ai bien aussi tenté avec le
unbox-closurede flamba pour voir s'il avait assez d'infos pour s'en sortir mais ça n'a rien donné.Quoi qu'il en soit ce n'est pas l'essentiel, ce qui m'intrigue c'est la ressemblance dans certains codages sur le plan syntaxique.
Par exemple dans leur article, pour le code de leur compilateur (le module qui interprète la signature en ayant recours à MetaOCaml) pour
lametappon a :ce qui est au fond les fonctions
back : ('a code -> 'b code) -> ('a -> 'b) codeetforth : ('a -> 'b) code -> 'a code -> 'b codede la première leçon de Jeremy.De l'autre côté, pour traiter le cas statique dans la méthode tagless final (ce qui est au fond une automatisation du binding-time analysis de la lecon 2) il m'a fallu utiliser les types suivants :
Avant d'arriver à ce choix, j'avais fait d'autres essais pour le cas des fonctions (dont un qui m'obligeait à utiliser l'option
rectypes) mais rien ne fonctionnait. Il y a aussi le code correspondant :ce qui montre une similitude d'usage entre
quoteetescaped'un côté, puisbwdetfwdde l'autre.Ensuite, dans le cadre de la correspondance de Curry-Howard, il semblerait que pour typer une fonction similaire au
quotedu LISP il faille recourir à l'axiome du choix ou une de ses variantes : Dependent choice, quote and the clcok. Je dois reconnaître que je n'ai pas tout saisi à l'article et aux techniques utilisées, mais je fais confiance à son auteur.C'est aussi un sport en mathématique de chercher à prouver un énoncé avec le moins d'axiomes possibles et l'axiome du choix est un cas à part : c'est globalement le seul où on pourra trouver des énoncés qui précise explicitement que l'on en fait usage dans la preuve. Dans un dépêche récente présentant un projet d'ouvrage sous licence libre pouvant servir de référence aux candidats à l'agrégation, j'avais fait un commentaire répondant à une demande de preuve sans recourir à cet axiome. La demande était un peu étrange, cela portait sur une question de théorie de la mesure et habituellement quand on demande à un logicien ce qu'il entend par analyse, il répond tout de go : l'arithmétique du second ordre avec axiome du choix dénombrable. C'est la base qui permet de formaliser le calcul intégrale, la théorie de la mesure, l'analyse réelle et complexe… en gros toutes les mathématiques dont ont besoin les physiciens et ingénieurs.
De son côté Gödel avait montré que l'on pouvait l'ajouter aux autres axiomes de la théorie des ensembles sans contradiction en construisant inductivement un univers du discours qui le satisfaisait. Il a construit un univers stratifié où à chaque rang on ne peut parler que des objets de rangs inférieurs ou du rang actuel mais pas des rangs supérieurs encore à venir. L'analogie avec l'approche de MetaOCaml est ses strates ou stage suscite chez moi bien des interrogations.
Pour ce qui est de la possibilité d'utiliser les GADT et la technique du lift générique pour obtenir cette structure stratifiée, je reste dans l'interrogative. Bonne idée à explorer ? fausse piste ? je n'en sais rien. Faut-il adapter le niveau meta du compilateur comme à l'heure actuelle, ou sera-t-il possible de le ramener à une bibliothèque ? le futur le dira. Mais d'après Oleg :
Wait and see, comme on dit.
Pour ce qui est de ta dernière remarque :
je le reconnais. Mais il y a un certain passif avec benja, cela a du influencé ma réaction. Il m'a enquiquiné sur des détails sans importance (que je n'ai toujours pas compris) en commentaire à ma dépêche de présenttaion du MOOC OCaml. Son ton de l'époque n'était pas des plus plaisant (dans le même genre que celui d'Aluminium dans ton journal de présentation de Malfunction) et il passait complètement à côté du sujet et de l'essentiel de mon propos.
Je donnais un exemple de code du genre :
afin de montrer l'analogie entre l'analyse de type et l'analyse grammaticale, en me focalisant sur l'analyse du groupe adverbiale « 5 fois ». Exemple qui m'avait été inspiré par des échanges au cours d'un dépêche sur le standard C++17 et un conférence de Gérard Huet. Conférence intitulée Fondements de l'informatique, à la croisée des mathématiques, de la logique et de la linguistique dont je cite ici in extenso un passage :
Selon benja, dans mon exemple, mon intention était de « singer les normes du français » (sic). Dois-je lui préciser que Gérard Huet a eu pour thésard Thierry Coquand (à l'origine du langage Coq) et Xavier Leroy (à l'origine du langage OCaml) ? Cherche-t-il lui aussi à singer la grammaire française en comparant le typage des fonctions dans le lambda-calcul avec le fonctionnement des verbes transitifs et intransitifs ? Ou encore avec l'analyse dimensionnelle en physique ? Et de voir que le point commun formel entre tout cela est la forme des jugements hypothétiques et la règle du modus ponens. Dois-je aussi signaler, en passant, que cette forme des jugements hypothétiques et de son principe du modus ponens est le type que donna Kant au principe de causalité dans la Critique de la Raison Pure dans ce qu'il appela logique transcendantale ?
Pour sa seconde remarque sur son insistance à désapprouver le fait que j'appelle
foldla fonction générique pour traverser une structure en remplaçant ses constructeurs par des applications de fonctions, je n'ai toujours pas compris.L'attitude qu'il a eu à l'époque, non dans le faits de faire des remarques ou des critiques, mais dans le ton employé est justement ce qui à tendance à m'énerver sur ce site : c'est trop fréquent, pour tout et n'importe quoi. J'en ai ma claque ! Et là j'ai eu le sensation à demi-mot qu'il prenait le même chemin : j'ai dégainé direct. Oui je sais ce que fait MetaOCaml : pas besoin de chercher à me l'expliquer. Mon intention n'était pas tant d'affirmer que d'interroger. Jusqu'à quel point l'approche de MetaOCaml et de la méthode tagless final se ressemble-t-elle ? Cette dernière, qui a également été mise au point par Oleg Kiselyov auteur de BER MetaOcaml, est-elle un piste envisageable pour atteindre un objectif qu'il semble avoir lui-même ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
Posté par kantien . En réponse au journal Découvrir MetaOCaml dans son navigateur. Évalué à 2.
Après, je ne suis pas développeur ni informaticien, mais mathématicien et logicien. Ce que j'aime c'est retrouver mes « petits », et là cela me parle. Pour l'intérêt pratique, ce n'est pas mon domaine.
Mais au delà du problème de l'extensibilité (c'est un des points), c'est la structure modulaire et composable des optimisations que je trouve élégante. Et comme via le lift générique on a
bwf (fwd x) = xquand on ne touche pas à un terme dans une passe, on a une phénomène qui ressemble au cross-stage persistence de MetaOCaml. Ça titille ma curiosité théorique ! :-PSapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
Posté par kantien . En réponse au journal Découvrir MetaOCaml dans son navigateur. Évalué à 2.
Non rien à voir, là où les GADT sont absolument nécessaire c'est pour avoir un lift générique :
Dyn : 'a from -> ' a term. Ce qui permet d'avoir une approche semblable à le réduction par évaluation (via les fonctionsfwdetbwdqui assurent quebwd (fwd x) = x) et de rester coller à la sémantique dénotationnelle. C'est ce qui permet de réutiliser une passe dans les langages qui étendent celui pour lequel elle est faite.Dans mes textes, j'ai un joli dessin en ASCII art qui pourra plaire aux catégoriciens :
Et de fait j'en ai un : la fonction
observe. ;-)Il y a un ancêtre commun à tous les Eval :
Dans leur article, Kiselyov et al. appelle cet interprète metacirculaire, car on replonge le langage dans OCaml en interprétant un terme… par lui-même. ;-)
Si tu veux voir les différents stages à la façon de MetaOCaml voilà le type exact de la représentation interne :
Chaque passe d'optimisation crée un « stage » lié à la succession d'application de foncteur. Donc au lieu de voir toute la chaîne comme un graphe plan, tu peux le voir comme une succession de cube en profondeur :
Merci, déjà lu.
C'est là qu'est toute mon interrogation. Ma fonction retournée par mon optimiseur est bien
fun x y -> 3 + (x + (7 + (y + 11))). Bon le plus simple serait que je compile un exemple en natif et que je ragarde le dump cmm sur un cas genre :pour voir si le code de
fest bien celui que je pense. Ma question reste : que ne peut-on pas faire avec l'approche tagless final qui nécessite le recours à MetaOCaml ? Mon interrogation est : ne peut on pas voir le processus comme « avec unfwdje monte d'un étage et avec unbwdje reviens dans l'étage du dessous, jusqu'à revenir au niveau 0'a = 'a» ?Il y a un côté inception dans le processus, comme avec MetaOCaml, le tout étant de ne pas rester coincer dans les limbes. :-P
Mon instinct est que tu n'a pas compris le sujet. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
Posté par kantien . En réponse au journal Découvrir MetaOCaml dans son navigateur. Évalué à 2.
Ma question portait sur comment faire en OCaml standard (donc sans MetaOCaml ;-) ce que permet de faire la méthode finale : c'est-à-dire étendre le langage par un processus d'héritage. L'exemple de mon premier message est un langage simple avec des booléens et des fonctions, si j'utilise un GADT je vais écrire :
Cette approche où on représente l'AST par un type de données est dite initiale, c'est du deep embedding. Maintenant si je veux rajouter des
intet l'addition, je dois créer un nouveau GADT qui rajoute des cas et je ne pourrais pas réutiliser le code écrit pour celui-ci. C'est le problème de l'extension par héritage, ce qui se fait bien en POO. Là avec les modules il me suffit de faire :C'est là le mécanisme « d'héritage » entre les modules, et je peux réutiliser facilement tout le code déjà écrit pour le modules de signature
SymHOqui est un sous-type de cette signature étendue. En fait la méthode finale est une version étendue et plus poussé de l'encodage de Boehm-Berarducci présenté par Aluminium dans le journal EDSL et F-algèbre. Au lieu d'utiliser des enregistrements, comme dans le journal, on utilise des modules — et des foncteurs — qui sont des « enregistrements » qui permettent un plus haut niveau d'abstraction et que l'on peut étendre via la directiveinclude. La méthode finale avec les modules est du shallow embedding. :-)Si tu regardes ma passe d'optimisation pour réduire les additions et rentrer dans la pile comme dans la deuxième leçon de Jeremy, c'est un foncteur paramétrisé par une module de signature
SYM_ADD:mais je l'utilise sur un module de signature
SYM_ADD_COND_HOqui étend celle-ci :Le code ci-dessus montre au passage comment on fait de l'héritage multiple entre module avec la définition de la signature
SYM_ADD_COND.C'est ce qu'il fait en partie ;-) Si je reprends mon exemple avec
Eopt:Regarde son type :
(int -> int -> int) Eopt.repr, il est isomorphe au type(int -> int -> int) codede MetaOCaml, et son code est bien optimisé sous la formefun x y -> 3 + (y + (x + 11))comme le montre la sortie du pretty printer. Et ma fonctionobserveme renvoie la fonction de typeint -> int -> intsous sa forme optimisée comme lerunde MetaOCaml. ;-)Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
Posté par kantien . En réponse au journal Découvrir MetaOCaml dans son navigateur. Évalué à 2.
C'est pour ça que c'est intéressant ! Il faut bien que l'on finisse par comprendre. :-)
Comment fais-tu avec des variants et l'approche initiale si tu veux rajouter des
intet l'opération d'additionaddau langage jouet avec les booléens ? Il faut redéfinir une nouvelle structure de données et réécrire le code (c'est une des raisons pour laquelle MetaOCaml est un fork, il étend le type Parsetree de l'AST du langage OCaml). Il y a bien les variants polymorphes mais comparé à l'approche initiale avec GADT il n'y a pas de vérification de typage : il faut écrire un type checker. Là dans mon langage jouet ça va, il n'y a qu'un seul type — les booléens — mais si on rajoute lesintil faut vérifier statiquement que le premier paramètre deif_est bien un booléen.Avec l'approche finale on a de l'héritage multiple. Il suffit de définir différents sous-ensembles de langages, de construire le langage que l'on souhaite par héritage et on récupère tout le code de ses sous-langages. Dans mon journal en écriture j'ai trois langages : un avec des
int, un autre avec desboolet un autre avec uniquement des fonctions (du pur lambda-calcul). Le langage jouet avec booléen et fonction est obtenu en combinant les deux derniers.C'est juste un niveau d'abstraction au-dessus, comme avoir des fonctions en tant que valeur comme les autres dans les langages fonctionnels par rapport aux langages qui n'en ont pas. D'ailleurs j'ai commencé à lire le cours de Jeremy, et sa deuxième leçon m'a donné une idée. Sa leçon consiste à utiliser MetaOCaml pour optimiser le code d'une stack machine implémentée avec des fonctions plutôt qu'un GADT.
Avec l'approche final, on peut faire une chose similaire sans MetaOCaml. Je montrerai juste la sortie d'optimiseur que j'ai codé sur le langage complet qui hérite des trois dont j'ai parlé : entier, booléen et fonctions.
Avec l'approche finale les optimiseurs sont assez simples à coder, on ne les fait que pour la partie du langage qui nous importe (addition, structure de contrôle, fonction…) et on les reprend telle quelle pour tous les langages qui en héritent. Là je montre la passe pour réduire les additions en rentrant dans la pile :
Dans le fond on écrit le code des fonctions comme d'habitude, il faut juste les passer dans la fonction
lamet on peut définir de macros pour simplifier l'écriture :Je vais essayer de le mettre au point dans la semaine. Je comprends que tu ne viennes pas souvent, l'ambiance est spéciale par moment. Si je ne te vois pas réagir au journal, je t'enverrai un mail.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
Posté par kantien . En réponse au journal Découvrir MetaOCaml dans son navigateur. Évalué à 2.
En fait, je vais arrêter là. Je me suis rendu compte, en réfléchissant plus, que je me suis fourvoyé. :-/
Dans leur article, pour gérer les évaluations partielles ils utilisent deux techniques : les types fantômes et MetaOCaml. Mon exemple avec les GADT remplace l'utilisation des types fantômes. Cela n'a rien d'étonnant, ils ont été introduits en partie pour cela : on les appelle aussi first-class phantom type. Par contre MetaOCaml et son type
('a,t) codejoue le rôle de mon interprèteShowHOde pretty printing. Donc que je n'ai pas besoin de MetaOCaml dans mon code est normal : j'utilise un autre interprète. :-PPour ce qui est de faire une dépêche sur MetaOCaml, je ne le connais pas du tout, il faudrait que j'expérimente avec pour en savoir plus. Là la seule chose que je sache c'est le principe du dialecte : différer les calculs sous le contrôle du développeur (c'est proche des
quoteetunquotedu LISP, il me semble).Pour exposer plus en détail l'approche tagless, j'ai un journal en préparation mais il faut que je restructure. J'ai deux textes de 900 lignes : un sous forme de fichier
.mlavec du code commenté et illustrant le principe tant des extensions de langage via héritage multiple que les optimisations, un autre plus dans la forme d'un journal avec moins de code et comparant la méthode « classique » avec variant pour l'AST et la méthode tagless.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
Posté par kantien . En réponse au journal Découvrir MetaOCaml dans son navigateur. Évalué à 3.
C'est ce que j'avais compris de ta présentation de BER MetaOCaml sur lambda-the-ultimate et des commentaires qui ont suivi. Son principe est sain : construire une tour dont on n'a pas assez étudié les fondements, cela mène à la tour de Pise et ensuite il faut coller des étais de tous le côtés pour que ça ne se casse pas la gueule. Cette dernière façon de procéder est une pratique architecturale douteuse et non recommandable. ;-)
Je ne me suis jamais penché vraiment sur MetaOCaml car bien que les primitives soient claires, je trouvais la syntaxe un peu lourde. Les liens de ton journal seront une occasion de regarder cela de plus près.
Pour la méthode tagless qu'il a mise au point conjointement avec Carette et Shan, elle donne une solution élégante au problème de l'extension : ajouter des cas aux variants et ajouter des traitements sur les données sans avoir à recompiler et avec la sécurité du typage statique. Wadler a développé les generics en Java pour cela, en C++ ils ont les templates mais dans les deux cas il faut utiliser le visitor pattern que je trouve étrange. De leur côté les langages fonctionnels ont la technique du fold, plus naturel, pour se substituer au visitor pattern mais pour réutiliser du code et ajouter des cas aux variants c'est compliqué. Là avec leur solution, on a de l'héritage multiple via le système « d'héritage » des modules et on n'a pas besoin de variants exotiques comme les variants polymorphes ou les GADT pour garantir le typage. Oleg l'avait signalé sur la discussion « GADT vs. Type Classes ».
Là où je vois une ouverture vers MetaOCaml en OCaml standard, c'est dans la combinaison de cette méthode avec les GADT pour l'évaluation partielle. Dans l'article dont j'ai donné le lien dans mon précédent message, ils utilisent MetaOCaml pour faire de l'évaluation partielle et jouer sur deux niveaux : statique et dynamique. Avec les GADT, on peut s'en passer ! :-)
Un exemple rapide. On prend un langage simple avec des booléens, la structure de contrôle if-then-else et des fonctions. Dans leur approche, le langage est défini par la signature suivante :
Ici chaque fonction mime les branches d'un variant avec GADT. Ainsi la signature exprime clairement la syntaxe et la sémantique du langage sans avoir besoin des GADT. Pour la structure if-then-else, on met chaque branche dans un thunk (
unit -> 'x) car OCaml fait du call-by-value et cela permet de n'évaluer la branche que si l'on en a besoin. Ensuite plutôt que de faire un fold sur un variant avec GADT pour faire varier les interprétations, on implémente des modules qui satisfont cette interface.Là je passe les détails pour deux interprétations classiques :
evalpour évaluer les termes du calcul etshowpour faire du pretty printing. Mais là où les GADT deviennent intéressants c'est pour faire des optimisations comme de l'évaluation partielle.Dans leur article de présentation, ils utilisaient un enregistrement avec un type
'a optionpour la partie statique et une type('c, t) codede MetaOCaml pour la partie dynamique. Avec les GADT, pas besoin de MetaOCaml. L'idée est reprise du tutoriel Modular, composable, typed optimizations in the tagless-final style sur le site de Oleg.Maintenant pour les liens avec les macros et le recours à l'évaluation partielle :
Soit on se sert de OCaml pour rajouter la primitive
not_au langage sous forme de « macro », où on l'implémente dans le langage vu qu'il dispose des fonctions. À l'usage :En espérant n'avoir pas trop dévié du thème original du journal.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
# Tagless final un chemin vers MetaOCaml en bibliothèque ?
Posté par kantien . En réponse au journal Découvrir MetaOCaml dans son navigateur. Évalué à 1. Dernière modification le 12 novembre 2016 à 23:17.
Tout d'abord merci pour ce journal et le lien vers la présentation de Jeremy Yallop. Ça va me faire de la lecture. :-)
J'ai une question à te poser. Il me semble que le développeur principal de MetaOCaml, et qui a repris le projet, est Oleg Kiselyov. J'ai cru lire sur son site qu'il avait grandement réduit la quantité de code qui le sépare du compilateur standard, et qu'il espère un jour pouvoir en faire une simple bibliothèque plutôt qu'un dialecte.
J'ai justement un journal en cours d'écriture pour présenter la méthode tagless final pour plonger un langage en OCaml et faire de l'évaluation partielle sans passer par des variants pour représenter l'AST mais en utilisant des modules et des foncteurs. Bon, il va falloir que j'élague un peu parce que là j'ai un pavé. :-P
Depuis que je joue avec cette méthode, j'en suis venu à voir OCaml comme un langage de macros typés pour le langage objet ce qui permet de faire de la méta-programmation intéressante sur celui-ci ainsi que des passes d'optimisations simples à réaliser, indépendantes, modulaires et facilement composables. Au final je me demande si cette méthode n'ouvre pas la voie vers la possibilité de ramener MetaOCaml à une simple bibliothèque ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Peut être pas la bonne approche ?
Posté par kantien . En réponse à la dépêche surveillance:// Entretien avec son auteur Tristan Nitot et 10 livres à gagner. Évalué à 3.
Il y a bien un moyen que les GAFAM ne possèdent pas et qui reste la prérogative des États : celui de définir le droit (pouvoir législatif), de rendre la justice selon le droit (pouvoir judiciaire) et d'exécuter les sentences juridiques via son bras armé (pouvoir exécutif). C'est là le domaine (et le seul) qui doit relever du monopole de l'État et sur lequel se fonde sa souveraineté. Raison pour laquelle, la réponse du chiffrement face aux États n'est qu'un pis aller — révélateur d'un recul ou d'une absence de l'état de droit — et la seule réponse qui vaille est politique c'est-à-dire juridique et non technique.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: alternative crédible
Posté par kantien . En réponse au journal Le courage de l'innovation. Évalué à 3.
chouchou: j'trouve pas d'réseau wifi dans cette maison ?! C'est nul, y'a pas l'internet !!!! :-(moi: mais si ! faut juste que tu t'colles un fil à la patte : l'ethernet c'est le top pour l'internet ! \o/chouchou: j'm'en fous d'ton fil, mets moi le wifi !!!!! :@Voilà une situation qui me semble bien plus proche de la réalité pour la grande majorité de la population. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: abort != avorter
Posté par kantien . En réponse au journal Gestion des erreurs d’allocation mémoire en C. Évalué à 2.
Il est vrai que si le verbe anglais to abort et le verbe français avorter sont issus d'une racine commune, l'évolution de l'usage anglais en a fait un verbe qui peut être intransitif ou transitif. Là où en français, lorsque le sujet de la proposition est l'agent qui pratique l'avortement, on préférera utiliser des formulations comme « faire avorter qqch. », « arrêter qqch. » ou « interrompre qqch. ». Comme le montre ces quelques exemples issus de linguee :
Malgré cela, le projet ourdi en secret par les grammar nazi afin de conquérir le monde n'a pas encore avorté. :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: abort != avorter
Posté par kantien . En réponse au journal Gestion des erreurs d’allocation mémoire en C. Évalué à 2.
Certes mais, comme il t'a répondu, il l'utilise bien comme une verbe intransitif dans son journal. Du moins, on peut discuter ce dernier point. En dehors de son usage en titre de section, il écrit :
On peut soit considérer que les auteurs ont décidé d'avorter le programme (qui serait ici sous-entendu en fonction objet) ce qui en ferait bien un usage incorrect en tant que verbe transitif; soit, toujours dans une acception figurée du verbe, considérer que le programme représente le processus par lequel les auteurs veulent engendrer un résultat et ils décident d'avorter en cas d'erreur produisant ainsi quelque chose étant mort; ou encore on pourrait écrire, par métonymie, en substituant l'agent par l'instrument : le programme avorte en cas d'erreur.
Quoi qu'il en soit, je ne vois toujours pas en quoi un tel usage relève d'un affreux anglicisme (sic). ;-)
Aucun drosophile n'a été abusé sexuellement au cours de cet échange linguistique.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: abort != avorter
Posté par kantien . En réponse au journal Gestion des erreurs d’allocation mémoire en C. Évalué à 2.
C'est surtout un « affreux » latinisme au sens figuré ! Il y a aussi du latin dans la langue anglaise, et ce sens figuré se pratiquait déjà en France au XIIe siècle. ;-)
Mot qui vient du latin aborto : mettre à jour avant terme.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: TP-Link et FCC
Posté par kantien . En réponse au journal Point d'étape sur le matériel et nos libertés partie 2. Évalué à 5. Dernière modification le 26 octobre 2016 à 18:35.
Article intéressant à plus d'un titre. Voici mon résumé de ce que j'en ai compris :
TP-link a écopé d'une amende de 200.00 $ parce qu'ils vendaient des routeurs permettant d'être utilisés à une puissance supérieure à la limite autorisée par les règles de la FCC. Mais cette infraction ne relevait pas de la nouvelle réglementation sur le 5 GHz, dont parle le journal, mais des règles sur la bande à 2.4 GHz : en changeant une option dans la configuration du routeur (le code du pays) celui-ci pouvait émettre à une puissance trop forte. Pour corriger le tir, TP-link a fait une mise à jour de son firmware qui au passage empêchait l'installation de tout autre firmware issu de tierce partie : telle fut la solution choisie pour satisfaire au passage à la nouvelle réglementation sur le 5 GHz. Ce en quoi le règlement du FCC ne stipule pas que l'on ne puisse installer d'autre firmware que ceux fournis par TP-link, mais seulement que ceux-ci ne doivent pas permettre d'utiliser le matériel en dehors des limites légales. Et finalement, pour ne pas payer une amende plus importante, la FCC et TP-link sont tombés sur un accord obligeant ce dernier a collaboré avec les fabricants de chipset Wi-Fi et la communauté open-source pour permettre aux utilisateurs d'installer le firmware de leur choix. On apprend de plus, en fin d'article, que Linksys, sans être contraint de le faire, a déjà travaillé avec Marvell et OpenWRT pour être certain que ses routeurs satisferont la nouvelle législation sans bloquer les firmwares libres.
Me vient donc deux questions :
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Remarques diverses et ... tardives
Posté par kantien . En réponse au journal Gestion de l'erreur - C++ - std::optional. Évalué à 1.
Effectivement c'est une meilleure approche si on veut plus d'information sur la raison de l'échec.
Dans le même genre, à la place des
Maybe a, en Haskell on peut utiliser lesdata Either a b = Left a | Right b.Et en Ocaml, il y a soit le type
'a option = None | Some of 'asoit le type('a, 'b) result = Ok of 'a | Error of 'b.Ce qui correspond à la classe
std::expected<T,E>proposée pour le C++ :Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Jai: Language for game programmming
Posté par kantien . En réponse à la dépêche C++17, Genèse d’une version mineure. Évalué à 2.
Dans la série liens intéressants et instructifs : Demystifying Type Classes sur le site de Oleg Kiselyov. D'une manière générale, son site est une véritable mine d'or ! :-)
Sur cette page, il y explique de manière didactique et complète le principe des type classes en étudiant trois implémentations possibles du système dans un langage : par passage de dictionnaire, par monomorphisation ou par analyse intentionnelle de type. La première étant la plus répandue et les deux secondes étant issues de l'article pionnier sur le sujet : Parametric overloading in polymorphic programming languages de Stephan Kaes en 1988 (un lien vers cet article est donné en bas de page).
On y trouve aussi une comparaison avec des techniques du C++, comme il le souligne en conclusion :
Traduction rapide :
La dernière technique m'a donné une idée un peu différente de la sienne, mais largement inspirée de son illustration en OCaml, en utilisant des types sommes ouverts et des GADT. Exemple avec la fonction
show:Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Harmonie ?
Posté par kantien . En réponse à la dépêche Sortie de la bibliothèque d’analyse musicale Bliss 1.0. Évalué à 3.
C'est vrai mais cela peut être une piste intéressante à explorer pour les futures évolutions de la bibliothèque.
Lorsque l'on conçoit une set list pour un concert, ou même lorsque l'on réfléchit à l'ordre des chansons sur un album c'est une information que l'on prend en compte. Le principe ayant était poussé à l'extrême sur l'album concept Le fil de Camille qui tournait autour de la note si restant en bourdon.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Money makes the world go round
Posté par kantien . En réponse au journal Les routeurs Turris Omnia sont livrés. Évalué à 4.
Non, pas nécessairement.
Non, pas nécessairement.
Comme tu ne sembles toujours pas comprendre ce qu'est l'argent, je vais extraire la partie la plus importante sur le sujet du lien que j'ai donné plus haut (le texte est long, mais ça vaut le coup de le lire si tu veux bien comprendre de quoi tu parles lorsque tu parles d'argent).
L'argent n'apparaît que lors des échanges à titre onéreux et non à titre gracieux : autrement dit lorsqu'une personne dit à une autre « j'accepte de faire cela pour toi à la seule condition que tu fasses ceci pour moi ». On peut même dire que ce sont ces types de contrats qui créent l'argent : l'argent ce n'est que de la reconnaissance de dette. Il ne fait que représenter un troc suspendu, différé ou non finalisé.
Il y a une grande différence entre ces trois propositions :
Ce que l'on te dit c'est que l'on ne peut exiger d'autrui qu'il échange avec nous à titre gracieux, c'est-à-dire sans contrepartie.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Tél
Posté par kantien . En réponse au journal Les routeurs Turris Omnia sont livrés. Évalué à 1.
L'important ce n'est pas les deux numéros, mais qu'ils correspondaient à deux lignes distinctes. Chez Orange, j'ai toujours eu une ligne branchée directement sur la prise et l'autre était branchée sur la box. Si tu appelais le numéro en
09, les téléphones connectés directement à la prise ne sonnaient pas. Dans ton cas, les numéros en01et09correspondent-ils à deux lignes distinctes ou sont-ce deux alias pour la même ligne ?Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Tél
Posté par kantien . En réponse au journal Les routeurs Turris Omnia sont livrés. Évalué à 2. Dernière modification le 21 octobre 2016 à 09:54.
Cela doit bien être possible, étant donné que c'est réel : cela fonctionne comme cela chez moi. ;-) Pour les détails techniques, je n'ai aucune idée de la manière dont cela fonctionne.
Avant j'avais deux lignes : une avec le préfixe en
01-05(selon la région) et une autre en09. Maintenant je n'ai plus que la première avec la même offre que celle que j'avais avec la seconde, ce qui est tout de même plus simple pour l'usager : il ne fallait pas se tromper de ligne lorsque l'on appelait.Edit : je parle de l'offre ADSL.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Money makes the world go round
Posté par kantien . En réponse au journal Les routeurs Turris Omnia sont livrés. Évalué à 5.
Il y a un malentendu sur la notion de logiciel libre. Pour citer la référence FSF et RMS :
Traduction : « Pour comprendre le concept, vous devriez penser à « free » comme dans « liberté d'expression », non comme dans « bière gratuite ». Nous l'appelons parfois « logiciel libre », empruntant le mot français ou espagnol pour « free » comme dans « liberté », pour monter que nous ne signifions pas par là que le logiciel est gratuit. »
Le texte original est essentiellement destiné aux anglophones, car en anglais le mot « free » peut signifier aussi bien « libre » que « gratuit », ambiguïté qui n'existe pourtant pas dans la langue française.
Pour rebondir sur la remarque « l'argent n'est que du travail figé » de Marotte, je rajouterai que le principe de base de l'économie marchande c'est le troc : je te donne ça si tu me donnes ça en échange ou je fais cela pour toi si tu fais cela pour moi, i.e. échange de biens et services. L'argent c'est juste un troc non finalisé, et permet de recevoir en échange du service rendu un service de la part d'une autre personne que celle à qui l'on a rendu service : c'est un bien qui améliore grandement les échanges librement consentis de services, là où sans cela le système de ton village africain ne pourrait nullement passer à l'échelle. ;)
Maudit argent !
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.