Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?

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 :

let lam f = .<fun x -> .~(f .<x>.)>.
let app e1 e2 = .<.~e1 .~e2>.

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 : 'a from -> 'a repr
 | Sta : 'a * 'a from -> 'a repr
 | Fun : ('a repr -> 'b repr) -> ('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 *)
let lam f = .<fun x -> .~(f .<x>.)>.
(* pour la branche du cas fonctionnel dans `bwd` *)
Fun f -> I.lam (fun x -> bwd (f (fwd x)))

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.

Je donnais un exemple de code du genre :

let fois n = fun verbe cod -> for i = 1 to n do verbe cod done
let ecrire = print_endline
(fois 5) ecrire "coin< coin<"

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.