• [^] # Re: Dans l'art voluptueuse de ne rien comprendre

    Posté par . En réponse au journal EDSL et F-algèbres. Évalué à 1.

    pour info, je bosse dans le domaine, autour des objet EMF d'eclipse, et des stéréotypes de sysml

    Je sais que c'est le domaine dans lequel tu travailles; mais je voulais surtout insisté sur le côté embedded du DSL : à la fin on code dans le langage hôte (Haskell, ici OCaml, où le langage que tu veux peu importe) et non dans le DSL.

    Jeremy Gibbons (qui n'est pas né de la dernière pluie non plus) dans son exposé (c'est la vidéo) commence par cette classification :

    Programming Language
     |
     |-- General Purpose
     |
     |-- Domain Specific
     |
     |-- standalone
     |
     |-- embedded
     |
     |-- deep
     |
     |-- shallow
    

    La technique avec construction de l'AST puis interprétation via un fold sur celui-ci c'est du deep, et la technique qu'il présente et qui est le sujet du journal c'est du shallow.

    En regardant à nouveau la vidéo, j'ai vu le passage où il aborde la manière de gérer un type checker : en passant d'une interprétation conctextualisée (avec environnement) à une interprétation non-contextualisée via un flip (dans la vidéo, il ne l'illustre pas sur un type checker mais sur une fonction de pretty printing avec paranthésage minimal) ce qui ramène à la situation d'un fold.

    à propos des type fantômes j'ai retrouvé ça : https://linuxfr.org/users/montaigne/journaux/les-types-fantomes.

    Si tu réutilises ton système de typage de ton langage hôte, tu ne peux pas faire "autre chose", ce qui est très limitant.

    L'idée des types fantômes puis des GADT est de réutiliser le type checker du langage hôte pour s'assure que les termes de l'EDSL sont bien typés. Le principe général de faire de l'embedding est que cela évite d'avoir à coder un lexer et un type checker : on réutilise les outils fournis par la langage hôte. Comme dans l'exemple suivant :

    type _ term =
    | Lit : int -> int term
    | Bool : bool -> bool term
    | Add : int term * int term -> int term
    | Neg : int term -> int term
    | If : bool term * 'a term * 'a term -> 'a term
    let rec eval : type a. a term -> a = function
    | Lit n -> n
    | Bool b -> b
    | Add (t,t') -> (eval t) + (eval t')
    | Neg t -> -(eval t)
    | If (b,t,t') -> if (eval b) then (eval t) else (eval t')
    let lit n = Lit n
    let true_ = Bool true and false_ = Bool false
    let add t t' = Add (t,t')
    let neg t = Neg t
    let if_ b t t' = If (b,t,t');;
    let t1 = if_ true_ (lit 1) (add (lit 2) (lit 3));;
    val t1 : int term = If (Bool true, Lit 1, Add (Lit 2, Lit 3))
    let t2 = if_ false_ (lit 1) (add (lit 2) (lit 3));;
    val t2 : int term = If (Bool false, Lit 1, Add (Lit 2, Lit 3))
    eval t1, eval t2;;
    - : int * int = (1, 5)
    if_ (lit 2) (lit 1) (lit 3);;
    Error: This expression has type int term but an expression was expected of type
     bool term
     Type int is not compatible with type bool

    Enfin, il ne présente pas la méthode shallow comme un remplacement mais comme un approche complémentaire de la méthode deep. Il donne deux exemples intéressants à la fin de la conf', dont un où le shallow language a pour sémantique des termes de l'AST d'un langage plus petit pour, par exemple, compiler vers une architecture very Risc où l'addition add x y est interprétée par Sub x (Sub (Lit 0) y).

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