Re: Reason

Euh... tagless final ou GADT c'est bonnet blanc et blanc bonnet ! ;-)

Regarde bien dans mon article à la fin de la première partie. Les types des constructeurs de mon GADT sont justement ceux que je donne ensuite aux fonctions d'interprétations.

L'idée derrière la méthode tagless final est la même que celle exposée dans l'article EDSL et F-algèbres d'Aluminium95 à la différence que j'utilise des modules et non des enregistrements. Les modules sont justes des enregistrements extensibles (objets) dopés aux stéroïdes.

Après je dois avouer que je ne comprends pas trop les spécifications de ton langage, mais il faudra bien que tu écrives un type checker (qui est une interprétation comme une autre des termes du langage). De ce que je crois comprendre de ton intention, ça me fait penser aux typages des modules et foncteurs en OCaml, c'est pour cela que je les évoquaient. Mais je me trompe peut être là-dessus.

Par exemple, quand tu écris :

Ainsi, tu écris 'int ~ 1 ~ Name "a"', pour définir un truc du nom de "a" qui est de type int et vaux 1. Cela permet de le composer en plusieurs fois.

N'y a-t-il pas un rapport avec ce code ?

module M : sig
 type t
 val a : t
end = struct
 type t = int
 let a = 1
end

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