gasche a écrit 1151 commentaires

Dans le cas de LLVM, c'est clair que oui : une grande partie des mainteneurs de LLVM et Clang sont payés par Apple pour bosser à temps plein sur le projet. LLVM était prometteur au moment où Apple a mis le grapin dessus (ils cherchaient un truc pour se débarasser de GCC et sa licence), mais il ne serait pas forcément arrivé depuis à ce niveau de maturité sans le soutien d'Apple. C'est une bonne affaire pour cette boîte, puisqu'ils ont aussi acquis les talents pour faire Swift et redevenir compétitifs en terme de confort de programmation mobile. (Apple est une entreprise détestable par de nombreux aspects, mais qui a toujours fait de beaux paris techniques et, de façon intéressante, a souvent cru en le choix de meilleurs langages de programmation (HyperCard, Dylan, etc.).

Je pense que c'est bien de tempérer l'image assez injuste "GCC c'est un truc de vieux maintenant le futur c'est LLVM", mais il ne faut pas non plus verser dans l'excès inverse: LLVM et GCC sont deux bons projets qui se font une concurrence très sérieuse et sans doute bénéfique des deux côtés. Par ailleurs les critiques sur la difficulté à se plonger dans le code source de GCC, qui avaient motivées en grande partie les contributeurs passant à LLVM au départ, sont sans doute toujours valide en grande partie—et le fait que le code de LLVM prenne de l'âge est un peu indépendant.

Peut-être que l'erreur vient de toi, c'est d'espérer trouver un compilateur miracle qui réponde au rêve du projet parfait à soutenir et défendre contre tous les autres. Ce compilateur miracle n'existe sans doute pas. (Ou ça dépend ce qu'on cherche; CompCert a un côté miraculeux.)

Pour ce qui est de la recherche, j'espérais le dire dans mon journal mais j'ai un peu oublié : il y a des gens qui font de la recherche en compilation et qui contribuent et à GCC et à LLVM. Ils ne travaillent pas forcément sur les parties du compilateur citées dans le message de Daniel Berlin, qui sont en train d'accumuler des couches, mais par exemple le travail sur Polly est développé et maintenu par des chercheurs et chercheuses, à la fois dans GCC et dans LLVM.

Pour revenir sur la question de quels sont les "compilateurs intéressants", je pense que ça dépend de ce qu'on veut y trouver. Pour un compilateur qui intègre régulièrement des résultats de recherche en compilation, GCC et LLVM sont plutôt raisonnables; il y a des projets de recherche plus ciblés et peut-être plus innovants (au sens noble du terme), mais ils ne cherchent pas forcément à couvrir les besoins des utilisateurs arbitraires de C ou C++—si ton rêve c'est les optimizations backend tu ne vas pas forcément te farcir un frontend C++.

Après mon rêve à moi c'est plutôt les langages que les compilateurs, et j'aurais tendance à m'intéresser plutôt aux langages qui font des choses chouettes, même quand leur backend est un peu simple (OCaml, Haskell) ou simplement délégué à LLVM (Rust, Pony, Pure, Julia).

CUPS n'est pas vraiment un exemple puisqu'il a été racheté récemment par Apple après des années d'usage dans le libre. Personne ne se plaint que son mainteneur ait maintenant un boulot, et je suppose qu'il continue à améliorer aussi la partie du code libre utilisée par Linux (je ne sais pas, je ne suis pas le développement de près), mais on ne peut pas dire que c'est la participation d'Apple qui a fait son succès.

Un autre non-exemple serait MySQL: ce n'est pas la participation d'Oracle qui fait son succès. (Les grincheux auraient envie de dire "au contraire" et ils n'auraient pas forcément complètement tort, même si je suis surpris de la ténacité de MySQL alors qu'il existe un fork communautaire très compatible, MariaDB; on n'est pas au niveau de flingage qu'on a pu voir pour OpenOffice).

Je suis parfois du côté du mainteneur et je suis d'accord avec ce que tu dis. La différence principale est sans doute, comme le fait remarquer, la valeur que l'on attache au mot "grincheux"—chez moi il y avait un effet non-sérieux voulu mais ce n'était pas vraiment péjoratif.

Merci d'avoir développé autant, je suis sûr que ça va intéresser des gens. Quelques compléments:

• Tu dis "les deux se défendent" comme s'il y avait deux positions discrètes, le tout-va et le toujours-nickel. En pratique il y a un continuum et on peut être "plus souple" ou "plus strict" sans passer d'un extrême à l'autre.

• Tu ne parles que des "bons cas" dans les deux scénarios. Il y aussi les cas où ça ne se passe pas bien. Par exemple, parfois le mainteneur n'est pas satisfait avec un patch, mais il ne sait pas exactement expliquer pourquoi ou ne sait même pas quelle est la meilleure approche, il n'a pas envie de demander au contributeur de faire ce travail de recherche mais il n'a pas le temps de le faire lui-même non plus, et donc il évite le problème, ne dit rien, et le patch stagne. Dans les conflits dont on entend parler où un mainteneur bloque un projet, c'est souvent ce genre de problèmes à la base, où les gens s'accrochent à une notion de qualité qui a l'effet de geler le projet. C'est très facile de tomber dans ce travers là, ça m'est arrivé à moi aussi, et je pense que que c'est important d'en être conscient.

• Je me suis posé aussi la question de quand rebaser de mon côté pour faire les petits correctifs mineurs qui ont du sens pour moi mais pas forcément pour les contributeurs non fréquents. À ma surprise à l'époque, les contributeurs m'ont demandé d'arrêter: ils n'aiment pas qu'on modifie leurs patchs "derrière eux" parce qu'ils ont vraiment envie d'apprendre comment faire le patch parfait et ils préfèrent donc que je leur explique les changements à faire. Maintenant je ne le fais que très très rarement.

À quand un kakoune-mode dans Emacs ou Spacemacs ? L'éditeur proposé a l'air d'avoir des idées chouettes, mais j'aurais du mal à abandonner les autres programmes de mon OS.

Merci pour les compliments et les remarques. Je passe souvent de l'anglais au français et il m'arrive de rater mes convenients. J'aimerais mieux que le moteur de rendu de linuxfr mette la bonne typographie pour le français (ajoute l'espace nécessaire avant : ou ; et gère les -- correctement). Hélas il n'est toujours pas possible d'éditer ses messages sur LinuxFR donc, comme je remarque ce genre de soucis systématiquement après avoir publié le message, il y a très peu de chances que j'arrive à corriger ici. J'essaierai d'en tenir compte sur les plateformes dont les utilisateurs se font assez confiance les uns aux autres pour s'autoriser à éditer leurs messages.

(La typographie c'est un sujet maudit à mon avis : on est heureux tant qu'on l'ignore, et le fait de l'apprendre n'attire que des désagréments — et on peut difficilement le désapprendre. Attention à bien mesurer les risques que tu fais subir aux gens en leur faisant des points d'information !)

je ne cherche pas à dire que les spécifications de CompCert sont fausses, seulement qu'on ne peut pas savoir si elles sont complètes et réalistes

Comme le souligne kantien, il n'est pas clair de savoir ce que tu veux dire par "complètes et réalistes". J'aimerais expliquer pourquoi je me permets de chipoter ici. On a peu de logiciels vérifiés formellement, Compcert est un des premiers qu'on puisse envisager d'utiliser à grande échelle (parce que bon tout le monde n'a pas de raison de faire tourner SeL4 ou CertiKOS sur sa machine, alors qu'un compilateur C si), donc c'est le bon moment de bien comprendre et bien expliquer les garanties (non absolues, bien sûr) données par la vérification formelle. Au grand public, on peut se permettre des approximations et simplifications—encore que. Mais toi tu sembles assez proche du milieu de la recherche pour avoir un avis (foireux) sur comment citer les articles, alors je pense que ça vaut le coup de pousser la discussion un peu plus loin et de te demander d'être précis dans la critique que tu as en tête.

Je ne suis pas suffisamment expert pour juger de la validité des bugs ou non. En revanche, ils précisent bien que les auteurs de CompCert eux-mêmes ont reconnu la validité de ces bugs (qui ont j'imagine été corrigés depuis).

J'aimerais mieux qu'on discute de la question technique sous-jacente (les soi-disant bugs; tu peux essayer de te renseigner mieux, puisque le sujet t'intéresse; moi je me suis renseigné en lisant l'article et j'ai donné mon avis), plutôt que de discuter de on-dit. On n'a pas la réponse précise des auteurs de Compcert, le fait que les auteurs d'un article (qui, même de bonne foi, ont tout intérêt à gonfler l'importance des remarques qu'ils ont fait sur Compcert) disent vaguement "les auteurs sont d'accord" ne veut pas dire grand chose—par exemple si j'étais un auteur poli, ma réponse sur le premier "bug" rapporté serait quelque chose comme "merci beaucoup pour ce retour, je vais effectivement corriger ça, en testant plus strictement les accès aux sous-objets je peux rendre l'interpréteur plus utile", ce qui ne veut pas dire qu'un bug a été trouvé dans Compcert, mais peut être présenté par les auteurs de l'article comme "les auteurs de CompCert sont d'accord et d'ailleurs ont corrigé"—ce qui est faux si on interprète comme tu le fais "sont d'accord" comme "reconnaissent un bug dans Compcert". On est dans l'hypothétique là, et justement j'aimerais en sortir en discutant le fond et pas qui a dit quoi.

Le fait qu'une remarque aux auteurs conduise à un changement dans CompCert ne veut pas du tout dire qu'il y avait un bug à la base. Par exemple le second problème rapporté dans l'article est lié au type de la fonction main, on peut trouver un correctif associé dans le commit 3eb2b3b7bb464, mais la version avant correction respectait tout autant la spécification de correction et compilait tout aussi correctement les programmes valides.

Je considère au contraire que la conférence/journal (ainsi que l'année, incluse dans cette notation) est bien l'une, si ce n'est la plus importante, des informations à donner—à l'inverse de la liste des auteurs qui est bien elle l'information la moins importante.

Question de point de vue peut-être, mais qui n'est pas totalement subjective ou arbitraire. En nommant les auteurs je les récompense pour leur travail (puisque la valeur dans le milieu de la recherche n'est pas récompensée financièrement mais par la reconnaissance)—ça me semble très important et juste, et en particulier je préfère toujours citer tous les auteurs et pas "Machin et al.". En nommant la conférence, tu donnes l'impression que la valeur du travail est liée à la réputation de la conférence : les travaux publiés dans une "bonne" conférence sont mis en valeur et ceux qui viennent d'une conférence moins connue sont moins bien considérés. C'est un système qui me semble dommageable, qui encourage la compétition et les mauvaises pratiques—au contraire je préfère que le travail des gens parle de lui-même, qu'on juge l'article par son contenu et pas son étiquette. Après si tu tiens à citer la conférence aussi, rien ne t'en empêche et c'est plutôt la norme, mais le mettre à la place du nom des auteurs me semble mauvais.

(Il faut distinguer de la façon dont les gens citent leur propre travail, par exemple dans leur CV ou leurs exposés de présentation de carrière. Dans ce cas il est courant et compréhensible d'utiliser le format CONF'YY, puisque les auteurs sont toujours l'exposant et ses collaborateurs. Et puis ça correspond à la façon dont beaucoup de gens se souviennent de leurs propres travaux: ils ou elles peuvent avoir plusieurs publications sur la même année et se souviennent souvent bien de l'endroit où chaque travail a été présenté. Mais ça ne se généralise pas nécessairement aux travaux des autres.)

Tu mélanges un peu deux choses différentes: une spécification peut être différente de la réalité, et aussi il y a des parties d'un programme à qui on ne sait pas forcément donner de spécification. Les erreurs trouvées par Csmith¹ sont dans des parties du logiciel qui n'avaient pas de spécification formelle (par exemple l'affichage de code assembleur, depuis la représentation interne du compilateur à un fichier texte à passer à un outil externe), et pas dans des erreurs d'une spécification qui les couvrirait. (Je chipote; mais on ne peut pas vraiment parler de gap spécification/réalité ici.)

¹: Csmith c'est ce que tu appelles "PLDI'11"; je ne suis pas convaincu par cette façon de nommer des articles qui tait l'important (le titre et les auteurs—et l'année) et montre la conférence, peu importante et source de vanité.

Les "erreurs" citées par l'article "Randomized Stress-Testing of Link-Time Optimizers" de Vu Le, Chengnian Sun et Zhendong Su me semblent extrêmement suspectes, pour ne pas dire foireuses. Il faut réfléchir à ça plus en détail mais je ne crois pas qu'il soit correct de dire que ce sont des bugs de Compcert. Dans un cas, c'est un comportement qui n'est pas défini selon la norme C, mais qui est défini par la spécification "Compcert C" qui est plus fine; ce n'est pas un bug, mais une différence d'interprétation. Le second "bug" concerne un comportement de l'interpréteur, pas du compilateur, et il s'agit d'un message d'erreur oublié pour une façon particulière de rejeter le programme sans l'exécuter—donc il n'y a même pas eu d'interprétation incorrecte. Dans le cas du premier soit-disant bug en tout cas, j'ai l'impression que les auteurs n'ont pas compris les garanties données par Compcert.

La liberté de parler, de donner ton opinion, tout le monde l'a. Mais en faisant cela, on encourt le risque que quelqu'un d'autre fasse remarquer que cette opinion donnée (1) ne fait pas avancer grand chose, (2) pourrait être remplacée par une action concrète et utile et (3) a peu de valeur car elle est basée sur une déformation des faits et pas sur la réalité.

Tu dis que "la FSF et GNU ont les mains libres", mais aucun de ces deux groupes de gens n'est intervenu dans l'histoire en question—à part indirectement, à travers l'influence (reconnue et consentie) qu'ils ont sur les gens qui maintiennent et développent Emacs aujourd'hui.

Je ne suis pas forcément en désaccord, par ailleurs, avec une partie de ce que tu dis sur le projet GNU ou la FSF—j'ai parfois des réserves aussi. Mais je pense qu'il faut trouver un équilibre entre l'opinion et l'action : nos écosystèmes de logiciel libre ne peuvent rester actifs et vivants que si tout le monde fait un effort pour s'emparer de la capacité de faire des améliorations et la transmettre, et ça passe par le fait de savoir se dire : "et si on contribuait concrètement à ce problème dont on discute ?".

D'abord, personne ne connaît le code de Emacs ici, et certainement pas mieux que ses développeurs.

Ce n'est pas grave, il suffit de se jeter dans le bain. Ça prend certes plus de temps que ça ne prendrait à un développeur (je dirais que pour un projet inconnu je compterais une demi-journée pour mettre en place l'environnement de développement: télécharger et compiler les sources, trouver quels tests lancer pour tester une modification, etc.), mais c'est une bonne expérience qui apprend plein de choses et une façon agréable et constructive de donner un coup de pouce à un projet—tiens, des gens discutent d'une fonctionnalité manquant dans Emacs, et si je l'implémentais ?

La discussion que j'ai pointée dans mon premier commentaire contient des détails sur quels endroits modifier dans le code et, implicitement, de qui est un peu intéressé par ce sujet et serait partant pour donner des conseils, relire un patch proposé, etc. Parfois un contributeur extérieur ne va pas implémenter la fonctionnalité de "la bonne façon", mais le fait qu'un patch soit proposé va donner envie aux mainteneurs d'aider, de donner des conseils, et de faire avancer cet aspect du logiciel auxquel il n'avaient pas auparavant accordé d'importance.

Bref, ce n'est pas qu'une question d’énergie/motivation, mais avant tout de compétences.

À partir d'une base correcte en programmation (quelle que soit le langage), les compétences nécessaire à ce genre de contributions s'acquièrent assez facilement. Il suffit de faire un effort pour contribuer de manière constructive, et le reste vient avec.

Et par ailleurs, avoir autant peu de respect pour le débat public, quel qu'il soit ("fermez-là et codez !"), est bien plus choquant que les quelques piques écrites plus haut à l'attention de la FSF & Co.

Tu réduis mon argument en le présentant de façon absurde et en m'accusant d'un mal terrible—c'est assez insultant.

Dans le monde du logiciel libre, "those who do the work decide", ceux qui font le travail décident. Discuter peut être utile, comme dans n'importe quel autre cadre, et la communication peut faire et défaire les projets; mais je pense que chacun et chacune devrait essayer de se tenir à une hygiène, un certain équilibre entre le fait de consommer et réagir passivement à des changements (on ne peut pas être présent sur tout), et le fait d'être au contraire moteur de changements quand on voit qu'il y a un coup de main à donner pour aider.

Ce que tu appelles "débat public" ici, c'est un mélange entre une discussion de fond légitime et peut-être intéressante, et un décalage complet par rapport à la réalité. Personne ou presque n'a fait l'effort de chercher de quoi cette histoire ressort réellement; on s'écharpe sur un article de blog qui lui-même déforme les faits en extrapolant à partir d'un résumé de la discussion présente dans le Changelog. On insulte ou on défend Richard Stallman (RMS)… mais RMS n'est jamais intervenu dans cette discussion et la décision. Pareil, la FSF n'a pas mis son nez dans cette affaire—ou un représentant du projet GNU en dehors de l'équipe qui développement collaborativement Emacs.

Je vois deux commentaires qui partent des faits réels et non d'une vision déformée: mon commentaire initial, pointant vers la discussion réelle, et le commentaire d'alenvers qui explique que la personne ayant implémenté la fonctionnalité et la personne l'ayant retiré sont la même personne. Encore une fois, discuter c'est bien, mais s'informer c'est mieux. Est-ce "insulter le débat public" que de pointer ça du doigt ? Au contraire, je pense que les gens qui se lancent tête baissée dans une confrontation sans faire l'effort d'aller chercher des informations fiables (alors que justement c'est facile pour les projets libres où tout ou presque est discuté publiquement) lui font plus de tort, à ce fameux débat public.

Sur la question de where, il y a deux niveaux de réponse.

1. Pourquoi ça a été enlevé. Ça a été enlevé parce que Xavier Leroy a conçu Caml Light comme un sous-ensemble simplifié du Caml existant à l'époque, en retirant tout ce qui lui semblait peu utilisé en pratique ou redondant. Donc where a sauté parce qu'on avait déjà let pour faire la même chose.

2. Pourquoi ça n'a pas été remis. J'aime bien where aussi et si j'étais convaincu de pouvoir fournir une argumentation solide pour le remettre, je l'aurais fait. Le problème c'est que where pose plein de questions délicates sur les précédences de la grammaire qui n'ont pas de réponses claires—je m'en suis rendu compte en implémentant une extension de syntaxe pour where, pa_where. let <p> = <e1> in <e2> est une construction qu'on peut appeler "ouverte à droite", il y a un délimiteur qui ferme la construction sur la gauche mais pas sur la droite (comme if <e1> then <e2> else <e3> ou d'autres, mais au contraire de begin <e> end qui n'est ouvert d'aucun côté). Au contraire, <e1> where <p> = <e2> est ouverte à gauche; mélanger des constructions ouvertes à gauche et ouverte à droite pose de nombreux problèmes de précédence à décider. Par exemple, quelle est la signification de let x = e1 in e2 where y = e3 ? Un autre cas délicat est la gestion du and qui est commun à where et let: let x1 = e1 where x2 = e2 and x3 = e3 in e4, à qui est attaché le and ?

Dans un langage à indentation significative, on a beaucoup moins de problèmes de précédence puisque le parenthésage apporté par l'indentation ferme beaucoup plus les constructions. C'est un avantage notable de ces langages en terme d'évolutions possibles de la syntaxe.

Je ne pense pas que ta comparaison ait du sens, puisque les développeurs d'Emacs ont justement choisi de ne pas travailler sur ça, mais de travailler sur autre chose—c'est clairement dit dans le dernier message que je cite. (Par ailleurs le changement principal à faire semble être au niveau de libXft plutôt que Emacs.)

Je trouve ta réponse un peu antagonisante, d'une façon qui à mon avis n'est pas productive. Plutôt que me mettre les gens à dos, j'aimerais montrer que contribuer n'est pas si difficile qu'on peut le penser, et que ce sujet est par exemple un cas possible de contribution concrète.

OCaml n'a pas de "type families" dans ce sens; pour définir une fonction sur les types au cas par cas, on voit la fonction comme une relation entre types (donc un type paramétré ('input1, 'input2, 'output) f_or), et on définit un GADT correspondant à cette relation—dont les habitants sont les témoins dynamiques.

type open = Open
type closed = Closed
type ('a, 'b, 'c) f_or =
  | Left : (open, _, open)
  | Right : (_, open, open)
  | Closed : (closed, closed, closed)

C'est en inspectant cette valeur-témoin que tu guides le raisonnement par cas.

Note cependant que je trouve l'idée de faire une distinction entre deux cas "open" et "closed" très artificielle. On met en valeur les limites des GADTs, qui est qu'il faut penser au moment de la définition de son type à tous les usages dans les types (les fonctions depuis ses valeurs vers les types) dont on va avoir besoin. Il me semblerait plus naturel et plus général d'avoir un typage plus général Expr Env où Env est une représentation, au niveau des types, de l'ensemble des variables libres de l'expression—une représentation assez courante est d'utiliser des emboîtements de Maybe pour "compter" le nombre de variable libres connues dans le terme: Expr (Maybe (Maybe (Maybe a)))) pour un terme à quatre variable libres connues, le type vide pour un environnement clos, et par exemple Add : Expr a -> Expr a -> Expr a et Lam : Expr (Maybe a). Ça reste difficile à utiliser et donc un choix à faire avec soin—j'aurais pour ma part tendance à préférer soit une représentation moins typée soit l'usage d'un langage mieux pensé pour les types riches comme Coq ou Idris.

Bon journal; en particulier, le fait de montrer les étapes intermédiaires et "ce qui se fait sans cette technique" me semble très utile pour la compréhension. L'inconvénient bien sûr, c'est que le résultat est très long, trop long je pense pour que quelqu'un qui découvre puisse confortablement le lire en une seule fois. Il faut espérer que les gens ont la discipline de faire des pauses et de reprendre la suite un autre jour, même si la structure ne l'encourage pas forcément. Pour la suite, je t'encouragerais à écrire plusieurs journaux séparés (par exemple un journal par partie de haut niveau), étalés de quelque jours.

As-tu envisagé de le convertir en un tutoriel sur Zeste de Savoir ? C'est un site avec de bonnes valeurs d'ouverture et de diffusion de la connaisance, une équipe sympathique, et plus adaptée au stockage à long terme des connaissances que les journaux de LinuxFR, il me semble.

Points de détail:

• Quand tu dis que le typage des GADTs n'est pas "décidable", tu veux dire qu'il n'est pas "inférable": c'est le fait de deviner le type qui n'est pas décidable, pas le fait de vérifier qu'un type donné est correct (qui est ce qu'on entend par "typage décidable").

• Un pointeur complémentaire sur les GADTs, francophone, serait le cours de Programmation Fonctionnelle Avancée de Roberto di Cosmo (ou des autres enseignants ayant donné le même cours à Paris 7).

Un journal et 140 commentaires. Si on revient aux sources, c'est-à-dire les discussions de développement de Emacs, on a :

1. Clément Pit--Claudel qui s'interroge en décembre 2015 sur le support des fontes multicolores sur les différentes plateformes.

2. Il apparaît pendant la discussion de décembre que c'est bien géré par Emacs sous OSX mais par sur les autres plateformes. La discussion continue sur comment ajouter ça sur les plateformes libres. Clément indique que freetype et d'autres programmes utilisateurs (Firefox, Chrome) gèrent ça, mais Rüdiger Sonderfeld repère un blocage: libXft ne gère pas ça pour l'instant, un travail inachevé a été proposé pour cette bibliothèque, et sa finition serait nécessaire pour ce que soit facilement disponible dans Emacs.

3. Début janvier 2016, Yamamoto Mitsuharu fait remarquer qu'avoir une fonctionnalité implémentée dans OSX (il y a du code spécifique pour gérer ça dans Emacs) et pas sur les autres systèmes est contradictoire avec l'accord de principe qui a été conclu au moment de l'intégration du port MacOS. Après une relance en avril 2016, la fonctionnalité est désactivée du port Mac.

Les développeurs d'Emacs ont exprimé plusieurs fois pendant cette discussion que, même si la fonctionnalité n'était pas prioritaire pour eux, ils seraient tout à fait prêts à l'intégrer si quelqu'un faisait le travail de la faire marcher:

• Patches are welcome to add support for this to Emacs on Posix systems.

• If some volunteer wants to take it on, then we could enable it in your code.

Il est tout à fait légitime d'avoir un (long) débat sur cette approche de la responsabilité des développeurs de logiciels dans les choix de plateformes logicielles. Mais on peut aussi se demander : si une petite portion de l'énergie investie dans le débat sur LinuxFR avait été dirigée vers le fait d'aider à implémenter cette fonctionnalité dans Emacs (ou en amont dans libXft), ou au moins de communiquer avec les développeurs de la brique qui bloque pour leur faire savoir l'intérêt pour la fonctionnalité, est-ce qu'elle ne serait pas disponible aujourd'hui ?

Parler, c'est bien, mais c'est important de faire aussi, en même temps.

Agir concrètement demande des compétences, certes, mais la barrière n'est pas aussi élevée qu'on pourrait le penser; de plus, c'est en essayant de faire, en continu, est qu'on entretient une culture où c'est possible et normal, et qu'on partage les compétences nécessaires.

Bon le plus simple serait que je compile un exemple en natif et que je ragarde le dump cmm sur un cas pour voir si le code de f est bien celui que je pense.

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 !

(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.)

Il y a un débat assez proche sur la modularité au niveau purement théorique de la construction des preuves de sûreté des langages. Les techniques de preuve par induction sur les dérivations de typage sont assez simples (… quand on a tous les invariants qui vont bien qui sont exprimés par la syntaxe, ce qui est parfois loin d'être simple ou même pas bien compris du tout), mais pas contre il faut en théorie les refaire à chaque fois qu'on modifie un peu le langage, on ne peut pas prouver les constructions une par une de façon modulaire—d'ailleurs les assistants de preuve aident dans ce cas à vérifier rapidement que le reste de la preuve marche toujours. En contraste les techniques de preuves plus sémantiques comme la réalisabilité ou les relations logiques, ou en général par modèles, ont un aspect plus modulaire, puisque les constructions sont montrées admissibles une par une, et en ajouter une nouvelle ne demande pas de reprendre l'existant. Par contre elles sont nettement plus lourdes à mettre en place, et elles fixent quand même un univers de discours qu'il faut modifier et reconstruire quand on introduit des constructions vraiment différentes (enfin dans la syntaxe aussi).

Je me demande naïvement s'il serait possible d'utiliser MetaOCaml pour l'implémentation d'un tel interpréteur afin de supprimer les injections/projections sur un type universel qui permettent l'extensibilité dans le cas de la solution de "Module Mania"¹, ou de rendre performant l'interpréteur de kantien².

Oui, ça me semble une piste à creuser (en particulier le fait que certaines fonctionnalités avancées de OCaml ne soit pas disponibles dans le code stagé n'est pas forcément un problème, tant qu'on peut les utiliser depuis le code qui génère le code: à priori tu peux utiliser des GADTs pour représenter tes programmes sans les utiliser ensuite pour dans l'interpréteur). L'important pour pouvoir utiliser MetaOCaml c'est que la représentation dont tu pars contiennes assez d'information pour pouvoir inspecter les sous-termes et obtenir toute l'information qu'on peut avoir "statiquement" (qui est connue en regardant la source de l'objet représenté).

Dans ce cas MetaOCaml est à comparer avec la production d'une représentation intermédiaire pour la compilation; par exemple LLVM, mais aussi Malfunction, cf. précédent journal. D'ailleurs ce genre d'usage "staging" est justement le sujet d'un des exemples d'utilisation de Malfunction, examples/primrec.ml.

kantien parle du problème de l'extensibilité, qui est de trouver des mécanismes de langage qui permettent d'étendre, de manière sure, un ensemble de types et d'opérations, mais sans modifier (ni dupliquer) les définitions existantes, en rajoutant uniquement du code pour définir de nouvelles versions étendues. Le folklore sur ce sujet est que le style fonctionnel typique permet d'étendre facilement les opérations (on définit une nouvelle fonction) mais pas les types (ce serait: rajouter des cas dans un type algébrique), alors que le style objet typique permet d'étendre les types (on rajoute une classe dérivée) mais pas les opérations.

Dans les deux communautés il y a eu des propositions intéressantes pour franchir le fossé (l'héritage par famille côté objet, dans Beta, par exemple; les variantes polymorphes côté fonctionnel, par exemple). "Résoudre le problème" en utilisant le moins de fonctionnalités avancées possibles (mais ça ne veut pas dire que la solution est simple) reste un sport très apprécié, qui génère des idées utiles—les object algebras par exemple.

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 ?

La réponse un peu triviale c'est que je ne fais pas souvent ça¹. Dans mes cas d'usages personnels on peut souvent revenir éditer la définition initiale. Le problème d'extensibilité des données et opérations (parfois connu sous le nom de "Expression problem" qui est assez peu clair, "Extensibility problem" est un nom plus ancien et plus clair) est intéressant et important, mais pour moi c'est un peu comme la récursion ouverte, ou d'ailleurs les GADTs: moins on en a besoin, plus on peut faire simple, mieux on se porte. Dans les programmes que j'ai eu l'occasion d'écrire, j'ai eu la chance de pouvoir toujours utiliser des approches plus simples.

¹: Si je voulais vraiment faire ça sans fonctionnalité avancée j'envisagerais d'avoir une définition du type de départ en style "récursion ouverte", avec un constructeur "la suite" qui est paramétré, pour pouvoir faire l'extensibilité après-coup. Ça marche mais c'est assez inélégant à l'usage, puisque si on fait deux couches d'extension il faut traverser deux constructeurs "la suite" et il y a des paramètres dans tous les coins. De plus pour faire ça avec les GADTs il faut abstraire sur un type paramétré, donc un foncteur, ça peut vite devenir lourd aussi.

Après le fait d'avoir plusieurs définitions de données différentes mais proches et liées entre elles (sous-ensembles image de traductions, etc.), qui est aussi bien résolu par les variantes polymorphes, se pose plus souvent dans ma "vraie vie", par exemple quand on écrit des compilateurs c'est typique, et encore plus avec les approches "Nanopass" qui sont assez populaires (Scheme, Scala), avec plein de passes qui touchent seulement une construction ou deux. Souvent les gens utilisent de la métaprogrammation pour faire ça (fonctions de traversée auto-générées, etc.), au lieu d'essayer d'avoir cette modularité dans le langage (à quel coût à l'utilisation ?).

Je suis intéressé par vos retours sur le sujet, vos constats, vos ressentis, vos éventuelles pistes d'amélioration, etc., ici ou en privé par courriel (oumph CHEZ linuxfr.org) si vous préférez.

Merci, je t'écrirai sans doute un mail quand j'aurai un peu de temps pour réfléchir à ça. (Un journal ça va aussi, dans le sens où il n'y a rien de privé, mais je pense qu'un mail pour commencer c'est mieux.)

(message au mauvais endroit)

C'est une déviation intéressante, merci ! Ce sont des sujets assez délicats que personne ne comprend vraiment bien (sinon il n'y aurait pas de recherche active là-dessus; le principe de la recherche c'est souvent une discussion active sur des questions que personne ne comprend vraiment bien, même si des gens comme Oleg peuvent donner l'impression d'avoir des avis très arrêtés).

Pour ma part je me méfie un peu de la complexité des encodages finaux. C'est très rigolo et assez excitant, mais personnellement je perds facilement le fil, et je ne sais plus forcément ce qui est vraiment mieux qu'avec une approche initiale (par structures de données concrètes), ce qui est plutôt une reformulation de la même chose, et ce qui ne va pas bien ou moins bien marcher et que je ne vois pas forcément. Ça n'est pas une critique de l'approche, et encore moins du fait d'expérimenter avec, c'est salutaire.

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).

¹: tiens ce serait pratique si on pouvait afficher une adresse email dans on profil…

Je pense qu'en un sens la réponse est oui, et d'ailleurs Oleg a aussi une bibliothèque en Haskell qu'il appelle tagless staged et qui utilise cette idée-là. Mais le résultat est assez compliqué, je trouve qu'on perd un peu en simplicité par rapport à un outil construit sur des primitives claires comme MetaOCaml.

(La réduction du code spécifique à MetaOCaml permet aussi d'envisager de l'intégrer un jour dans le langage OCaml. 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.)