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

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.