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

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.