Journal Découvrir MetaOCaml dans son navigateur

Posté par gasche le 12 novembre 2016 à 17:57. Licence CC By‑SA.

Étiquettes :

nov.

2016

Ce journal a été promu en dépêche : Découvrir MetaOCaml dans son navigateur.

OCaml est un langage de programmation généraliste, fonctionnel et statiquement typé.

MetaOCaml est une extension, un dialecte non-standard du langage qui a une longue histoire. Dérivée de MetaML il y a environ 15 ans, c'est toujours resté un prototype de recherche, avec une base d'utilisateur petite mais active au fil des années—au contraire de la plupart des prototypes de recherche qui meurent de mort naturelle assez vite. Le "Meta" dans le nom fait référence à la méta-programmation, l'écriture de programmes qui manipulent de programmes, et MetaML et MetaOCaml sont dans la catégorie de la méta-programmation "étagée" (staged), où il y a un nombre arbitraire de "niveaux d'exécution" qui construisent des morceaux de programme des niveaux précédents et les font tourner. (Par opposition il y a des langages où il y a un nombre fixe de niveau, par exemple "statique / à la compilation" et "dynamique / à l'exécution", comme en C++ ou D, beaucoup de langage à "macros" où la méta-programmation se résume à une passe de récriture de code, et des langages où la notion de niveaux est plus floue et plus complexe, et est combinée avec des récritures syntactiques de nature un peu différente et moins structurée, comme en Scheme, Lisp ou Racket).

Une façon de penser à MetaOCaml, c'est que c'est un langage pour décrire des optimisations de la forme "et si on spécialise comme-ci ou comme-ça à la compilation, on peut obtenir du super code au final", mais où la distinction entre ce qui est spécialisé "à la compilation" et ce qui est exécuté au final est explicite, elle ne repose pas sur l'intelligence du compilateur mais sur des marqueurs explicites insérés par le programmeur ou la programmeuse. (Il y eu beaucoup de recherche sur l'évaluation partielle comme super-optimisation, et le consensus de la communauté c'est que c'est puissant mais trop fragile / difficile à prévoir pour qu'on puisse laisser le compilateur le faire sans guidage humain).

Un récent exemple d'utilisation de la technique est Stream Fusion, to Completeness, un article qui utilise cette forme de méta-programmation pour optimiser des programmes décrivants des manipulants de flôt de données, avec une version en OCaml (utilisant MetaOCaml) et une version en Scala (utilisant "LMS", Lightweight Modular Staging, une autre approche de la méta-programmation par étage), et qui implémentent comme une librairie des optimisations puissantes de "fusion" qui sont traditionellement espérées du compilateur. (Ce travail va être présenté à Paris en janvier 2017, puisque les universités Paris 6 et Paris 7 accueillent et organisent cette année une des principales conférences de recherche en langages de programmation, et d'ailleurs si vous êtes étudiants et que vous voulez y aller et manger sur place mais pas payer les frais d'inscriptions vous pouvez vous proposer comment volontaire pour aider.)

Ne nous laissons pas distraire. Le sujet de ce journal c'est un cours sur MetaOCaml disponible en ligne, créé par Jeremy Yallop à l'université de Cambridge, C'est une sous-partie du cours Advanced Functional Programming, qui s'adresse à des gens connaissant déjà la programmation fonctionnelle mais pas forcément ses aspects les plus avancés. La partie sur MetaOCaml est à la fin, et elle est disponible (comme le reste) sous la forme de cahiers interactifs dans le navigateur (ça utilise IOCamlJS, un noyau IPython/Jupyter pour OCaml):

Voilà, bonne lecture.

# Tagless final un chemin vers MetaOCaml en bibliothèque ?

Posté par kantien le 12 novembre 2016 à 23:14. Évalué à 1. Dernière modification le 12 novembre 2016 à 23:17.

Tout d'abord merci pour ce journal et le lien vers la présentation de Jeremy Yallop. Ça va me faire de la lecture. :-)

J'ai une question à te poser. Il me semble que le développeur principal de MetaOCaml, et qui a repris le projet, est Oleg Kiselyov. J'ai cru lire sur son site qu'il avait grandement réduit la quantité de code qui le sépare du compilateur standard, et qu'il espère un jour pouvoir en faire une simple bibliothèque plutôt qu'un dialecte.

J'ai justement un journal en cours d'écriture pour présenter la méthode tagless final pour plonger un langage en OCaml et faire de l'évaluation partielle sans passer par des variants pour représenter l'AST mais en utilisant des modules et des foncteurs. Bon, il va falloir que j'élague un peu parce que là j'ai un pavé. :-P

Depuis que je joue avec cette méthode, j'en suis venu à voir OCaml comme un langage de macros typés pour le langage objet ce qui permet de faire de la méta-programmation intéressante sur celui-ci ainsi que des passes d'optimisations simples à réaliser, indépendantes, modulaires et facilement composables. Au final je me demande si cette méthode n'ouvre pas la voie vers la possibilité de ramener MetaOCaml à une simple bibliothèque ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
- [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
  
  Posté par gasche le 13 novembre 2016 à 01:36. Évalué à 3.
  
  Je pense qu'en un sens la réponse est oui, et d'ailleurs Oleg a aussi une bibliothèque en Haskell qu'il appelle tagless staged et qui utilise cette idée-là. Mais le résultat est assez compliqué, je trouve qu'on perd un peu en simplicité par rapport à un outil construit sur des primitives claires comme MetaOCaml.
  
  (La réduction du code spécifique à MetaOCaml permet aussi d'envisager de l'intégrer un jour dans le langage OCaml. 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.)
  - [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
    
    Posté par kantien le 13 novembre 2016 à 10:53. Évalué à 3.
    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.
    - [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
      
      Posté par ZeroHeure le 13 novembre 2016 à 11:42. Évalué à 3.
      
      Dévie, dévie, c'est enrichissant!
      
      On est en train de transformer cette dépêche en journal (lapsus : c'est le contraire!)
      Ça vous dirait de travailler dessus tous les deux ?
      
      "La liberté est à l'homme ce que les ailes sont à l'oiseau" Jean-Pierre Rosnay
      - [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par kantien le 13 novembre 2016 à 15:51. Évalué à 2.
        
        En fait, je vais arrêter là. Je me suis rendu compte, en réfléchissant plus, que je me suis fourvoyé. :-/
        
        Dans leur article, pour gérer les évaluations partielles ils utilisent deux techniques : les types fantômes et MetaOCaml. Mon exemple avec les GADT remplace l'utilisation des types fantômes. Cela n'a rien d'étonnant, ils ont été introduits en partie pour cela : on les appelle aussi first-class phantom type. Par contre MetaOCaml et son type ('a,t) code joue le rôle de mon interprète ShowHO de pretty printing. Donc que je n'ai pas besoin de MetaOCaml dans mon code est normal : j'utilise un autre interprète. :-P
        
        Pour ce qui est de faire une dépêche sur MetaOCaml, je ne le connais pas du tout, il faudrait que j'expérimente avec pour en savoir plus. Là la seule chose que je sache c'est le principe du dialecte : différer les calculs sous le contrôle du développeur (c'est proche des quote et unquote du LISP, il me semble).
        
        Pour exposer plus en détail l'approche tagless, j'ai un journal en préparation mais il faut que je restructure. J'ai deux textes de 900 lignes : un sous forme de fichier .ml avec du code commenté et illustrant le principe tant des extensions de langage via héritage multiple que les optimisations, un autre plus dans la forme d'un journal avec moins de code et comparant la méthode « classique » avec variant pour l'AST et la méthode tagless.
        
        Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par gasche le 13 novembre 2016 à 16:08. Évalué à 5.
        
        C'est une déviation intéressante, merci ! Ce sont des sujets assez délicats que personne ne comprend vraiment bien (sinon il n'y aurait pas de recherche active là-dessus; le principe de la recherche c'est souvent une discussion active sur des questions que personne ne comprend vraiment bien, même si des gens comme Oleg peuvent donner l'impression d'avoir des avis très arrêtés).
        
        Pour ma part je me méfie un peu de la complexité des encodages finaux. C'est très rigolo et assez excitant, mais personnellement je perds facilement le fil, et je ne sais plus forcément ce qui est vraiment mieux qu'avec une approche initiale (par structures de données concrètes), ce qui est plutôt une reformulation de la même chose, et ce qui ne va pas bien ou moins bien marcher et que je ne vois pas forcément. Ça n'est pas une critique de l'approche, et encore moins du fait d'expérimenter avec, c'est salutaire.
        
        J'attends ton journal avec curiosité (enfin bon je ne vais pas souvent sur LinuxFR où je ne me sens pas très bien, alors envoie-moi peut-être un mail¹ quand tu le publieras).
        
        ¹: tiens ce serait pratique si on pouvait afficher une adresse email dans on profil…
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par kantien le 14 novembre 2016 à 03:54. Évalué à 2.
        
        le principe de la recherche c'est souvent une discussion active sur des questions que personne ne comprend vraiment bien
        
        C'est pour ça que c'est intéressant ! Il faut bien que l'on finisse par comprendre. :-)
        
        je ne sais plus forcément ce qui est vraiment mieux qu'avec une approche initiale
        
        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 ? Il faut redéfinir une nouvelle structure de données et réécrire le code (c'est une des raisons pour laquelle MetaOCaml est un fork, il étend le type Parsetree de l'AST du langage OCaml). Il y a bien les variants polymorphes mais comparé à l'approche initiale avec GADT il n'y a pas de vérification de typage : il faut écrire un type checker. Là dans mon langage jouet ça va, il n'y a qu'un seul type — les booléens — mais si on rajoute les int il faut vérifier statiquement que le premier paramètre de if_ est bien un booléen.
        
        Avec l'approche finale on a de l'héritage multiple. Il suffit de définir différents sous-ensembles de langages, de construire le langage que l'on souhaite par héritage et on récupère tout le code de ses sous-langages. Dans mon journal en écriture j'ai trois langages : un avec des int, un autre avec des bool et un autre avec uniquement des fonctions (du pur lambda-calcul). Le langage jouet avec booléen et fonction est obtenu en combinant les deux derniers.
        
        C'est juste un niveau d'abstraction au-dessus, comme avoir des fonctions en tant que valeur comme les autres dans les langages fonctionnels par rapport aux langages qui n'en ont pas. D'ailleurs j'ai commencé à lire le cours de Jeremy, et sa deuxième leçon m'a donné une idée. Sa leçon consiste à utiliser MetaOCaml pour optimiser le code d'une stack machine implémentée avec des fonctions plutôt qu'un GADT.
        
        Avec l'approche final, on peut faire une chose similaire sans MetaOCaml. Je montrerai juste la sortie d'optimiseur que j'ai codé sur le langage complet qui hérite des trois dont j'ai parlé : entier, booléen et fonctions.
        
        (* là ce sont les deux interprètes classiques *) module E = EvalAddCondHO module S = ShowAddCondHO (* je les passe dans une chaîne d'optimisations *) module Sopt = LinearizeAddHO(Static(SuppressZeroHO(S))) module S1opt = LinearizeAddHO(ReduceAddHO(Static(SuppressZeroHO(S)))) module Eopt = LinearizeAddHO(ReduceAddHO(Static(SuppressZeroHO(E)))) (* le premier fait de l'application statique et linéarise l'addition * pour, par exemple, optimiser le calcul sur une stack machine ;-) *) let open Sopt 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;; - : string = "Lx. Ly. 1 + (2 + (y + (3 + (4 + (x + 11)))))" (* avec le second on peut simplifier le contenu de la pile comme dans la leçon de Jérémy *) let open S1opt in let (+) = add in observe @@ lam @@ fun x -> lam @@ fun y -> lit 1 + lit 2 + y + lit 3 + lit 4 + x + lit 5 + lit 6;; - : string = "Lx. Ly. 3 + (y + (7 + (x + 11)))" (* Ainsi la fonction renvoyer par Eopt fait ce que le code écrit au-dessus dit *) let open Eopt in let (+) = add in observe @@ lam @@ fun x -> lam @@ fun y -> lit 1 + lit 2 + y + lit 3 + lit 4 + x + lit 5 + lit 6;; - : int -> int -> int = <fun> (* le code exécuté est fun x y -> 3 + (y + (7 + (x + 11))) *) 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) 10 11;; - : int = 42 (* \o/ *) (* avec une application partielle *) let open S1opt in let (+) = add in observe @@ app (lam @@ fun x -> lam @@ fun y -> lit 1 + lit 2 + y + lit 3 + lit 4 + x + lit 5 + lit 6) (lit 10);; - : string = "Lx. 3 + (x + 28)" (* \o/ *)
        
        Avec l'approche finale les optimiseurs sont assez simples à coder, on ne les fait que pour la partie du langage qui nous importe (addition, structure de contrôle, fonction…) et on les reprend telle quelle pour tous les langages qui en héritent. Là je montre la passe pour réduire les additions en rentrant dans la pile :
        
        module ReduceAddPass (F : SYM_ADD) = struct module X = struct type 'a from = 'a F.repr type 'a term = | Dyn : 'a from -> 'a term | Stv : (int * int from ) -> int term | Add : (int term * int term) -> int term let fwd x = Dyn x let rec bwd : type a. a term -> a from = function | Dyn x -> x | Stv (_,x) -> x | Add (x,y) -> F.add (bwd x) (bwd y) end open X module IDelta = struct let lit n = Stv (n, F.lit n) (* le principe est là : dès que deux valeurs * statiques se suivent on calcule statiquement *) let add : int term -> int term -> int term = fun x y -> match x,y with | Stv(n,_), Stv(n',_) -> lit (n + n') | Add (x,Stv(n,_)), Stv (n',_) -> Add (x, lit @@ n + n') | Stv (n,_), Add (Stv(n',_),y) -> Add (lit (n + n'), y) | _, _ -> Add (x,y) end end
        
        Dans le fond on écrit le code des fonctions comme d'habitude, il faut juste les passer dans la fonction lam et on peut définir de macros pour simplifier l'écriture :
        
        let lam2 f = lam @@ fun x -> lam @@ fun y -> f x y let lam3 f = lam @@ fun x -> lam @@ fun y -> lam @@ fun z -> f x y z let app2 f x y = app (app f x) y let app3 f x y z = app (app (app f x) y) z observe @@ lam2 @@ fun x y -> lit 1 + x + lit 3 + lit 4 + y + lit 5;; - : string = "Lx. Ly. 1 + (x + (7 + (y + 5)))" observe @@ app2 (lam2 @@ fun x y -> lit 1 + x + lit 3 + lit 4 + y + lit 5) (lit 14) (lit 15);; - : string = "42" (* \o/ *)
        
        J'attends ton journal avec curiosité (enfin bon je ne vais pas souvent sur LinuxFR où je ne me sens pas très bien, alors envoie-moi peut-être un mail quand tu le publieras).
        
        Je vais essayer de le mettre au point dans la semaine. Je comprends que tu ne viennes pas souvent, l'ambiance est spéciale par moment. Si je ne te vois pas réagir au journal, je t'enverrai un mail.
        
        Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par Benoît Sibaud (site web personnel) le 14 novembre 2016 à 11:49. Évalué à 10.
        
        J'attends ton journal avec curiosité (enfin bon je ne vais pas souvent sur LinuxFR où je ne me sens pas très bien, alors envoie-moi peut-être un mail quand tu le publieras).
        
        Je vais essayer de le mettre au point dans la semaine. Je comprends que tu ne viennes pas souvent, l'ambiance est spéciale par moment. Si je ne te vois pas réagir au journal, je t'enverrai un mail.
        
        Je suis intéressé par vos retours sur le sujet, vos constats, vos ressentis, vos éventuelles pistes d'amélioration, etc., ici ou en privé par courriel (oumph CHEZ linuxfr.org) si vous préférez. Et merci pour vos contenus et commentaires à tous les deux.
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par gasche le 14 novembre 2016 à 16:27. Évalué à 2. Dernière modification le 14 novembre 2016 à 16:28.
        
        (message au mauvais endroit)
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par gasche le 14 novembre 2016 à 16:28. Évalué à 3.
        
        Je suis intéressé par vos retours sur le sujet, vos constats, vos ressentis, vos éventuelles pistes d'amélioration, etc., ici ou en privé par courriel (oumph CHEZ linuxfr.org) si vous préférez.
        
        Merci, je t'écrirai sans doute un mail quand j'aurai un peu de temps pour réfléchir à ça. (Un journal ça va aussi, dans le sens où il n'y a rien de privé, mais je pense qu'un mail pour commencer c'est mieux.)
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par benja le 14 novembre 2016 à 14:00. Évalué à 1. Dernière modification le 14 novembre 2016 à 14:02.
        
        Merci pour ces contributions intéressantes. Je vais essayer de mettre mon grain de sel en espérant être à propos ;-)
        
        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). Ce que tu peux faire avec ton approche, 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. Si j'ai bien compris, c'est grosso-modo le comportement de MO, avec la grosse différence que la vérification de typage sera postposée au run-time avec les problèmes qui en découlent, là où MO tente de valider la génération de code de tous les stages à la première compilation, au stage 0.
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par benja le 14 novembre 2016 à 14:13. Évalué à 1.
        
        PS: Pour en revenir à ta question, il me semble trivialement que si tu cherches à implémenter un langage, tu auras les mêmes problèmes (inhérents à ce langage) à résoudre quel que soit la technique utilisée. Mais j'avoue avoir mal compris le cheminement de votre discussion.
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par gasche le 14 novembre 2016 à 16:35. Évalué à 5. Dernière modification le 14 novembre 2016 à 16:36.
        
        kantien parle du problème de l'extensibilité, qui est de trouver des mécanismes de langage qui permettent d'étendre, de manière sure, un ensemble de types et d'opérations, mais sans modifier (ni dupliquer) les définitions existantes, en rajoutant uniquement du code pour définir de nouvelles versions étendues. Le folklore sur ce sujet est que le style fonctionnel typique permet d'étendre facilement les opérations (on définit une nouvelle fonction) mais pas les types (ce serait: rajouter des cas dans un type algébrique), alors que le style objet typique permet d'étendre les types (on rajoute une classe dérivée) mais pas les opérations.
        
        Dans les deux communautés il y a eu des propositions intéressantes pour franchir le fossé (l'héritage par famille côté objet, dans Beta, par exemple; les variantes polymorphes côté fonctionnel, par exemple). "Résoudre le problème" en utilisant le moins de fonctionnalités avancées possibles (mais ça ne veut pas dire que la solution est simple) reste un sport très apprécié, qui génère des idées utiles—les object algebras par exemple.
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par benja le 14 novembre 2016 à 17:24. Évalué à 2. Dernière modification le 14 novembre 2016 à 17:25.
        
        Merci pour ces précisions même si j'ai encore du mal à voir le rapport avec MetaOCaml. Il me semble que le papier "module mania" (qui est relativement vieux) parvient à résoudre ce problème dans le cas d'un interpréteur "dynamique", en utilisant une technique simple quoique verbeuse. On reste loin d'une solution compilée et sans faute de type au run-time.
        
        Je me demande naïvement s'il serait possible d'utiliser MetaOCaml pour l'implémentation d'un tel interpréteur afin de supprimer les injections/projections sur un type universel qui permettent l'extensibilité dans le cas de la solution de "Module Mania"¹, ou de rendre performant l'interpréteur de kantien².
        
        1: en fait j'ai réutilisé cet interpréteur (~~ Lua 2.0) pour un projet personnel et je m'étais posé la question, sans avoir le temps/compétence/motivation pour la tester sérieusement.
        2: dans lequel je ne retrouves pas la solution au problème d'extensibilité mais simplement des transformations/extensions d'AST pour faire des optimisations avec une conversion vers la représentation initiale utilisée par l'interpréteur. Ça permet de faire de l'extensibilité sur l'optimisation, donc sur les fonctions comme vous dites et non sur le type "valeur". J'ai du mal à voir une application concrète de cette technique de conversion bi-directionnelle car on peut baser l'évaluateur sur l'AST optimisé directement (vu qu'on n'a quand même pas d'extensibilité sur la valeur). Enfin soit.
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par gasche le 14 novembre 2016 à 17:43. Évalué à 3.
        
        Je me demande naïvement s'il serait possible d'utiliser MetaOCaml pour l'implémentation d'un tel interpréteur afin de supprimer les injections/projections sur un type universel qui permettent l'extensibilité dans le cas de la solution de "Module Mania"¹, ou de rendre performant l'interpréteur de kantien².
        
        Oui, ça me semble une piste à creuser (en particulier le fait que certaines fonctionnalités avancées de OCaml ne soit pas disponibles dans le code stagé n'est pas forcément un problème, tant qu'on peut les utiliser depuis le code qui génère le code: à priori tu peux utiliser des GADTs pour représenter tes programmes sans les utiliser ensuite pour dans l'interpréteur). L'important pour pouvoir utiliser MetaOCaml c'est que la représentation dont tu pars contiennes assez d'information pour pouvoir inspecter les sous-termes et obtenir toute l'information qu'on peut avoir "statiquement" (qui est connue en regardant la source de l'objet représenté).
        
        Dans ce cas MetaOCaml est à comparer avec la production d'une représentation intermédiaire pour la compilation; par exemple LLVM, mais aussi Malfunction, cf. précédent journal. D'ailleurs ce genre d'usage "staging" est justement le sujet d'un des exemples d'utilisation de Malfunction, examples/primrec.ml.
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par kantien le 14 novembre 2016 à 15:09. Évalué à 2.
        
        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.
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par benja le 14 novembre 2016 à 15:56. Évalué à 2.
        
        fonction de type int -> int -> int sous sa forme optimisée
        
        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
        2) de fait, tu as encore besoin d'un interprêteur, eval : 'a repr -> 'a.
        
        Ne te méprends pas sur mon commentaire, je trouve cette technique intéressante, de part justement du trade-off facilité d'implémentation vs performance inhérent à tout interpréteur. J'aime bien aussi utiliser les modules; 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.
        
        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).
        
        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. Malheureusement il n'y a pas de gadt (pas encore ?) dans MO donc tu devras t'en passer, idem au niveau des foncteurs ça risque d'être un peu plus compliqué; néanmoins ça serait intéressant que tu t'y essayes lors de ton expérimentation avec MO.
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par kantien le 14 novembre 2016 à 18:16. Évalué à 2.
        
        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.
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par benja le 14 novembre 2016 à 19:47. Évalué à 2.
        
        Mon instinct est que tu n'a pas compris le sujet. ;-)
        
        [ Tu finis par me le répèter gentillement à chacune de nos discussions. Ironiquement il y aurait au moins une chose que j'ai comprise avant que tu aies du me l'apprendre… Mais soit, je te laisse le loisir d'en douter aussi, juste pour la beauté d'atteindre le point méta ;-) ]
        
        Blague à part, tu as écris toi même que ton 'a repr était l'équivalent au 'a code de MO, ça ne devrait pas être si difficile que ça à faire, non ? Ok j'ai compris que tu ne relèveras pas ce défit, tant pis.
        
        Ma question reste : que ne peut-on pas faire avec l'approche tagless final qui nécessite le recours à MetaOCaml ?
        
        Profiter de l'optimisateur d'ocaml et d'un compilateur efficace qui ciblent du code machine ? Le unboxing implicite ?
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par gasche le 14 novembre 2016 à 20:10. Évalué à 4.
        
        Bon le plus simple serait que je compile un exemple en natif et que je ragarde le dump cmm sur un cas pour voir si le code de f est bien celui que je pense.
        
        Je ne pense pas, tu risques d'obtenir le code d'une fonction qui est extentionnellement égale, mais dont le graphe d'évaluation des fermetures pendant le calcul correspond à un évaluateur (du programme après évaluation partielle). Mais il faut tester !
        
        (Je trouve aussi que ta réponse à benja est trop sèche. C'est un sujet compliqué et c'est un peu normal que les gens se parlent un peu à travers.)
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par kantien le 15 novembre 2016 à 23:06. Évalué à 0.
        
        Je ne pense pas, tu risques d'obtenir le code d'une fonction qui est extentionnellement égale, mais dont le graphe d'évaluation des fermetures pendant le calcul correspond à un évaluateur (du programme après évaluation partielle). Mais il faut tester !
        
        Exact ! J'ai bien aussi tenté avec le unbox-closure de flamba pour voir s'il avait assez d'infos pour s'en sortir mais ça n'a rien donné.
        Quoi qu'il en soit ce n'est pas l'essentiel, ce qui m'intrigue c'est la ressemblance dans certains codages sur le plan syntaxique.
        
        Par exemple dans leur article, pour le code de leur compilateur (le module qui interprète la signature en ayant recours à MetaOCaml) pour lam et app on a :
        
        let lam f = .<fun x -> .~(f .<x>.)>. let app e1 e2 = .<.~e1 .~e2>.
        
        ce qui est au fond les fonctions back : ('a code -> 'b code) -> ('a -> 'b) code et forth : ('a -> 'b) code -> 'a code -> 'b code de la première leçon de Jeremy.
        
        De l'autre côté, pour traiter le cas statique dans la méthode tagless final (ce qui est au fond une automatisation du binding-time analysis de la lecon 2) il m'a fallu utiliser les types suivants :
        
        type _ repr = | Dyn : 'a from -> 'a repr | Sta : 'a * 'a from -> 'a repr | Fun : ('a repr -> 'b repr) -> ('a -> 'b) repr (* le type de back *)
        
        Avant d'arriver à ce choix, j'avais fait d'autres essais pour le cas des fonctions (dont un qui m'obligeait à utiliser l'option rectypes) mais rien ne fonctionnait. Il y a aussi le code correspondant :
        
        (* pour le compilateur en MetaOCaml *) let lam f = .<fun x -> .~(f .<x>.)>. (* pour la branche du cas fonctionnel dans `bwd` *) Fun f -> I.lam (fun x -> bwd (f (fwd x)))
        
        ce qui montre une similitude d'usage entre quote et escape d'un côté, puis bwd et fwd de l'autre.
        
        Ensuite, dans le cadre de la correspondance de Curry-Howard, il semblerait que pour typer une fonction similaire au quote du LISP il faille recourir à l'axiome du choix ou une de ses variantes : Dependent choice, quote and the clcok. Je dois reconnaître que je n'ai pas tout saisi à l'article et aux techniques utilisées, mais je fais confiance à son auteur.
        
        C'est aussi un sport en mathématique de chercher à prouver un énoncé avec le moins d'axiomes possibles et l'axiome du choix est un cas à part : c'est globalement le seul où on pourra trouver des énoncés qui précise explicitement que l'on en fait usage dans la preuve. Dans un dépêche récente présentant un projet d'ouvrage sous licence libre pouvant servir de référence aux candidats à l'agrégation, j'avais fait un commentaire répondant à une demande de preuve sans recourir à cet axiome. La demande était un peu étrange, cela portait sur une question de théorie de la mesure et habituellement quand on demande à un logicien ce qu'il entend par analyse, il répond tout de go : l'arithmétique du second ordre avec axiome du choix dénombrable. C'est la base qui permet de formaliser le calcul intégrale, la théorie de la mesure, l'analyse réelle et complexe… en gros toutes les mathématiques dont ont besoin les physiciens et ingénieurs.
        
        De son côté Gödel avait montré que l'on pouvait l'ajouter aux autres axiomes de la théorie des ensembles sans contradiction en construisant inductivement un univers du discours qui le satisfaisait. Il a construit un univers stratifié où à chaque rang on ne peut parler que des objets de rangs inférieurs ou du rang actuel mais pas des rangs supérieurs encore à venir. L'analogie avec l'approche de MetaOCaml est ses strates ou stage suscite chez moi bien des interrogations.
        
        Pour ce qui est de la possibilité d'utiliser les GADT et la technique du lift générique pour obtenir cette structure stratifiée, je reste dans l'interrogative. Bonne idée à explorer ? fausse piste ? je n'en sais rien. Faut-il adapter le niveau meta du compilateur comme à l'heure actuelle, ou sera-t-il possible de le ramener à une bibliothèque ? le futur le dira. Mais d'après Oleg :
        
        It is now a distinct possibility that MetaOCaml becomes just a regular library or a plug-in, rather being a fork.
        
        Wait and see, comme on dit.
        
        Pour ce qui est de ta dernière remarque :
        
        (Je trouve aussi que ta réponse à benja est trop sèche. C'est un sujet compliqué et c'est un peu normal que les gens se parlent un peu à travers.)
        
        je le reconnais. Mais il y a un certain passif avec benja, cela a du influencé ma réaction. Il m'a enquiquiné sur des détails sans importance (que je n'ai toujours pas compris) en commentaire à ma dépêche de présenttaion du MOOC OCaml. Son ton de l'époque n'était pas des plus plaisant (dans le même genre que celui d'Aluminium dans ton journal de présentation de Malfunction) et il passait complètement à côté du sujet et de l'essentiel de mon propos.
        
        Je donnais un exemple de code du genre :
        
        let fois n = fun verbe cod -> for i = 1 to n do verbe cod done let ecrire = print_endline (fois 5) ecrire "coin< coin<"
        
        afin de montrer l'analogie entre l'analyse de type et l'analyse grammaticale, en me focalisant sur l'analyse du groupe adverbiale « 5 fois ». Exemple qui m'avait été inspiré par des échanges au cours d'un dépêche sur le standard C++17 et un conférence de Gérard Huet. Conférence intitulée Fondements de l'informatique, à la croisée des mathématiques, de la logique et de la linguistique dont je cite ici in extenso un passage :
        
        On nous dit « il faut inculquer aux jeunes l’esprit scientifique ». Très bien, mais qu’est ce que ça veut dire au juste, au-delà d’une incantation un peu creuse ? Inculquer l’esprit scientifique ne se fait pas à coup de bourrage de crâne de connaissances scientifiques rebutantes, ce qui est au contraire la meilleure manière de faire fuir les élèves. De toutes façons, la science moderne est trop vaste et trop complexe pour que quiconque puisse tout connaître, on n’aura plus de Pic de la Mirandole, et c’est aussi bien. Par contre, on peut susciter la curiosité des élèves en mettant en valeur les figures de rhétorique développées par la science pour acquérir ces connaissances. Pour avoir prononcé ce terme de rhétorique devant vous, je devrais m’excuser, c’est un terme vieillot. Autrefois, il y avait des classes de rhétorique, et la notion de débat intellectuel était valorisée. Maintenant c’est terminé, on inculque des connaissances prédigérées, et la Science est imposée comme un prêche. On apprend par cœur des formules que l’on fait réciter, les exercices sont calibrés pour être résolus par application mécanique d’un cours bien saucissonné, l’esprit critique n’est pas encouragé. Ouvrons la fenêtre, discutons des méthodes qui permettent de raisonner droit, de comprendre comment poser des hypothèses, d’élaborer des conjectures, de chercher des contre-exemples. Ces méthodes sont transversales à toutes les matières enseignées, littéraires comme scientifiques. Il y a là un lien important entre philosophie et informatique, car la méthodologie informatique prolonge la rhétorique traditionnelle en tant que moyen légitime d’acquérir des connaissances. Ce sont ces préoccupations qui ont développé la logique, qui a finalement quitté la philosophie pour s’intégrer aux mathématiques, mais a perdu en passant sa finalité argumentative, qui est l’essence de la démarche scientifique. […]
        
        Je vais prendre un autre exemple dans un domaine complètement différent, c’est l’analyse grammaticale dans la classe de français. Je ne sais pas si on fait encore beaucoup ça, mais de mon temps on décortiquait les phrases : toute phrase doit avoir un verbe, tout verbe doit avoir un sujet. Là, il y a un petit bout de raisonnement aussi. Comment est-ce que l’on obtient une phrase à partir d’un verbe ? Prenons d’abord un verbe intransitif. Un verbe intransitif a besoin d’un sujet pour exprimer son action. Donc, vous pouvez voir le rôle fonctionnel de ce verbe comme utilisant le syntagme nominal représentant le sujet pour construire la phrase représentant l’action. De même, un verbe transitif peut être vu comme une fonction qui prend son complément d’objet pour construire un syntagme verbal, se comportant comme un verbe intransitif. Vérifier que « le chat mange la souris » est une phase correcte devient un petit raisonnement où le verbe « mange » prend la souris pour construire « mange la souris », objet fonctionnel qui peut maintenant manger le chat, si je puis dire, pour donner la phrase. Le petit arbre de raisonnement, qui exprime la composition des deux fonctions en vérifiant leurs types, hé bien, c’est ce qu’on appelle l’analyse grammaticale de la phrase. Regardez de près, vous vous rendez compte que c’est exactement le même raisonnement que celui pour la machine à laver du cours de physique, avec deux étapes de modus ponens. L’analyse dimensionnelle devient l’analyse grammaticale. C’est important, en exhibant les procédés rhétoriques similaires on abstrait le raisonnement commun, pour lequel les deux disciplines fournissent des exemples concrets. Les deux exemples s’éclairent l’un l’autre, et on retient un procédé cognitif général qui peut servir pour toutes sortes d’autres investigations. En exhibant le procédé rhétorique commun, et en le réifiant dans deux disciplines supposées étanches l’une à l’autre, on apprend aux élèves que l’esprit scientifique transcende les matières enseignées et les présente comme des aventures intellectuelles cohérentes. Et puis, cela peut donner des idées. En classe de français on faisait de l’analyse grammaticale, mais on n’en faisait pas en classe d’anglais. Pourquoi ? Le même type de raisonnement s’applique, et on montre deux exemples du même phénomène, qui est ainsi mieux mémorisé. Par contre il y a des détails de grammaire qui ne sont pas les mêmes. Par exemple, en introduisant les paramètres morphologiques, on va pouvoir exprimer l’accord du verbe avec son sujet comme une contrainte sur les arbres d’analyse. En français comme en anglais. Par contre, l’adjectif est invariable en anglais, et donc ne s’accorde pas avec le nom qu’il qualifie. En mettant en lumière ces différences structurelles fondamentales, on éclaire les difficultés rencontrées par les élèves, les faux amis, les analogies erronées qui sont difficiles à déraciner. C’est important de le montrer en contraste avec le français. Parce que si vous leur apprenez l’analyse grammaticale du français, il y a une grande partie qu’ils vont pouvoir appliquer à l’anglais aussi, et les parties où cela ne s’applique pas, c’est justement les endroits où il faut faire attention à ne pas calquer d’une langue sur l’autre.
        
        Selon benja, dans mon exemple, mon intention était de « singer les normes du français » (sic). Dois-je lui préciser que Gérard Huet a eu pour thésard Thierry Coquand (à l'origine du langage Coq) et Xavier Leroy (à l'origine du langage OCaml) ? Cherche-t-il lui aussi à singer la grammaire française en comparant le typage des fonctions dans le lambda-calcul avec le fonctionnement des verbes transitifs et intransitifs ? Ou encore avec l'analyse dimensionnelle en physique ? Et de voir que le point commun formel entre tout cela est la forme des jugements hypothétiques et la règle du modus ponens. Dois-je aussi signaler, en passant, que cette forme des jugements hypothétiques et de son principe du modus ponens est le type que donna Kant au principe de causalité dans la Critique de la Raison Pure dans ce qu'il appela logique transcendantale ?
        
        Pour sa seconde remarque sur son insistance à désapprouver le fait que j'appelle fold la fonction générique pour traverser une structure en remplaçant ses constructeurs par des applications de fonctions, je n'ai toujours pas compris.
        
        L'attitude qu'il a eu à l'époque, non dans le faits de faire des remarques ou des critiques, mais dans le ton employé est justement ce qui à tendance à m'énerver sur ce site : c'est trop fréquent, pour tout et n'importe quoi. J'en ai ma claque ! Et là j'ai eu le sensation à demi-mot qu'il prenait le même chemin : j'ai dégainé direct. Oui je sais ce que fait MetaOCaml : pas besoin de chercher à me l'expliquer. Mon intention n'était pas tant d'affirmer que d'interroger. Jusqu'à quel point l'approche de MetaOCaml et de la méthode tagless final se ressemble-t-elle ? Cette dernière, qui a également été mise au point par Oleg Kiselyov auteur de BER MetaOcaml, est-elle un piste envisageable pour atteindre un objectif qu'il semble avoir lui-même ?
        
        It is now a distinct possibility that MetaOCaml becomes just a regular library or a plug-in, rather being a fork.
        source :A brief history of (BER) MetaOCaml
        
        Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par gasche le 14 novembre 2016 à 16:29. Évalué à 3.
        
        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 ?
        
        La réponse un peu triviale c'est que je ne fais pas souvent ça¹. Dans mes cas d'usages personnels on peut souvent revenir éditer la définition initiale. Le problème d'extensibilité des données et opérations (parfois connu sous le nom de "Expression problem" qui est assez peu clair, "Extensibility problem" est un nom plus ancien et plus clair) est intéressant et important, mais pour moi c'est un peu comme la récursion ouverte, ou d'ailleurs les GADTs: moins on en a besoin, plus on peut faire simple, mieux on se porte. Dans les programmes que j'ai eu l'occasion d'écrire, j'ai eu la chance de pouvoir toujours utiliser des approches plus simples.
        
        ¹: Si je voulais vraiment faire ça sans fonctionnalité avancée j'envisagerais d'avoir une définition du type de départ en style "récursion ouverte", avec un constructeur "la suite" qui est paramétré, pour pouvoir faire l'extensibilité après-coup. Ça marche mais c'est assez inélégant à l'usage, puisque si on fait deux couches d'extension il faut traverser deux constructeurs "la suite" et il y a des paramètres dans tous les coins. De plus pour faire ça avec les GADTs il faut abstraire sur un type paramétré, donc un foncteur, ça peut vite devenir lourd aussi.
        
        Après le fait d'avoir plusieurs définitions de données différentes mais proches et liées entre elles (sous-ensembles image de traductions, etc.), qui est aussi bien résolu par les variantes polymorphes, se pose plus souvent dans ma "vraie vie", par exemple quand on écrit des compilateurs c'est typique, et encore plus avec les approches "Nanopass" qui sont assez populaires (Scheme, Scala), avec plein de passes qui touchent seulement une construction ou deux. Souvent les gens utilisent de la métaprogrammation pour faire ça (fonctions de traversée auto-générées, etc.), au lieu d'essayer d'avoir cette modularité dans le langage (à quel coût à l'utilisation ?).
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par kantien le 14 novembre 2016 à 18:52. Évalué à 2.
        
        Après, je ne suis pas développeur ni informaticien, mais mathématicien et logicien. Ce que j'aime c'est retrouver mes « petits », et là cela me parle. Pour l'intérêt pratique, ce n'est pas mon domaine.
        
        Mais au delà du problème de l'extensibilité (c'est un des points), c'est la structure modulaire et composable des optimisations que je trouve élégante. Et comme via le lift générique on a bwf (fwd x) = x quand on ne touche pas à un terme dans une passe, on a une phénomène qui ressemble au cross-stage persistence de MetaOCaml. Ça titille ma curiosité théorique ! :-P
        
        Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
        
        [^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
        
        Posté par gasche le 14 novembre 2016 à 20:04. Évalué à 3.
        
        Il y a un débat assez proche sur la modularité au niveau purement théorique de la construction des preuves de sûreté des langages. Les techniques de preuve par induction sur les dérivations de typage sont assez simples (… quand on a tous les invariants qui vont bien qui sont exprimés par la syntaxe, ce qui est parfois loin d'être simple ou même pas bien compris du tout), mais pas contre il faut en théorie les refaire à chaque fois qu'on modifie un peu le langage, on ne peut pas prouver les constructions une par une de façon modulaire—d'ailleurs les assistants de preuve aident dans ce cas à vérifier rapidement que le reste de la preuve marche toujours. En contraste les techniques de preuves plus sémantiques comme la réalisabilité ou les relations logiques, ou en général par modèles, ont un aspect plus modulaire, puisque les constructions sont montrées admissibles une par une, et en ajouter une nouvelle ne demande pas de reprendre l'existant. Par contre elles sont nettement plus lourdes à mettre en place, et elles fixent quand même un univers de discours qu'il faut modifier et reconstruire quand on introduit des constructions vraiment différentes (enfin dans la syntaxe aussi).