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

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.