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

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.