Re: chaud

Je vais essayer de présenter la chose autrement, avec le langage de base sur les entiers :

module type SYM_INT = sig
 type 'a repr
 type 'a obs
 val lit : int -> int repr
 val add : int repr -> int repr -> int repr
 val mul : int repr -> int repr -> int repr
 val observe : 'a repr -> 'a obs
end

Maintenant, si je définis un terme du langage via un foncteur paramétré par une interprétation, j'obtiens cela :

module T (I : SYM_INT) = struct
 open I
 let t = mul (add (lit 1) (lit 2)) (add (lit 3) (lit 4))
end;;
module T : functor (I : SYM_INT) -> sig val t : int I.repr end

En donnant une interprétation au foncteur, on obtient un terme de type int I.repr. On voit déjà comment la combinaison de la signature et du système de type de OCaml donne un type correcte à notre terme. La signature, d'une certaine façon, exprime les règles de typage de notre langage.

Ensuite, je ne sais si mon image est adaptée mais elle peut aider, on peut voir un module d'interprétation (qui implémente cette signature) comme un VM pour ce langage. Le foncteur T permet d'écrire un code, un programme, dans ce langage via le terme t. Puis lorsqu'on lui donne une VM, il exécute le programme et on obtient à l'arrivée le résultat t pour cette VM.

Dans cette façon de voir, on pourrait regarder les foncteurs d'optimisations comme un processus construisant une VM à partir d'une autre VM tout en préservant des invariants de la « sémantique » du langage.

Pour ta dernière remarque :

la génération est "refaite" à chaque type d’interprétation (eval ou pretty print)

J'ai envie de dire : comme avec l'approche par ADT ou GADT. Dans celles-ci, un programme est représenté par une structure de données (et non par un foncteur) et la génération d'une interprétation est refaite à chaque fois que l'on fait un fold dessus.

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