kantien a écrit 1189 commentaires

Ok, merci pour l'explication, c'est plus clair maintenant.
Une autre question : peut-on avoir plusieurs clefs associées à la même adresse ? Si oui, quelle utilité ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Merci pour ce journal riche en information. N'étant pas utilisateur du système certains points m'échappent encore, mais j'en ai déjà une meilleure compréhension grâce au journal.

J'ai une question sur la politique ask du modèle TOFU : comment l'active-t-on ? Tu dis que les seules politiques par défaut possibles sont unknowkn, auto ou good; mais alors à quoi sert la politique ask ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Pour la résistance, j'ai eu un peu de mal à voir la meilleur analogie : c'est une voix plus "étroite" ? il faut plus de tension pour faire passer plus de courant ?

La meilleure analogie ne serait-elle pas sa propre définition : un frottement ? Il me semble bien que la loi U = R . I n'est que la forme intégrale d'une loi différentielle qui exprime le frottement que subit la charge en traversant le conducteur. Pour l'analogie avec l'intensité du courant comme débit (la vitesse de déplacement des charges dans le milieu) par rapport à la gravitation : prendre une bille de plomb est la lâcher dans l'air, puis comparer avec la même expérience où elle doit traverser un milieu visqueux comme de la confiture. Dans la seconde elle ira moins vite, l'intensité est plus faible bien que la tension soit la même (même hauteur de chute, même différence de potentiel gravitationnel) car la résistance du milieu est plus grande.

Après avec la gravitation, il y a ce résultat marrant : en l'absence de frottement (dans le vide) une plume de 1g et un poids de 1kg tombe au sol en même temps si on les lâche de la même hauteur avec la même impulsion. Résultat bien connu depuis Galilée, qui est le point de départ de la théorie de la gravitation d'Einstein, mais que la plupart des personnes ont du mal à accepter. Je me souviens d'une série d'articles du Canard Enchaîné où les auteurs s'évertuaient à vouloir prouver le contraire, sans jamais réussir à comprendre qu'ils expérimentaient la résistance de l'air et non une propriété physique du champ de gravitation.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Effectivement, la coquille se trouve dans l'article d'origine de Gérard Berry, je n'ai pas relu attentivement la phrase (sachant ce qu'elle cherchait à exprimer) en citant. Mais c'est une bonne chose au final, cela illustre une source potentielle de bug dans la démarche : lorsque l'humain traduit formellement la spécification du langage. Ce qui minimise grandement la surface. Il suffit de lire les deux articles cités dans ce commentaire : 4 erreurs minimes trouvées et corrigées pour CompCert face à des centaines, non toutes corrigées, pour GCC et LLVM. :-)

Pour la note de modérateur à rajouter sur la correction, je ne sais si elle est vraiment nécessaire. Quoi que la source a une clause ND : un correction de coquille est-elle une œuvre dérivée ? :-P

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Ces dernières années, différents bugs ont été trouvés dans CompCert par test aléatoire (PLDI'11, ISSTA'15, peut-être d'autres, je ne suis pas expert), vraisemblablement causés par des "trous" dans la spécification.

Effectivement, mais cela a été corrigé. Je ne suis pas rentré dans les détails dans le journal, mais Gérard Berry en parle dans sa présentation dont le lien est dans le journal (il y parle aussi du projet deepspec) :

L’importance de CompCert devient claire quand on regarde d’autres projets comme l’outil Csmith développé à l’université d’Utah, qui, à l’aide de techniques de génération aléatoire, a permis d’engendrer automatiquement un million de programmes C destinés à casser les compilateurs. Le résultat a été étonnant : Csmith a permis de détecter des centaines de bugs dans les principaux compilateurs C, mais aucun dans CompCert (en fait deux au début, mais pas dans les parties bien définies de C, et ces bugs ont ensuite été corrigés).

En ce qui concerne les approches formelles :

On retombe un peu sur l'idée que les approches formelles supposent souvent un monde qui n'est pas la réalité.

Cette remarque s'applique inéluctablement à la conception de matériel qui repose sur des théories physiques qui sont une modélisation de la réalité. Comment prouver que le modèle « correspond » au réel ? Et d'ailleurs quel sens pourrait bien avoir une telle question ?

Pour ce qui est de la formalisation de processus de calcul, ce n'est pas le cas. Mais on peut tomber sur d'autres problématiques ironiquement bien formulées dans cet article :

1973 - Robin Milner creates ML, a language based on the M&M type theory. ML begets SML which has a formally specified semantics. When asked for a formal semantics of the formal semantics Milner's head explodes.

Robin Milner est un des pères fondateurs de la discipline dans laquelle travaille Xavier Leroy : la preuve mathématique assistée par ordinateur. Le langage OCaml est un langage de la famille ML, et tous les langages de cette famille (avec SML, OCaml, Haskell, Coq, Idris…) sont tous fondés sur la correspondance de Curry-Howard ou correspondance preuve-programme : un programme est une preuve d'un théorème mathématique et son type est l'énoncé du théorème.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je vais essayer de présenter la chose autrement, avec le langage de base sur les entiers :

module type SYM_INT = sig
  type 'a repr
  type 'a obs

  val lit : int -> int repr
  val add : int repr -> int repr -> int repr
  val mul : int repr -> int repr -> int repr

  val observe : 'a repr -> 'a obs
end

Maintenant, si je définis un terme du langage via un foncteur paramétré par une interprétation, j'obtiens cela :

module T (I : SYM_INT) = struct
  open I
  let t = mul (add (lit 1) (lit 2)) (add (lit 3) (lit 4))
end;;
module T : functor (I : SYM_INT) -> sig val t : int I.repr end

En donnant une interprétation au foncteur, on obtient un terme de type int I.repr. On voit déjà comment la combinaison de la signature et du système de type de OCaml donne un type correcte à notre terme. La signature, d'une certaine façon, exprime les règles de typage de notre langage.

Ensuite, je ne sais si mon image est adaptée mais elle peut aider, on peut voir un module d'interprétation (qui implémente cette signature) comme un VM pour ce langage. Le foncteur T permet d'écrire un code, un programme, dans ce langage via le terme t. Puis lorsqu'on lui donne une VM, il exécute le programme et on obtient à l'arrivée le résultat t pour cette VM.

Dans cette façon de voir, on pourrait regarder les foncteurs d'optimisations comme un processus construisant une VM à partir d'une autre VM tout en préservant des invariants de la « sémantique » du langage.

Pour ta dernière remarque :

la génération est "refaite" à chaque type d’interprétation (eval ou pretty print)

J'ai envie de dire : comme avec l'approche par ADT ou GADT. Dans celles-ci, un programme est représenté par une structure de données (et non par un foncteur) et la génération d'une interprétation est refaite à chaque fois que l'on fait un fold dessus.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je ne sais pas trop, je ne suis que le messager et je ne connais pas les entrailles du système. Sur le site du projet, à la page consacrée à son fonctionnement, on peut y lire :

The subset of C supported

CompCert C supports all of ISO C 99, with the following exceptions:

• switch statements must be structured as in MISRA-C; unstructured "switch", as in Duff's device, is not supported.
• longjmp and setjmp are not guaranteed to work.
• Variable-length array types are not supported.

Consequently, CompCert supports all of the MISRA-C 2004 subset of C, plus many features excluded by MISRA (such as recursive functions and dynamic heap memory allocation).

Several extensions to ISO C 99 are supported:

• The _Alignof operator and the _Alignas attribute from ISO C2011.
• Pragmas and attributes to control alignment and section placement of global variables.

Je pense que cela parlera plus aux développeurs C qu'à moi-même. Et pour l'architecture, on trouve ce schéma :

De ce que j'ai compris, la certification commence après la traduction en Clight.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je ne suis pas certain de comprendre tes questions.

Est-ce le "code" est dupliqué pour chaque functor ?

Un foncteur c'est une fonction qui prend des modules comme paramètres et qui renvoie un module (qui pourrait lui-même être un foncteur d'ailleurs). Le système des modules avec ses foncteurs est au fond un langage fonctionnel mais non turing-complet, il est proche du lambda-calcul simplement typé (en). Qu'entends-tu par le code dupliqué pour chaque foncteur ? Il y aura de l'allocation à chaque application du foncteur, mais tout comme avec n'importe quelle application de fonction. Par exemple :

let f i = i + 1

let i = f 1
let j = f 2

ici, à chaque fois que l'on applique f on alloue de la mémoire pour stocker le résultat dans i et j. C'est pareil avec les foncteurs.

Mais dans le cas de "génération" d'une expression par lecture d'un fichier par exemple, il faut le faire pour chaque functor ?

Une expression c'est un terme d'un langage. Pour pouvoir l'interpréter, il faut le mettre dans un foncteur paramétré par un module d'interprétation, et en appliquant le foncteur tu obtiendras l'interprétation de ton choix.

Comment partager une expression qui n'est pas statique ?

Via la directive include. Par exemple si tu as un terme t, tu peux faire :

module T(I : SYM) = struct
  let t = (* la désérialisation de ton terme *)
end

Et si tu veux l'utiliser avec un autre terme t', tu fais :

module T' (I : SYM) = struct
  include T(I)
  let t' = (* expression qui comporte t *)
end

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je dois avouer que je n'ai jamais creusé la question. Mais les premières questions qui me viennent à l'esprit sont : comment le mot-clé where était-il géré avant sa disparition ? comment font-ils en Haskell ?

Ensuite pour ce qui relève de son intérêt et de son utilité : la construction est certes redondante avec la forme let res = let x = e1 in e2, mais d'un autre côté écrire let res = e2 where e2 = e3 permet de comprendre au premier coup d'œil où l'on veut en venir. C'est du même acabit que lorsque dans mon journal j'ai traité la question du pretty printing. En commençant par écrire la conclusion à laquelle je voulais arriver, il me semble plus simple de comprendre le développement qui s'ensuit. Tandis que si je n'avais pas procédé ainsi, le lecteur se serait sans doute demandé où je voulais en venir. C'est souvent ce qui m'arrive avec la forme let ... in lorsqu'elle sert à définir des termes auxiliaires : une fois arrivée à la fin, je dois reprendre la lecture pour comprendre.

Pour ce qui est de la gestion de la précédence : pourquoi ne pas mettre les let et where au même niveau et les voir comme une parenthèse ouvrante pour le premier et une parenthèse fermante pour le second ? Cela ne marche pas ? N'est-ce pas ce que tu as fait dans ton extension de syntaxe ?

Pour les cas que tu proposes, je les lis ainsi :

let x = y + 1 in 2 * x where y = 3
(* devient *)
let y = 3 in let x = y + 1 in 2 * x

let x1 = x2 + x3 where x2 = 1 and x3 = 2 in 2 * x1
(* devient *)
let x2 = 1 and x3 = 2 in let x1 = x2 + x3 in 2 * x1

Une petite précision terminologique : j'ai tendance à qualifier de syntaxique ce genre de problématique, et de réserver le qualificatif grammatical pour ce qui relève des problématiques de typage. Pour comparer avec le domaine de la physique, l'équation P = U * I² est syntaxiquement correcte mais grammaticalement erronée car il n'est pas possible d'unifier le deux membres de l'équation : ils n'ont pas la même unité de mesure; ce qui en fait une proposition vide de sens.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Merci pour ton commentaire.

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.

Effectivement, l'article est long et dense. Il faudra y revenir plus d'une fois pour les lecteurs qui voudraient le comprendre. Et encore, j'ai fait des coupes : au départ j'abordais la problématique de l'héritage multiple par exemple. J'ai hésité, également, à le couper en plusieurs journaux mais j'ai finalement choisi cette forme en me disant que le lecteur le lirai plus d'une fois.

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.

Je ne connaissais pas, j'y réfléchirai. Pour un tutoriel comme celui-ci, c'est sans doute une bonne idée.

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

Effectivement je me suis mal exprimé, je voulais bien dire que c'est l'inférence qui est indécidable dans le cas général pour les GADT. Vérifier la correction d'une preuve, c'est toujours décidable. Trouver une preuve, en revanche… ;-)

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

Merci pour la référence, je n'y avais pas pensé. Pourtant je me suis rendu plus d'une fois sur le site de Roberto Di Cosmo.

Au passage, une question qui n'a rien à voir avec le thème du journal. Sais-tu pourquoi les where statement ont disparu du langage OCaml ? Je pense à cela car dans le cours de Paris 7, il y a une leçon sur les zipper, et dans son article sur le sujet Gérard Huet en faisait usage. Je trouve cette perte dommage, cela permet d'écrire des codes plus élégants, et la beauté dans le code c'est important ! Comme il répondait dans un interview, sur le blog de la SIF (Société Informatique de France), intitulée Poésie et esthétisme du logiciel :

— Binaire : […] Mais tu as dépassé l’état de le compréhension. Tu nous parles d’esthétique : un programme informatique peut-il être beau ?

—Gérard Huet : Bien sûr. Son rôle est d’abord d’exposer la beauté de l’algorithme sous-jacent. L’esthétique, c’est plus important qu’il n’y paraît. Elle a des motivations pratiques, concrètes. D’abord, les programmes les plus beaux sont souvent les plus efficaces. Ils vont à l’essentiel sans perdre du temps dans des détails, des circonvolutions inutiles. Et puis un système informatique est un objet parfois très gros qui finit par avoir sa propre vie. Les programmeurs vont et viennent. Le système continue d’être utilisé. La beauté, la lisibilité des programmes est essentielle pour transmettre les connaissances qui s’accumulent dans ces programmes d’une génération de programmeurs à l’autre qui ont comme mission de pérenniser le fonctionnement du système.

Pour les programmes, de même que pour les preuves, il ne faut jamais se satisfaire du premier jet. On est content quand ça marche, bien sûr, mais c’est à ce moment là que le travail intéressant commence, qu’on regarde comment nettoyer, réorganiser le programme, et c’est souvent dans ce travail qu’on découvre les bonnes notions. On peut avoir à le réécrire tout ou en partie, l’améliorer, le rendre plus beau.

Et je suis bien d'accord avec lui : un théorème vrai, c'est important. Mais une belle démonstration l'est tout autant ! Elle permet de mieux saisir les raisons profondes de la vérité du résultat et d'éclairer son harmonie sous-jacente.

On est accoutumé à nommer beauté les propriétés évoquées des figures géométriques aussi bien que des nombres […] C'est bien plutôt une démonstration de telles propriétés que l'on serait en droit de nommer belle, parce que, par son intermédiaire, l'entendement comme pouvoir des concepts et l'imagination comme pouvoir de leur présentation a priori se sentent renforcés (ce qui, combiné avec la précision que donne la raison, se nomme l'élégance de la démonstration); car, en tout ceci, du moins la satisfaction, bien que le fondement s'en trouve dans des concepts, est-elle subjective, tandis que la perfection implique une satisfaction objective.

Kant, Critique de la faculté de juger.

Et comme les programmes sont des preuves. :-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Avant tout je voudrais te remercier pour ce super journal, instructif et très pédagogique (ce qui a certainement demandé beaucoup de temps de ta part).

De rien. Cela m'a demandé effectivement du temps, mais il me fut avant tout profitable à moi même. En vertu du principe : « ce qui se conçoit bien, s'explique bien », il me fallait d'abord bien comprendre la méthode pour pouvoir l'expliquer. Ensuite, s'il peut être utile aux lecteurs du site : c'est du bonus, et c'est pour cela que je partage ma compréhension de la technique.

Une modeste contribution pour la curryfication (il faut voir si c'est instructif ou non).

Ton explication est tout à fait correcte, et elle code un principe général de curryfication pour des fonctions sur des couples. Elle explicite un isomorphisme (du moins un des sens) entre les fonction sur des couples et leurs versions curryfiées. C'est au fond ce que l'on fait en mathématique lorsque l'on pratique des applications partielles sur des fonctions de deux variables en en fixant une et en faisant varier la seconde.

Après j'ai choisi l'approche de comparaison avec python pour ne pas trop rentrer dans des détails formels sur le principe de la curryfication. Ce passage était surtout là pour montrer qu'en rendant le contexte explicite, via la curryfication, alors on pouvait se ramener au cas d'un fold ce qui est nécessaire pour utiliser la technique tagless final. Cette question avait amené de long échanges entre toi et Nicolas Boulay dans ton journal, c'est pour cela que je voulais la traiter. D'autant que j'avais besoin du code obtenu pour la suite du journal. L'exemple du pretty printing est d'ailleurs emprunté à la vidéo de ton journal. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Oui, un fichier pour chaque exemple, bien séparer. Pour pouvoir comparer les évolutions et les différences. Genre je suis bloqué sur le fold appliquée aux parenthèses, mais je bloque surtout sur le principe de précédence, plus que sur le code.

Je vais voir ce que je peux faire pour mettre du code plus détaillé et commenté sur github. Je ne te promets rien, cela dépendra de mon temps libre.

Pour le principe de précédence qu'est-ce qui te pose problème ? On a d'abord une fonction de mise entre parenthèse sous condition :

let cparen b = if b then paren else (fun s -> s);;
val cparen : bool -> string -> string = <fun>

Elle permet de retourner une fonction de type string -> string selon la valeur du booléen : soit cette fonction met des parenthèses si b = true, sinon c'est l'identité et on ne met pas de parenthèses. Ensuite pour le cas de l'addition, on a :

let add x y = fun p -> cparen (p > 3) @@ show_add (x 3) (y 4)

Autrement dit, tant que la priorité du contexte est ≤ 3 on ne met pas de parenthèse : 3 représente le degré de priorité de l'opérateur additif. Ensuite comme l'addition est associative à gauche, pour le membre de gauche on reste au degré 3 de l'addition, par contre pour le membre de droite on passe au degré suivant. C'est pour distinguer 1 + 2 + 3 == ((1 + 2) + 3) de 1 + (2 + 3) == (1 + (2 + 3)). Pour la multiplication, son degré de priorité est de 4 : la multiplication est prioritaire sur l'addition.

Cela étant, c'est plus un code « standard » pour gérer la priorité des opérateurs en programmation fonctionnelle. Si tu ne vois pas trop pourquoi il fait ce qu'on lui demande, ce n'est pas très important pour le reste du journal.

Mais pourquoi ?! En objet, c'est simplement une injection. Un composant d'un objet qui est construit à l’extérieur de celui-ci et donné en paramètre au constructeur. En quoi instancier un module en fixant un des type paramètre en fait une fonction ?

J'ai du mal à comprendre où tu veux en venir, et je me suis peut être mal exprimé. Les implémentations de la signature d'un langage corresponde aux différentes interprétations du dit langage. Les foncteurs eux servent à écrire du code dans ses langages (comme les foncteurs d'exemples) ou à transformer les dits programmes (comme les optimiseurs). Pour moi, et comme l'a dit Thomas Douillard, c'est exactement le niveau d'abstraction qu'il me faut pour raisonner sur ce genre de problématique.

Depuis que j'ai découvert cette méthode, et également suite aux discussions sur le journal de présentation de MetaOCaml, il y a deux comics xkcd qui résument bien mon état du moment :

et celui-ci :

J'ai essayé d'éviter le plus possible le recours au vocabulaire et aux concepts abstraits des mathématiques, mais ce n'est pas toujours évident.

Pour ce qui est de l'approche final avec les objets de OCaml cela pourrait ressemblait au code suivant :

(* on définit la symantique d'un langage avec litéraux
 * et addition comme un type d'objet paramétré par son interprétation *)
class type ['repr] symAdd = object
  method lit : int -> 'repr
  method add : 'repr -> 'repr
end

(* là on a des fonctions pour créer nos termes
 * du langage à partir de ses implémentations *)
let lit n = fun ro -> ro#lit n
let add x y = fun ro -> ro#add (x ro) (y ro)

(* un terme d'exemple *)
let t1 () = add (lit 1) (add (lit 2) (lit 3))

(* on implémente deux interprétations *)
class eval = object
  method lit n = (n:int)
  method add x y = x + y
end

class view = object
  method lit n = string_of_int n
  method add x y = "(" ^ x ^ " + " ^ y ^ ")"
end

(* on instancie un objet pour chacune *)
let eval = new eval
let view = new view

(* notre exemple est une fonction qui prend une
 * instance de classe, à la manière d'un foncteur *)
t1 () eval;;
- : int = 6

t1 () view;;
- : string = "(1 + (2 + 3))"

Et pour étendre les langages, par exemple en rajoutant la multiplication, on fait de l'héritage entre objets :

(* on ajoute un opérateur aux langages *)
class type ['repr] symMul = object
  method mul : 'repr -> 'repr -> 'repr
end

(* la nouvelle fonction pour écrire nos termes *)
let mul x y = fun ro -> ro#mul (x ro) (y ro)

(* on étend par héritage nos précédents interprètes *)
class evalM = object
  inherit eval
  method mul x y = x * y
end

class viewM = object
  inherit view
  method mul x y = "(" ^ x ^ " * " ^  y ^ ")"
end

(* on les instancie *)
let evalM = new evalM
let viewM = new viewM

(* un exemple de test *)
let t2 () = mul (add (lit 1) (lit 2)) (add (lit 3) (lit 4))

t2 () evalM;;
- : int = 21

t2 () viewM;;
- : string = "((1 + 2) * (3 + 4))"

Cette façon de faire est plus proche de l'encodage en Haskell via les typeclasses.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

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 (h x))

(* comme dans ce bout de code issu du journal *)
let lam f = fwd @@ I.lam @@ fun x -> bwd (f (fwd x))

(* que j'aurai pu tout aussi bien écrire *)
let lam f = fwd (I.lam (fun x -> bwd (f (fwd x))))

(* ou encore avec plus de @@ *)
let lam f = fwd @@ I.lam @@ fun x -> bwd @@ f @@ fwd x

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 :

module type F = S1 -> S2
(* ou S1 et S2 sont des signatures de modules *)

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

J'ai encore mal au cerveau.

Désolé. :-P

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 :

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.

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.

Et de fait j'en ai un : la fonction observe. ;-)

Il y a un ancêtre commun à tous les Eval :

module EvalCommon = struct
  type 'a repr = 'a
  type 'a obs = 'a
  let observe (x :'a repr) : 'a obs = x
end

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 :

let open Eopt in
let (+) = add in
lam @@ fun x -> lam @@ fun y -> lit 1 + lit 2 + x + lit 3 + lit 4 + y + lit 5 + lit 6;;
- : (int -> int -> int) Eopt.repr = 
 Eopt.OptM.X.Unk (ReduceAddHO(Static(SuppressZeroHO(E))).OptM.X.Dyn
  (Static(SuppressZeroHO(E)).OptM.X.Fun <fun>))

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 :

   e-------f
  /|      /|
 / |     / |
a--|----b  |
|  g----|--h
| /     | /
c-------d

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 :

let f = 
  let open Eopt in
  let (+) = add in
  observe @@ lam @@ fun x -> lam @@ fun y -> 
    lit 1 + lit 2 + x + lit 3 + lit 4 + y + lit 5 + lit 6

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 :

type 'a expr =
  | Bool : bool -> bool expr
  | If : bool expr * (unit -> 'a expr) * (unit -> 'a expr) -> 'a expr
  | Lam : ('a expr -> b' expr) -> ('a -> 'b) expr
  | App : ('a -> b') expr * 'a expr -> 'b expr

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 :

module type SymAddHO = sig
  include SymHO
  val lit : int -> int repr
  val add : int repr -> int repr -> int repr
end

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 :

module ReduceAddPass (F : SYM_ADD) = struct
  (* blabla *)
end

mais je l'utilise sur un module de signature SYM_ADD_COND_HO qui étend celle-ci :

module type SYM_ADD_COND = sig
  include SYM_ADD
  include SYM_COND 
    with type 'a repr := 'a repr
    and type 'a obs := 'a obs
  val eq : 'a repr -> 'a repr -> bool repr
  val lt : int repr -> int repr -> bool repr
end

module type SYM_ADD_COND_HO = sig
  include SYM_ADD_COND
  val lam : ('a repr -> 'b repr) -> ('a -> 'b) repr
  val app : ('a -> 'b) repr -> 'a repr -> 'b repr
end

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 :

let open Eopt in
let (+) = add in
lam @@ fun x -> lam @@ fun y -> lit 1 + lit 2 + x + lit 3 + lit 4 + y + lit 5 + lit 6;;
- : (int -> int -> int) Eopt.repr

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 *)
module E = EvalAddCondHO
module S = ShowAddCondHO

(* je les passe dans une chaîne d'optimisations *)
module Sopt = LinearizeAddHO(Static(SuppressZeroHO(S)))
module S1opt = LinearizeAddHO(ReduceAddHO(Static(SuppressZeroHO(S))))
module Eopt = 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 ;-) *)
let open Sopt in
let (+) = add in
observe @@ lam @@ fun x -> lam @@ fun y -> lit 1 + lit 2 + x + lit 3 + lit 4 + y + lit 5 + lit 6;;
- : 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 *)
let open S1opt in
let (+) = add in
observe @@ lam @@ fun x -> lam @@ fun y -> lit 1 + lit 2 + y + lit 3 + lit 4 + x + lit 5 + lit 6;;
- : string = "Lx. Ly. 3 + (y + (7 + (x + 11)))"

(* Ainsi la fonction renvoyer par Eopt fait ce que le code écrit au-dessus dit *)
let open Eopt in
let (+) = add in
observe @@ lam @@ fun x -> lam @@ fun y -> lit 1 + lit 2 + y + lit 3 + lit 4 + x + lit 5 + lit 6;;
- : int -> int -> int = <fun>

(* le code exécuté est fun x y -> 3 + (y + (7 + (x + 11))) *)
let open Eopt in
let (+) = add in
(observe @@ lam @@ fun x -> lam @@ fun y -> lit 1 + lit 2 + x + lit 3 + lit 4 + y + lit 5 + lit 6) 10 11;;
- : int = 42 (* \o/ *)

(* avec une application partielle *)
let open S1opt in
let (+) = add in
observe @@ app (lam @@ fun x -> lam @@ fun y -> lit 1 + lit 2 + y + lit 3 + lit 4 + x + lit 5 + lit 6) (lit 10);;
- : 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 :

module ReduceAddPass (F : SYM_ADD) = struct
  module X = struct
    type 'a from = 'a F.repr
    type 'a term =
      | Dyn : 'a from -> 'a term
      | Stv : (int * int from ) -> int term
      | Add : (int term * int term) -> int term
    let fwd x = Dyn x
    let rec bwd : type a. a term -> a from = function
      | Dyn x -> x
      | Stv (_,x) -> x
      | Add (x,y) -> F.add (bwd x) (bwd y)
  end
  open X
  module IDelta = struct
    let lit n = Stv (n, F.lit n)

    (* le principe est là : dès que deux valeurs
     * statiques se suivent on calcule statiquement *)
    let add : int term -> int term -> int term = fun x y ->
      match x,y with
      | 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)
  end
end

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 :

let lam2 f = lam @@ fun x -> lam @@ fun y -> f x y
let lam3 f = lam @@ fun x -> lam @@ fun y -> lam @@ fun z -> f x y z

let app2 f x y = app (app f x) y
let app3 f x y z = app (app (app f x) y) z

observe @@ lam2 @@ fun x y -> lit 1 + x + lit 3 + lit 4 + y + lit 5;;
- : string = "Lx. Ly. 1 + (x + (7 + (y + 5)))"

observe @@ app2 (lam2 @@ fun x y -> lit 1 + x + lit 3 + lit 4 + y + lit 5) (lit 14) (lit 15);;
- : string = "42" (* \o/ *)

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 :

module type SymHO = sig
  type 'a repr
  type 'a obs
  val bool_ : bool -> bool repr
  val if_ : bool repr -> (unit -> 'x) -> (unit -> 'x) -> ('a repr as 'x)
  val lam : ('a repr -> 'b repr) -> ('a -> 'b) repr
  val app : ('a -> 'b) repr -> 'a repr -> 'b repr
  val observe : 'a repr -> 'a obs
end

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.

module PE (F : SymHO) = struct
  (* on part d'une interprétation F du langage *)
  type 'a from = 'a F.repr
  (* on en construit une nouvelle qui évalue ce qui est statiquement connu *)
  type 'a repr =
    | Dyn : 'a from -> 'a repr (* la valeur est connue dynamiquement *)
    | Stv : ('a * 'a from) -> 'a repr (* elle est connue statiquement *)
    | Fun : ('a repr -> 'b repr) -> ('a -> 'b) repr (* c'est une fonction *)
  (* la sortie de l'interprète partiel est la même que celui de départ *)
  type 'a obs = 'a F.obs
  (* deux morphismes entre les domaines de représentations internes *)
  let fwd x = Dyn x
  let rec bwd : type a. a repr -> a from = function
    | Dyn x -> x
    | Stv (_,x) -> x
    | Fun f -> F.lam @@ fun x -> bwd @@ f (fwd x)

  (* un booléen est connu statiquement *)
  let bool_ 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 *)
  let if_ b te ee = match b with
    | Stv (b,_) -> if b then te () else ee ()
    | _ -> fwd @@ F.if_ (bwd b) (fun () -> bwd @@ te()) (fun () -> bwd @@ ee())

  (* pour les fonctions on les applique *)
  let lam f = Fun f
  let app f x = match f with
    | Fun f -> f x
    | _ -> fwd @@ F.app (bwd f) (bwd x)

  let observe x = F.observe (bwd x)
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 :

module Macro (I : SymHO) = struct
  open I
  let observe = observe
  let true_ = bool_ true
  let false_ = bool_ false
  let not_ b = if_ b (fun () -> false_) (fun () -> true_)
end

module Code (I : SymHO) = struct
  open I
  let observe = observe
  let app = app
  let true_ = bool_ true
  let false_ = bool_ false
  let not_ = lam @@ fun b -> 
    if_ b (fun () -> false_) (fun () -> true_)
end

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 *)
module M = Macro(ShowHO)
module C = Code(ShowHO)
module CPE = (PE(ShowHO))

(* la fonction not_ de M est une nouvelle primitive *)
M.not_;;
- : bool ShowHO.repr -> bool ShowHO.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.app C.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.app CPE.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.