Journal Tagless-final ou l'art de l'interprétation modulaire.

Posté par  . Licence CC By‑SA.
Étiquettes :
32
22
nov.
2016

Sommaire

Dans la lignée du journal EDSL et F-algèbres, ce journal présente une méthode pour plonger un langage dans un autre (ici OCaml) qui généralise la précédente et centrée autour de la notion d'interprétation. Contrairement aux méthodes plus courantes pour résoudre cette question, la méthode tagless-final permet également de résoudre le problème de l'extensibilité : étendre un type de donnés, ajouter des opérations dessus, sans avoir à réécrire du code déjà compilé et cela avec la sécurité du typage statique.

J'ai essayé d'écrire le journal de telle façon qu'il ne soit pas nécessaire de connaître les fondamentaux du paradigme fonctionnel en programmation, même si une familiarité avec d'autres langages que OCaml sont indispensables. Si certains points vous semblent trop obscurs ou mal expliqués, les commentaires sont là pour vos questions.

Avant de présenter l'approche tagless-final et son originalité, je commencerai par présenter la façon plus « standard » de procéder. Celle-ci consistant à manipuler des structures de données, elle est moins spécifique au langage fonctionnel. Elle sera sans doute plus facile à appréhender dans un premier temps, et permettra de servir de point de comparaison.

Approche par AST comme structure de données ou méthode initiale.

Dans cette première partie, nous étudierons la manière usuelle de représenter les termes d'un langage via une structure de données correspondant à son AST (arbre de syntaxe abstrait). Nous commencerons en présentant cette méthode sur un langage algébrique simple d'expressions sur des entiers.

Langage additif et multiplicatif sur les entiers.

Dans un premier temps, nous allons voir comment représenter en OCaml un langage de calcul sur les entiers avec des expressions comme 1 + 2 + 3, ou 1 + 2 * 3, ou encore (1 + 2) * (3 + 4). La technique courante pour traiter un tel langage en OCaml est de définir un type de données représentant les termes du langage :

type expr = 
  | Lit : int -> expr (* un littéral représentant un entier *)
  | Add : expr * expr -> expr (* une expression représentant une addition *)
  | Mul : expr * expr -> expr (* une expression représentant une multiplication *)

Ce type de données est ce que l'on appelle un type somme ou variant, et ressemble un peu au union du C (en). Chaque ligne définit un constructeur pour ce type de données (par exemple le constructeur Add prend un couple de expr et renvoie un expr) et chaque valeur de ce type correspond à un et un seul de ces trois cas. Afin d'obtenir une expression, on utilise nos constructeurs comme dans ces exemples :

(* 1 + 2 *)
let ex1 = Add(Lit 1, Lit 2);;
val ex1 : expr = Add (Lit 1, Lit 2)

(* (1 + 2) * (3 + 4) *)
let ex2 = Mul(Add(Lit 1, Lit 2), Add(Lit 3, Lit 4));;
val ex2 : expr = Mul (Add (Lit 1, Lit 2), Add (Lit 3, Lit 4))

Une façon de se représenter visuellement une telle structure est sous la forme d'un arbre dont les nœuds sont étiquetés par les constructeurs Add ou Mul et où les feuilles sont des littéraux.

           Mul
         /     \
        /       \
       /         \
     Add         Add
    /   \       /   \
   /     \     /     \
Lit 1  Lit 2  Lit 3  Lit 4

Cette représentation est ce que l'on appelle l'arbre de syntaxe abstrait de l'expression qui, dans notre cas, est le produit de deux additions. Maintenant, afin d'évaluer la valeur entière de celle-ci, on va définir une fonction eval qui parcourt l'arbre récursivement pour le convertir en un entier.

let rec eval : expr -> int = function
  | Lit n -> n
  | Add (e1,e2) -> (eval e1) + (eval e2)
  | Mul (e1,e2) -> (eval e1) * (eval e2)

La définition de la fonction est simple et va de soi : on fait une étude de cas sur la forme que peut avoir notre expression, et on effectue le traitement adapté. Par exemple, dans le cas du constructeur Add on commence par évaluer récursivement chacune des sous-expressions e1 et e2 puis on en calcule la somme. Le compilateur se charge de vérifier que tous les cas possibles sont bien gérés et que l'analyse est exhaustive, sinon il émet un avertissement :

let rec eval : expr -> int = function
  | Lit n -> n
  | Add (e1,e2) -> (eval e1) + (eval e2);;
Characters 29-93:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Mul (_,_)
val eval : expr -> int = <fun>

Ici on a oublié de traiter le cas de la multiplication. On peut maintenant tester notre fonction d'évaluation sur nos exemples :

(* 1 + 2 *)
eval ex1;;
- : int = 3

(* (1 + 2) * (3 + 4) *)
eval ex2;;
- : int = 21

On pourrait aussi, au lieu d'évaluer la valeur du terme, afficher l'arbre sous forme de chaîne de caractères exprimant le calcul à effectuer.

(* une fonction qui prend deux chaînes puis rajoute un + entre les deux *)
let show_add s s' = s ^ " + " ^ s'
(* la même mais pour la multiplication *)
let show_mul s s' = s ^ " * " ^ s'
(* une fonction qui met une chaîne entre paranthèses *)
let paren s = "(" ^ s ^ ")"

(* notre fonction d'affichage *)
let rec view : expr -> string = function
  | Lit n -> string_of_int n
  | Add (e1,e2) -> paren (show_add (view e1) (view e2))
  | Mul (e1,e2) -> paren (show_mul (view e1) (view e2))

let _ = view ex1;;
- : string = "(1 + 2)"

let _ = view ex2;;
- : string = "((1 + 2) * (3 + 4))"

Si l'on regarde le code des deux fonctions eval et view ci-dessus, l'on constate un motif commun :

  • on décompose l'arbre en ses constituants et on applique une fonction aux éléments dans chaque cas ;
  • la valeur d'un nœud ne dépend que de la valeur des ses sous-arbres.

On peut alors coder une fonction générique capturant ce motif qui porte traditionnellement le nom de fold (en) :

let rec fold lit add mul = fun e ->
  let eval_or_view = fold lit add mul in
  match e with
  | Lit i -> lit i
  | Add (e1,e2) -> add (eval_or_view e1) (eval_or_view e2)
  | Mul (e1,e2) -> mul (eval_or_view e1) (eval_or_view e2)

let eval = fold (fun i -> i) (+) ( * )
let view =
  fold string_of_int
       (fun s s' -> paren (show_add s s'))
       (fun s s' -> paren (show_mul s s'))

Dans la définition de fold, j'ai volontairement définie une fonction locale eval_or_view pour souligner la correspondance avec les codes précédents. Regardons un instant le type inféré pour ces trois fonctions :

val fold : (int -> 'a) -> ('a -> 'a -> 'a) -> ('a -> 'a -> 'a) -> expr -> 'a
val eval : expr -> int
val view : expr -> string

La fonction fold prend pour argument une fonction lit : int -> 'a, une fonction add : 'a -> 'a -> 'a et une fonction mul : 'a -> 'a -> 'a qui constituent les interprétations des littéraux et des opérateurs du langage. Le type 'a constitue le domaine dans lequel on interprète nos termes, à savoir int dans le cas de eval et string dans le cas de view. Le principe général de la fonction fold consiste alors à parcourir l'arbre et à remplacer récursivement chaque constructeur par l'application d'une fonction correspondant à l'interprétation de celui-ci.

Nous avons vu là les principes de base pour définir un langage en OCaml :

  • on représente les termes du langage via un variant ;
  • on code une fonction fold générique sur celui-ci ;
  • on se sert de cette fonction pour faire varier les interprétations.

Nous allons voir, à présent, comment faire pour coder des interprétations dites contextuelles à travers l'exemple du pretty printing.

Interprétation contextualisée : le cas du pretty printing.

Dans cette section, nous allons traiter la notion d'interprétation dite contextualisée : l'interprétation d'un terme ne dépend plus alors seulement de ses constituants ou sous-termes, mais également du contexte dans lequel il est utilisé. Un exemple classique de telles interprétations est celui du pretty printing lorsque l'on cherche à afficher élégamment la structure de l'arbre syntaxique.

L'objectif ici sera d'afficher l'arbre en supprimant certaines parenthèses superflues. Si l'on reprend les deux exemples de la section précédente, nous avons pour l'instant :

view ex1;;
- : string = "(1 + 2)"

view ex2;;
- : string = "((1 + 2) * (3 + 4))"

Et l'on voudrait arriver à un affichage minimisant les parenthèses nécessaires à la représentation textuelle de la structure de l'arbre, les opérations étant vues comme associatives à gauche (ce qui est le cas en OCaml) :

show ex1;;
- : string = "1 + 2"

show ex2;;
- : string = "(1 + 2) * (3 + 4)"

Ici l'interprétation d'un terme sous forme de string dépend du contexte dans lequel il est employé : dans le cas de ex2 le terme 1 + 2 qui apparaît comme premier opérande de la multiplication est mis entre parenthèses, alors qu'il ne l'est pas dans le cas de ex1. Une solution consiste à utiliser un contexte p de type int représentant le niveau de précédence dans lequel se trouve le terme, puis de mettre des parenthèses en fonction de la valeur de celui-ci.

(* une fonction de parenthésage sous condition *)
let cparen b = if b then paren else (fun s -> s)

let rec cshow p e = match p,e with
  | _ , Lit n -> string_of_int n
  | p , Add (e1,e2) -> cparen (p > 3) @@ show_add (cshow 3 e1) (cshow 4 e2)
  | p , Mul (e1,e2) -> cparen (p > 4) @@ show_mul (cshow 4 e1) (cshow 5 e2)

cshow 0 ex1;;
- : string = "1 + 2"

cshow 0 ex2;;
- : string = "(1 + 2) * (3 + 4)"

(* avec un nouvel exemple : 1 + (2 + 3 * 4) *)
let ex3 = Add(Lit 1, Add(Lit 2, Mul(Lit 3, Lit 4)));;
val ex3 : expr = Add (Lit 1, Add (Lit 2, Mul (Lit 3, Lit 4)))

cshow 0 ex3;;
- : string = "1 + (2 + 3 * 4)"

Dans le code ci-dessus, on vient de rencontrer une nouvelle notation pour l'application de fonction avec l'opérateur infixe @@. Il est défini en OCaml par l'expression let (@@) f x = f x, ce qui signifie que les expressions f @@ x et f x sont équivalentes. Il permet d'éviter d'avoir recours à de trop nombreuses parenthèses — contrairement au LISP par exemple — autour des arguments d'une fonction, et de faciliter ainsi la lecture et la compréhension du code.

Le motif de la fonction cshow : int -> expr -> string ne suit malheureusement pas celui générique du fold : l'interprétation d'un terme ne dépend pas seulement de la valeur de ses sous-termes. Ici le paramètre p : int sert d'accumulateur quand on descend dans la structure et porte avec lui l'information pour savoir s'il faut ou non parenthèser l'expression — information non prise en compte pour les littéraux.

Que se passe-t-il si l'on définit la même fonction mais en inversant l'ordre des arguments ?

let rec cshow e p = match e,p with
  | Lit n , _ -> string_of_int n
  | Add (e1,e2) , p -> cparen (p > 3) @@ show_add (cshow e1 3) (cshow e2 4)
  | Mul (e1,e2) , p -> cparen (p > 4) @@ show_mul (cshow e1 4) (cshow e2 5)
val cshow : expr -> int -> string = <fun>

On commence à se rapprocher du motif de la fonction fold et la fonction prend bien une valeur de type expr pour renvoyer une fonction de type int -> string. Et si l'on pouvait se ramener à une interprétation via fold mais où l'on interpréterait notre arbre comme une fonction de type int -> string ?

Pour y arriver, faisons un petit détour par la curryfication de fonctions. Le principe est bien connu chez les adeptes de la programmation fonctionnelle, mais peut être moins chez les développeurs non habitués à ce paradigme. C'est surtout pour eux que le présent passage est écrit, pour les autres il suffit de le survoler.

Une fonction est caractérisée par un ensemble de définition (son domaine), un ensemble d'arrivée (son codomaine) et une relation univoque entre un élément du domaine vers un élément du codomaine. Lorsque l'on traite des fonctions de plusieurs variables, le domaine est constitué de n-uplets ou tuples. Le principe de la curryfication consiste à se ramener, dans ce cas, à des fonctions d'une seule variable. Illustrons la chose en python :

def plus (x, y):
  return x + y

>>> plus (1, 2)
3

Ici le domaine est constitué des couples d'entiers et le codomaine des entiers. La curryfication de cette fonction va consister à la transformer en une fonction dont le domaine est constitué des entiers et le codomaine des fonctions des entiers vers les entiers :

plus_curry = lambda x : lambda y : x + y
>>> plus_curry (1)
<function <lambda>.<locals>.<lambda> at 0x7f64b9d46f28>
>>> plus_curry (1) (2)
3

En OCaml, ces exemples donneraient :

let plus = fun (x, y) -> x + y
let plus_curry = fun x -> fun y -> x + y

plus (1, 2);;
- : int = 3

plus_curry 1;;
- : int -> int = <fun>

plus_curry 1 2;;
- : int = 3

Après cette légère digression, revenons à notre fonction de pretty printing :

let rec cshow e p = match e,p with
  | Lit n , _ -> string_of_int n
  | Add (e1,e2) , p -> cparen (p > 3) @@ show_add (cshow e1 3) (cshow e2 4)
  | Mul (e1,e2) , p -> cparen (p > 4) @@ show_mul (cshow e1 4) (cshow e2 5)
val cshow : expr -> int -> string = <fun>

On décompose le couple (e, p) et selon les cas l'on renvoie une chaîne de caractères particulière, il suffit donc de curryfier chaque branche de l'alternative pour obtenir :

let rec cshow e = match e with
  | Lit n -> fun p -> string_of_int n
  | Add (e1,e2) -> fun p ->
      cparen (p > 3) @@ show_add (cshow e1 3) (cshow e2 4)
  | Mul (e1,e2) -> fun p ->
      cparen (p > 4) @@ show_mul (cshow e1 4) (cshow e2 5)
val cshow : expr -> int -> string = <fun>

Ce qui, au final, donne la version suivante de show à base de fold :

let show e =
  let lit i = fun  p -> string_of_int i in
  let add x y = fun p -> cparen (p > 3) @@ show_add (x 3) (y 4) in
  let mul x y = fun p -> cparen (p > 4) @@ show_mul (x 4) (y 5) in
  fold lit add mul e 0

show ex2;;
- : string = "(1 + 2) * (3 + 4)"

show ex3;;
- : string = "1 + (2 + 3 * 4)"

Nous avons vu que même dans le cas où l'interprétation semblait devoir dépendre d'un contexte, l'on pouvait se ramener au cas d'une interprétation sans contexte en changeant le domaine d'interprétation via la curryfication. Essayons à présent d'enrichir un peu notre langage en lui rajoutant une structure conditionnelle du genre if-then-else.

Enrichissons le langage avec des booléens et conditions.

La première idée qui vient à l'esprit est de faire comme précédemment en définissant un variant pour représenter notre nouveau langage. Pour la structure if-then-else, on placera chaque branche dans un thunk (en) car le langage OCaml fait de l'appel par valeur, ainsi l'expression ne sera évaluée que si l'on en a réellement besoin.

type expr =
  | Lit : int -> expr
  | Add : expr * expr -> expr
  | Mul : expr * expr -> expr
  | Bool : bool -> expr
  | If : expr * (unit -> expr) * (unit -> expr) -> expr

Voilà qui est bien mais cela pose deux problèmes :

  • ce nouveau type n'est pas compatible avec le premier et il faut réécrire toutes nos fonctions ;
  • il permet de construire des expressions mal typées, comme ajouter deux booléens.

Le premier point peut être géré, entre autre, via ce que l'on appelle les variants polymorphes mais cette solution, que je ne traiterai pas, ne permet pas de résoudre le second point. Je vais néanmoins montrer comment résoudre le second grâce aux GADT ou types algébriques généralisés. En revanche le premier problème persistera : il faudra réécrire nos fonctions.

Un GADT consiste à utiliser un type paramétré par un autre type et à s'en servir pour typer tant les paramètres que la sortie de chacun des constructeurs du variant.

type _ expr =
  | Lit : int -> int expr
  | Add : int expr * int expr -> int expr
  | Mul : int expr * int expr -> int expr
  | Bool : bool -> bool expr
  | If : bool expr * (unit -> 'a expr) * (unit -> 'a expr) -> 'a expr

En fixant les bonnes valeurs du paramètre de type dans chacune des branches, on s'assure ainsi de ne jamais pouvoir ajouter deux booléens sans déclencher d'erreurs de typage à la compilation :

Add (Bool true, Bool false);;
     ^^^^^^^^^
Error: This expression has type bool expr
but an expression was expected of type int expr
Type bool is not compatible with type int

Outre la garantie de typage qu'ils offrent pour notre langage, les GADT sont un outil puissant afin de garantir de nombreux invariants sur des structures de données. Leurs possibilités dépassent de loin le cadre de ce journal, mais on pourra trouver un exposé détaillé dans cette leçon en anglais accompagné de son TD qui permet d'utiliser OCaml dans son navigateur.

Le typage de fonctions impliquant des GADT n'est en général pas décidable et il n'est pas possible de définir une fonction aussi générique que le fold comme pour les variants classiques. Je me contenterai simplement de montrer comment écrire la fonction eval pour ce nouveau langage.

let rec eval : type a. a expr -> a = function
  | Lit n -> n
  | Add (x,y) -> (eval x) + (eval y)
  | Mul (x,y) -> (eval x) * (eval y)
  | Bool b -> b
  | If (b,th,el) -> if (eval b) then eval (th ()) else eval (el ())

Il faut ajouter une annotation de typage avec un type local abstrait (type a) pour préciser au compilateur que le type de retour est le même que le paramètre de type de l'expression. En dehors de cette annotation, le corps de la fonction est équivalente à sa version avec variant classique. Son retour sur un exemple :

eval (If (Bool true, (fun () -> Lit 1), (fun () -> Lit 2)));;
- : int = 1

Approche par AST sous forme de fonctions ou méthode tagless-final.

Maintenant que nous avons vu comment comment plonger un langage en OCaml selon la méthode initiale, nous traiterons une autre méthode — objet principal du présent journal — qui permet de résoudre un problème inaccessible à l'autre manière de procéder : étendre les langages en réutilisant le code déja écrit.

Langage additif et multiplicatif sur les entiers.

Le principe de base de cette méthode consistera à utiliser le système de modules du langage OCaml (en), de s'inspirer des GADT pour garantir le bon typage du langage et de la fonction fold pour déterminer le contenu des modules. Dans un premier temps, un module peut être vu comme un espace de noms contenant des déclarations de type et de valeurs. Chaque module dispose d'une signature, qui est l'équivalent des types pour les modules, et celle-ci exprime la nature des éléments déclarés par le module.

module type SIG = sig
  type t
  val i : t
end

module M : SIG = struct
  type t = int
  let i = 1
end

M.i;;
- : M.t = <abstr>

Dans cet exemple, un module satisfaisant la signature SIG doit déclarer un type t et une valeur i de type t. Ce que fait le module M définit ensuite, et l'on accède aux valeurs définies dans le module par la notation pointée. Ici c'est de peu d'utilité car comme extérieurement on ne sait rien sur le type t de la valeur, on ne peut pas en faire usage. Pour pouvoir l'utiliser, il faudrait que le module M définisse également des fonctions pour opérer sur les valeurs du type qu'il déclare. C'est ce que nous allons faire avec notre langage 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

Cette signature définit deux types et quelques fonctions pour opérer dessus. On peut remarquer que le type des fonctions lit, add et mul mime, sous forme curryfiée, les constructeurs du GADT de la première partie. Le type paramétré 'a repr servira à la représentation interne des termes de notre langage, tandis que le type 'a obs permettra de les présenter extérieurement. Le nom de la signature est préfixée par SYM ce qui renvoie au néologisme symantique forgée par les inventeurs de la méthode afin de signifier que celle-ci exprime à la fois la syntaxe et la sémantique du langage.

Pour implémenter un module satisfaisant cette signature, il suffit alors de réutiliser ce que nous avons fait précédemment pour diversifier les interprétations avec la fonction fold. Chaque module correspondra à une interprétation différente de notre langage, et le code des fonctions sera celui des arguments passés à la fonction fold. On se retrouve alors avec ces deux interprétations possibles :

module EvalInt = struct
  type 'a repr = 'a
  type 'a obs = 'a

  let lit n = n
  let add = ( + )
  let mul = ( * )

  let observe x = x
end

module ShowInt = struct
  type 'a repr = int -> string
  type 'a obs = string

  (* quelques fonctions utilitaires *)
  let paren s = "(" ^ s ^ ")"
  let cparen b = if b then paren else (fun s -> s)
  let show_int = string_of_int
  let show_add s s' = s ^ " + " ^ s'
  let show_mul s s' = s ^ " * " ^ s'

  let lit n = fun p -> show_int n
  let add x y = fun p ->
    cparen (p > 3) @@ show_add (x 3) (y 4)
  let mul x y = fun p ->
    cparen (p > 4) @@ show_mul (x 4) (y 5)

  let observe x = x 0
end

Afin de les tester, définissons un module d'exemples :

module ExInt (I : SYM_INT) = struct
  open I
  let observe = observe
  let ( + ) = add
  let ( * ) = mul
  let ex1 = lit 1 + lit 2
  let ex2 = (lit 1 + lit 2) * (lit 3 + lit 4)
  let ex3 = lit 1 + (lit 2 + lit 3 * lit 4)
end

Ce module, contrairement aux précédents, est paramétré par un autre module d'interprétation de notre langage : c'est ce que l'on appelle un foncteur. La directive open permet d'ouvrir l'espace de nom du module I pour ne pas avoir besoin d'utiliser la notation pointée. Pour l'usage, cela se passe comme suit :

(* on applique notre foncteur sur nos deux modules *)
module ExEval = ExInt(EvalInt)
module ExShow = ExInt(ShowInt)

(* on teste le bon fonctionnement de nos interprétations *)
ExEval.(observe ex2);;
- : int = 21

ExShow.(observe ex2);;
- : string = "(1 + 2) * (3 + 4)"

ExShow.(observe ex3);;
- : string = "1 + (2 + 3 * 4)"

Enrichissons le langage avec des booléens et conditions.

Comme dans la première partie nous allons maintenant tenter d'étendre notre langage, et c'est là que nous verrons la supériorité de cette méthode sur l'autre : on pourra réutiliser le code déjà écrit. On commence par définir la signature définissant la symantique du langage étendu.

module type SYM_INT_COND = sig
  include SYM_INT

  val bool_ : bool -> bool repr
  val if_ : bool repr -> (unit -> 'x) -> (unit -> 'x) -> ('a repr as 'x)
  val eq : int repr -> int repr -> bool repr
  val lt : int repr -> int repr -> bool repr
end

Afin d'étendre le langage, il suffit d'utiliser la directive include puis de rajouter ensuite les nouvelles constructions du langage. On en a profité ici pour ajouter des fonctions de comparaisons sur les entiers. Pour les nouvelles interprétations, on procède de même :

module EvalIntCond = struct
  include EvalInt

  let bool_ b = b
  let if_ b th el = if b then th () else el ()
  let eq = ( = )
  let lt = ( < )
end

module ShowIntCond = struct
  include ShowInt

  let show_bool = string_of_bool
  let show_if bs ts es = "if " ^ bs ^ " then " ^ ts ^ " else " ^ es
  let show_eq s s' = s ^ " = " ^ s'
  let show_lt s s' = s ^ " < "  ^ s'

  let bool_ b = fun p -> show_bool b
  let if_ b th el = fun p ->
    cparen (p > 0) @@ show_if (b 0) (th () 0) (el () 0)
  let eq x y = fun p ->
    cparen (p > 0) @@ show_eq (x 1) (y 1)
  let lt x y = fun p ->
    cparen (p > 0) @@ show_lt (x 1) (y 1)
end

On peut de même étendre notre module d'exemples pour tester ces nouvelles interprétations :

module ExIntCond (I : SYM_INT_COND) = struct
  include ExInt(I)
  open I
  let ( = ) = eq
  let ( < ) = lt

  let true_ = bool_ true
  let false_ = bool_ false

  let ex4 = if_ true_ (fun () -> ex3) (fun () -> ex2)
  let ex5 = if_ (lit 1 < lit 2) (fun () -> ex3) (fun () -> ex4)
  let ex6 = if_ (ex5 = ex3) (fun () -> true_) (fun () -> false_)
end

Quelques tests :

module ExEval = ExIntCond(EvalIntCond)
module ExShow = ExIntCond(ShowIntCond)

ExEval.(observe ex4);;
- : int = 15

ExEval.(observe ex5);;
- : int = 15

ExEval.(observe ex6);;
- : bool = true

ExShow.(observe ex6);;
- : string = 
"if (if 1 < 2 then 1 + (2 + 3 * 4)
    else if true then 1 + (2 + 3 * 4)
    else (1 + 2) * (3 + 4)) = 1 + (2 + 3 * 4)
then true else false"

ExShow.(observe ex4);;
- : string = "if true then 1 + (2 + 3 * 4) else (1 + 2) * (3 + 4)"

Fiat lux : Que la lumière soit, et la lumière fut !

Jusqu'ici nous avons représenté les termes de nos langages objets directement dans le langage hôte OCaml de deux manières distinctes :

  • arbre syntaxique comme structure de données ;
  • arbre syntaxique sous forme de fonctions.

Nous allons montrer qu'au fond la première technique n'est qu'un cas particulier de la seconde, et illustrer comment l'approche tagless-final généralise la première. Ainsi, la première se subsumant sous la seconde, dans la suite du journal nous n'utiliserons plus que cette dernière.

Reprenons le code écrit jusqu'ici pour la méthode avec structures de données et fold pour le langage additif et multiplicatif, puis encapsulons le dans un module.

module Ast = struct
  (* on y met les définitions du type, du fold
   * et des différentes intéprétations *)
end

À partir de là, rien de plus simple que de définir des modules de signature SYM_INT qui s'intègrent parfaitement dans l'approche tagless-final.

On commence par un module dont la représentation interne est justement notre structure de données :

module AstBase = struct
  type _ repr = Ast.expr
  let lit n = Ast.Lit n
  let add x y = Ast.Add (x,y)
  let mul x y = Ast.Mul (x,y)
end

puis on l'étend vers différents modules de signature SYM_INT qui observeront ou interpréteront nos arbres différemment.

module AstEval = struct
  include AstBase 
  type _ obs = 'a
  let observe = Ast.eval
end

module AstShow = struct
  include AstBase
  type _ obs = string
  let observe = Ast.show
end

On peut maintenant les utiliser sans problème avec notre module d'exemples :

module ExEval = ExInt(AstEval)
module ExShow = ExInt(AstShow)

ExEval.(observe ex3);;
- : int = 15

ExShow.(observe ex3);;
- : string = "1 + (2 + 3 * 4)"

Optimisons un peu nos interprètes !

Dans cette section nous présenterons un cadre général, et ses principes, pour effectuer des optimisations sur nos langages. Nous verrons aussi comment tirer profit de la structure modulaire du code pour réaliser cette tâche.

Suppression des opérandes nuls.

La première optimisation que l'on va voir est celle qui consiste à supprimer tous les litéraux nuls, en appliquant les règles : x + 0 = 0 + x = 0 et x * 0 = 0 * x = 0.

Pour ce faire, on partira d'un interprète I quelconque puis on représentera chaque terme à l'aide d'un GADT qui exprimera notre connaissance sur sa nullité. Enfin, pour l'observer, on se contentera de renvoyer l'observation par I.

module RemoveZero (I : SYM_INT) = struct
  type 'a repr =
    | Unk : 'a I.repr -> 'a repr
    | Zero : int repr
  type 'a obs = 'a I.obs

  let lit n = if n = 0 then Zero else Unk (I.lit n)
  let add x y = match x,y with
    | Zero, _ -> y
    | _, Zero -> x
    | Unk x, Unk y -> Unk (I.add x y)
  let mul x y = match x,y with
    | Zero, _
    | _, Zero -> Zero
    |Unk x, Unk y -> Unk (I.mul x y)

  let observe : type a. a repr -> a obs = function
    | Unk x -> I.observe x
    | Zero -> I.observe (I.lit 0)
end

On écrit un module de test pour vérifier que tout se passe bien :

module Test (I : SYM_INT) = struct
  open I
  let observe = observe
  let (+) = add
  let ( * ) = mul

  let e1 = lit 1 + lit 0 + lit 2
  let e2 = e1 + lit 0 * lit 3
end

(* sans optimisation *)
let module M = Test(ShowInt) in
M.(observe e2);;
- : string = "1 + 0 + 2 + 0 * 3"

(* l'optimiseur en pratique *)
let module M = Test(RemoveZero(ShowInt)) in
M.(observe e2);;
- : string = "1 + 2"

(* sur un interprète issu de la méthode avec variant *)
let module M = Test(RemoveZero(AstShow)) in
M.(observe e2);;
- : string = "1 + 2"

Principe général des transformations.

Lorsque l'on a supprimé les littéraux nuls, on a au fond transformer l'arbre syntaxique (comme le montre leur représentation sous forme de chaîne de caractères) mais sans modifier son interprétation naturelle en tant qu'entier.

À cet effet, on est parti d'une représentation donnée par un interprète I, puis l'on a envoyé les représentations dans un autre domaine Unk : 'a I.repr -> 'a repr | Zero : int repr afin d'opérer dessus, pour enfin revenir dans le domaine de l'interpréteur I et observer la transformation. Le principe de l'aller-retour entre deux domaines est capturé par la signature de module suivante :

module type TRANS = sig
  type 'a from
  type 'a term
  val fwd : 'a from -> 'a term
  val bwd : 'a term -> 'a from
end

L'optimiseur travaille sur des 'a term qui contiennent les informations nécessaires à sa tâche. Ils sont obtenus à partir d'une autre représentation intermédiaire 'a from via la fonction fwd puis, une fois l'optimisation terminée, on revient dans la représentation de départ à l'aide de la fonction bwd.

On peut coder à partir d'une transformation X : TRANS un « optimiseur » trivial qui… ne change rien :-P

module SymIntT (X : TRANS) (I : SYM_INT with type 'a repr = 'a X.from) = struct
  open X
  type 'a repr = 'a term
  type 'a obs = 'a I.obs

  let lit n = fwd @@ I.lit n
  let add x y = fwd @@ I.add (bwd x) (bwd y)
  let mul x y = fwd @@ I.mul (bwd x) (bwd y)
  let observe x = I.observe (bwd x)
end

Pour avoir un optimiseur plus utile que celui-ci, il faut fournir deux choses :

  • une transformation X : TRANS pour obtenir des termes sur lesquels opérer ;
  • un interprète partiel qui opère sur la partie du langage qu'il optimise.

Le plus simple est de mettre le tout dans un module, ce qui dans le cas de la suppression des zéros donne :

module RemoveZeroPass (I : SYM_INT) = struct
  (* la transformation pour faire l'aller-retour entre les deux domaines *)
  module X = struct
    type 'a from = 'a I.repr
    type 'a term =
      | Unk : 'a I.repr -> 'a term
      | Zero : int term

    let fwd x = Unk x
    let bwd : type a. a term -> a from = function
      | Unk x -> x
      | Zero -> I.lit 0
  end
  open X 
  (* la passe d'optimisation proprement dite *)
  module IDelta = struct
    let lit n = if n = 0 then Zero else fwd @@ I.lit n
    let add x y = match x,y with
      | Zero, _ -> y
      | _, Zero -> x
      | _ -> fwd @@ I.add (bwd x) (bwd y)
    let mul x y = match x,y with
      | Zero, _
      | _, Zero -> Zero
      | _ -> fwd @@ I.mul (bwd x) (bwd y)
  end
end

Afin de préserver l'interprétation des termes qui ne sont pas concernés par la passe d'optimisation, il faut s'assurer que l'on a toujours bwd (fwd x) = x, ce qui est évident dans notre cas. Le module IDelta porte ce nom pour signifier qu'il contient la différence (le delta) d'interprétation par rapport à l'interprète initial I.

À partir de là, on obtient l'optimiseur de la manière suivante :

module RemoveZeroInt (I : SYM_INT) = struct
  module OptM = RemoveZeroPass(I)

  (* on inclut l'optimiseur trivial qui ne fait rien *)
  include SymIntT(OptM.X)(I)

  (* on surcharge les fonctions lit, add et mul *)
  include OptM.IDelta
end

let module M = Test(RemoveZeroInt(ShowInt)) in
M.(observe e2);;
- : string = "1 + 2"

Pour le lecteur qui aime bien les graphiques, on pourrait représenter la passe d'optimisation ainsi :

Domaine 'a from : terme t         t optimisé ------> t observé : 'a obs
                      |                 ^   I.observe
                      |                 |
                  fwd |                 | bwd
                      |                 |
                      V    passe        |
Domaine 'a term : terme t' -----> t' optimisé

Cette façon de procéder peut sembler étrange au premier abord : pourquoi inclure un optimiseur qui ne fait rien, pour ensuite remplacer immédiatement les fonctions qu'il importe ? Cela n'a effectivement aucun intérêt dans ce cas précis, mais elle illustre un principe général qui sera fort apprécié lorsque la passe ne modifiera pas toutes les constructions du langage : seules les fonctions de l'optimiseur trivial réellement utilisées par le notre seront remplacées et les autres resteront inchangées.

Simplification de la multiplication par un.

Dans la même lignée que l'optimisation précédente, on peut simplifier nos termes du langage en faisant usage de la règle : x * 1 = 1 * x = x.

module RemoveOnePass (I : SYM_INT) = struct
  module X = struct
    type 'a from = 'a I.repr
    type 'a term =
      | Unk : 'a from -> 'a term
      | One : int term
    let fwd x = Unk x
    let bwd : type a. a term -> a from = function
      | Unk x -> x
      | One -> I.lit 1
  end
  open X
  module IDelta = struct
    let lit n = if n = 1 then One else fwd @@ I.lit n
    let mul x y = match x,y with
      | One, _ -> y
      | _, One -> x
      | _ -> fwd @@ I.mul (bwd x) (bwd y)
  end
end

(* on utilise la passe comme au-dessus *)
module RemoveOneInt (I : SYM_INT) = struct
  module OptM = RemoveOnePass(I)
  include SymIntT(OptM.X)(I)
  (* on surcharge lit et mul *)
  include OptM.IDelta
end

Ici la transformation triviale est utile car la passe ne touche pas à l'addition. Un petit test qui combine les deux passes :

module Test (I : SYM_INT) = struct
  open I
  let observe = observe
  let ( +) = add
  let ( * ) = mul

  let e = lit 1 * lit 2 + lit 0
end

let module M = Test(RemoveZeroInt(ShowInt)) in
M.(observe e);;
- : string = "1 * 2"

let module M = Test(RemoveOneInt(ShowInt)) in
M.(observe e);;
- : string = "2 + 0"

(* nos deux passes commutent *)
let module M = Test(RemoveOneInt(RemoveZeroInt(ShowInt))) in
M.(observe e);;
- : string = "2"

let module M = Test(RemoveZeroInt(RemoveOneInt(ShowInt))) in
M.(observe e);;
- : string = "2"

Réutilisation de nos passes sur le langage étendu.

Un des grands avantages de la méthode tagless-final est de pouvoir réutiliser du code déjà écrit en structurant le programme de façon modulaire. Les optimisations n'échappent pas à la règle. Pour récupérer nos précédentes passes, il faut d'abord définir notre transformation triviale pour le langage étendu.

module SymIntCondT (X : TRANS)
(I : SYM_INT_COND with type 'a repr = 'a X.from) = struct
  (* on commence par récupérer la précédente *)
  include SymIntT (X)(I)
  open X  
  (* on ajoute les nouvelles constructions du langage *)
  let bool_ b = fwd @@ I.bool_ b
  let if_ b th el =
    fwd @@ I.if_ (bwd b) (fun () -> bwd @@ th ()) (fun () -> bwd @@ el ())
  let eq x y = fwd @@ I.eq (bwd x) (bwd y)
  let lt x y = fwd @@ I.lt (bwd x) (bwd y)
end

Et l'on peut alors réutiliser nos passes directement :

module RemoveZeroIntCond (I : SYM_INT_COND) = struct
  module OptM = RemoveZeroPass(I)
  include SymIntCondT(OptM.X)(I)
  (* on ne surcharge que les constructeurs optimisés *)
  include OptM.IDelta
end

module RemoveOneIntCond (I : SYM_INT_COND) = struct
  module OptM = RemoveOnePass(I)
  include SymIntCondT(OptM.X)(I)
  (* on ne surcharge que les constructeurs optimisés *)
  include OptM.IDelta
end

Un petit test pour la route :

module Test (I : SYM_INT_COND) = struct
  open I
  let observe = observe
  let ( + ) = add
  let ( * ) = mul
  let ( = ) = eq

  let e =
    if_ (lit 1 * lit 2 = lit 2 + lit 0)
    (fun () -> lit 3 * lit 1)
    (fun () -> lit 4 + lit 0)
end

let module M = Test(RemoveZeroIntCond(ShowIntCond)) in
M.(observe e);;
- : string = "if 1 * 2 = 2 then 3 * 1 else 4"

let module M = Test(RemoveOneIntCond(ShowIntCond)) in
M.(observe e);;
- : string = "if 2 = 2 + 0 then 3 else 4 + 0"

let module M = Test(RemoveOneIntCond(RemoveZeroIntCond(ShowIntCond))) in
M.(observe e);;
- : string = "if 2 = 2 then 3 else 4"

Étendre le langage avec des fonctions.

Notre langage commence à devenir sympa, mais ce serait mieux si on lui rajoutait la possibilité de définir des fonctions. C'est ce que nous ferons dans cette dernière partie, et nous rajouterons une passe de calcul des valeurs statiquement connues.

La symantique étendue et ses interprètes.

Pour étendre la signature du langage et rajouter des fonctions, rien de plus simple :

module type SYM_INT_COND_HO = sig
  include SYM_INT_COND
  val lam : ('a repr -> 'b repr) -> ('a -> 'b) repr
  val app : ('a -> 'b) repr -> 'a repr -> 'b repr
end

On ajoute un opérateur d'abstraction lam pour créer des fonctions, et un opérateur d'application app pour les utiliser. On étend ensuite nos interprètes en commençant par l'évaluateur.

module EvalIntCondHO = struct
  include EvalIntCond
  let lam f = f
  let app f x = f x
end

Pour l'interprète de pretty printing, il va falloir adapter légèrement la représentation interne pour prendre en compte le nombre de paramètres des fonctions.

module ShowIntCondHO = struct
  (*
    on ajoute un paramètre entier à nos représentations
    pour prendre en compte le nombre de variables de nos
    fonctions et éviter les colisions de noms.
  *)
  type 'a repr = int -> int -> string
  type 'a obs = string

  (*
    on surcharge nos fonctions de l'interprète du sous-langage
    avec entiers et booléens que l'on enveloppe pour prendre
    en compte le nouveau paramètre.
  *)
  open ShowIntCond

  let lit n = fun c -> lit n
  let add x y = fun c -> add (x c) (y c)
  let mul x y = fun c -> mul (x c) (y c)
  let bool_ b = fun c -> bool_ b
  let eq e e' = fun c -> eq (e c) (e' c)
  let lt i j = fun c -> lt (i c) (j c)
  let if_ b then_e else_e = fun c ->
    if_ (b c) (fun () -> then_e () c) (fun () -> else_e () c)

  (* quelques fonctions utilitaires *)
  let show_lam v body = "fun " ^ v ^ " -> " ^ body
  let varnames = "xyztuvw"
  let varname = function
    | i when i < String.length varnames ->
        String.make 1 varnames.[i]
    | i -> "x" ^ string_of_int i

  let lam f = fun c p ->
    let v = varname c in
    let body = f (fun _ _-> v) (c + 1) 0 in
    cparen (p > 0) @@ show_lam v body

  let app f x = fun c p -> 
    cparen (p > 10) (f c 10 ^ " " ^ x c 11)

  let observe x = x 0 0
end

On peut toujours interpréter les précédents exemples avec ces nouveaux modules :

let module M = ExIntCond(EvalIntCondHO) in
M.(observe ex3);;
- : int = 15

let module M = ExIntCond(ShowIntCondHO) in
M.(observe ex3);;
- : string = "1 + (2 + 3 * 4)"

Mais également des termes du nouveau langage, comme il se doit :

module ExHO (I : SYM_INT_COND_HO) = struct
  include ExIntCond(I)
  open I
  let app = app
  let lit = lit
  let ex7 = lam @@ fun x ->
    (x + lit 2 + lit 3 * x) * (lit 2 + x)
  let ex8 = app ex7 (lit 3)
  let ex9 x = lam @@ fun y ->
    if_ (y < lit x) (fun () -> lit 2 * y) (fun () -> lit 3 * y)
end

let module M = ExHO(EvalIntCondHO) in
M.(observe ex7);;
- : int -> int = <fun>

let module M = ExHO(EvalIntCondHO) in
M.(observe ex7) 3;;
- : int = 70

let module M = ExHO(EvalIntCondHO) in
M.(observe ex8);;
- : int = 70

let module M = ExHO(ShowIntCondHO) in
M.(observe ex7);;
- : string = "fun x -> (x + 2 + 3 * x) * (2 + x)"

let module M = ExHO(ShowIntCondHO) in
M.(observe ex8);;
- : string = "(fun x -> (x + 2 + 3 * x) * (2 + x)) 3"

let module M = ExHO(StaticHO(ShowIntCondHO)) in
M.(observe (ex9 2));;
- : string = "fun x -> if x < 2 then 2 * x else 3 * x"

Évaluation partielle et statique.

Il ne nous reste plus qu'à réaliser une optimisation qui réduit ce qui est statiquement connu. On commencera par définir notre transformation triviale puis nous passerons à la passe proprement dite.

module SymIntCondHOT (X : TRANS)
(I : SYM_INT_COND_HO with type 'a repr = 'a X.from) = struct
  include SymIntCondT(X)(I)
  open X
  let lam f = fwd @@ I.lam @@ fun x -> bwd (f (fwd x))
  let app f x = fwd @@ I.app (bwd f) (bwd x)
end

Pour la passe statique le code est assez simple : on commence par étiquetés nos termes pour savoir s'il sont statiquement connus (Sta), si c'est une fonction (Fun) ou s'ils ne seront connus que dynamiquement (Dyn). Dans le cas des fonctions, on les applique statiquement, si l'on opère avec des valeurs statiques alors on effectue le calcul statiquement, sinon on se rabat sur notre interprète I.

module StaticPass (I : SYM_INT_COND_HO) = struct
  module X = struct
    type 'a from = 'a I.repr    
    type 'a term =
      | Dyn : 'a from -> 'a term
      | Sta : ('a * 'a from) -> 'a term
      | Fun : ('a term -> 'b term) -> ('a -> 'b) term

    let fwd x = Dyn x
    let rec bwd : type a. a term -> a from = function
      | Dyn x -> x
      | Sta (_,x) -> x
      | Fun f -> I.lam @@ fun x -> bwd (f (fwd x))
  end
  open X
  module IDelta = struct
    let lit n = Sta (n, I.lit n)
    let add x y = match x,y with
      | Sta (x,_) , Sta (y,_) -> lit (x + y)
      | _ -> fwd @@ I.add (bwd x) (bwd y)
    let mul x y = match x,y with
      | Sta (x,_) , Sta (y,_) -> lit (x * y)
      | _ -> fwd @@ I.mul (bwd x) (bwd y)

    let bool_ b = Sta (b, I.bool_ b)
    let if_ b th el = match b with
      | Sta (b,_) -> if b then th () else el ()
      | _ -> fwd @@ I.if_ (bwd b) (fun () -> bwd @@ th()) (fun () -> bwd @@ el())

    let eq x y = match x,y with
      | Sta (x,_) , Sta(y,_) -> bool_ (x = y)
      | _ -> fwd @@ I.eq (bwd x) (bwd y)

    let lt x y = match x,y with
      | Sta (x,_) , Sta (y,_) -> bool_ ( x < y )
      | _ -> fwd @@ I.lt (bwd x) (bwd y)

    let lam f = Fun f

    let app f x = match f with
      | Fun f -> f x
      | _ -> fwd @@ I.app (bwd f) (bwd x)
  end
end

On peut alors définir notre optimiseur et récupérer les précédents.

module RemoveZeroHO (I : SYM_INT_COND_HO) = struct
  module OptM = RemoveZeroPass(I)
  include SymIntCondHOT(OptM.X)(I)
  include OptM.IDelta
end

module RemoveOneHO (I : SYM_INT_COND_HO) = struct
  module OptM = RemoveOnePass(I)
  include SymIntCondHOT(OptM.X)(I)
  include OptM.IDelta
end

module StaticHO (I : SYM_INT_COND_HO) = struct
  module OptM = StaticPass(I)
  include SymIntCondHOT(OptM.X)(I)
  include OptM.IDelta
end

La passe statique en action :

let module M = ExHO(ShowIntCondHO) in
M.(observe ex8);;
- : string = "(fun x -> (x + 2 + 3 * x) * (2 + x)) 3"

let module M = ExHO(StaticHO(ShowIntCondHO)) in
M.(observe ex8);;
- : string = "70"

let module M = ExHO(ShowIntCondHO) in
M.(observe (ex9 4));;
- : string = "fun x -> if x < 4 then 2 * x else 3 * x"

let module M = ExHO(ShowIntCondHO) in
M.(observe @@ app (ex9 4) (lit 2));;
- : string = "(fun x -> if x < 4 then 2 * x else 3 * x) 2"

let module M = ExHO(StaticHO(ShowIntCondHO)) in
M.(observe @@ app (ex9 4) (lit 2));;
- : string = "4"

let module M = ExHO(StaticHO(ShowIntCondHO)) in
M.(observe @@ app (ex9 1) (lit 2));;
- : string = "6"

Conclusion.

Le journal n'a présenté que dans les grands traits la méthode dite tagless-final pour plonger un langage dans un langage fonctionnel hôte. Comparée à la méthode plus classique consistant à représenter l'arbre de syntaxe abstrait du langage par un type de données algébriques (généralisé ou non), celle-ci permet d'étendre facilement les langages sans avoir à réécrire de code. De plus, elle garantie la bonne formation (au niveau du typage) des termes de nos langages en réutilisant le système de types du langage hôte : pas besoin d'écrire un type checker. De par sa structure modulaire, le code permet d'écrire des passes d'optimisations qui se concentrent uniquement sur le sous-ensemble du langage à optimiser. Par construction, ces dernières sont assurées de préserver le typage des termes et en « collant » à la sémantique dénotanionnelle du langage il est plus aisé de s'assurer de leur bon fonctionnement.

Les exemples du journal sont surtout des exemples jouets, ils servent essentiellement à illustrer les principes généraux de la méthode tagless-final. Pour un exemple d'application, sans doute plus utile dans la vie courante d'un développeur, on pourra regarder du côté de quel (sous licence MIT). Il permet de générer des requêtes SQL optimisées avec la garantie du typage statique. Son fonctionnement est présenté dans l'article Finally, Safely-Extensible and Efficient Language-Integrated Query.

On pourra également consulter l'exemple du langage des circuits logiques. Il se trouve sur la page du tutoriel sur l'optimisation via la méthode tagless-final de Oleg Kiselyov, tutoriel qui m'a servi de base pour ce journal. On y trouve des exemples de codes en Haskell et OCaml.

Comme référence, il y a enfin l'article originel présentant la méthode : Finally Tagless, Partially Evaluated. Celle-ci y est combinée à MetaOCaml (présenté récemment dans une dépêche) afin d'obtenir un interprète, un compilateur, un évaluateur partiel ou encore différentes transformations ou méthodes d'évaluation (par nom, par valeur…) pour le langage objet.

  • # Merci pour l'effort.

    Posté par  . Évalué à 5.

    Moi je ferais l'effort d'essayer de comprendre, mais je sens que ça va me prendre du temps…

    • [^] # Re: Merci pour l'effort.

      Posté par  . Évalué à 3.

      De rien. Cela m"a pris aussi du temps pour bien comprendre les tenants et aboutissants de la méthode. Écrire ce journal m'a permis de mieux l'assimiler, et il a connu plusieurs versions en fonction de l'évolution de ma compréhension.

      Si tu as des questions sur des points précis de code ou sur les principes méthodologiques, n'hésite pas. J'essaierai de clarifier la chose du mieux que je peux.

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

  • # chaud

    Posté par  (site web personnel) . Évalué à 2.

    J'ai encore mal au cerveau.

    Cela serait bien de proposer le code complet minimal par exemple (github ?). C'est parfois pas évident de comprendre les dépendances entre bout de code.

    "La première sécurité est la liberté"

    • [^] # Re: chaud

      Posté par  . Évalué à 1.

      J'ai encore mal au cerveau.

      Désolé. :-P

      Cela serait bien de proposer le code complet minimal par exemple (github ?). C'est parfois pas évident de comprendre les dépendances entre bout de code.

      Pourquoi pas. Il faudrait par contre que j'apprenne à me servir git et github. Tu connais un tutoriel pour une prise en main rapide du système ?

      Pour ce qui est du code que tu voudrais voir. Pourrais-tu être plus précis sur ce que tu attends ?
      Il y a un tutoriel avec plusieurs fichiers de code sur le langage des circuits logiques. Le code est complet et commenté, c'est cela que tu veux ? Là, Oleg utilise en plus la bibliothèque higher de Jeremy Yallop et Leo White. Cela lui permet de faire du higher-kinded polymorphism pour « dissimuler » le paramètre 'a du type 'a obs, d'utiliser ainsi des modules de première classe et de manipuler les foncteurs comme des fonctions normales.

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

      • [^] # Re: chaud

        Posté par  (site web personnel) . Évalué à 2.

        Justement, je voudrais les exemples de chaque étape, y compris le premier. Les fichiers dont tu parles doivent être bien trop compliqué pour comprendre le principe.

        J'ai codé pendant 2 ans en ocaml fonctionnel simple. Et tout ce qui est foncteur/module, et les opérateurs spécifiques (@@) me semblent bien étrange et peu lisible.

        Je n'ai toujours pas compris en quoi un module est si différent d'un objet ou d'une classe.

        Pour github, il suffit de s'inscrire dessus, créer un projet, et faire un premier git clone sur sa machine. Puis des "git add" pour ajouter les fichiers dans l'index, "git commit" pour mettre mettre l'index dans le repository local puis "git push" pour mettre à jour github. Il existe un tas de tuto sur le sujet.

        "La première sécurité est la liberté"

        • [^] # Re: chaud

          Posté par  . Évalué à 1.

          Justement, je voudrais les exemples de chaque étape, y compris le premier.

          Je ne suis pas sur de comprendre. Tu voudrais par exemple un dépôt avec :

          • un fichier pour le langage sur les entiers avec AST codé par un variant ;
          • un fichier pour le langage étendu avec les booléens codé avec un GADT ;
          • des fichiers pour les mêmes langages mais codés selon la méthode tagless-final.

          C'est cela ? Afin de pouvoir mieux comparer les codes et les méthodes ?

          Les fichiers dont tu parles doivent être bien trop compliqué pour comprendre le principe.

          C'est pas faux. Sans avoir besoin d'avoir bien compris le principe de la méthode — ils sont avant tout là pour l'illustrer sur un exemple — il vaut mieux en avoir une idée au moins approximative dans un premier temps.

          J'ai codé pendant 2 ans en ocaml fonctionnel simple. Et tout ce qui est foncteur/module, et les opérateurs spécifiques (@@) me semblent bien étrange et peu lisible.

          Je n'ai toujours pas compris en quoi un module est si différent d'un objet ou d'une classe.

          Pour ce qui est de l'opérateur @@ c'est une question de goût personnel pour éviter d'avoir trop de parenthèses et séparer visuellement les fonctions de leurs arguments. Cela permet d'écrire :

          f @@ g @@ h @@ x
(* au lieu de *)
f (g (h x))

(* comme dans ce bout de code issu du journal *)
let lam f = fwd @@ I.lam @@ fun x -> bwd (f (fwd x))

(* que j'aurai pu tout aussi bien écrire *)
let lam f = fwd (I.lam (fun x -> bwd (f (fwd x))))

(* ou encore avec plus de @@ *)
let lam f = fwd @@ I.lam @@ fun x -> bwd @@ f @@ fwd x

          Pour ce qui est des modules par rapport aux objets, ils ont un point commun : ce sont des enregistrements extensibles; et on aurait pu faire la même chose avec des objets. C'est ce qu'à fait Philipp Wadler en 1998 quand il a proposé sa solution au problème de l'extension sur la liste de diffusion Java Generics. Mais il faut utiliser le vistor pattern, et je préfère l'approche du fold qui dans cette solution est jouée par le rôle des foncteurs. Un foncteur est au fond une fonction des modules vers les modules, c'est plus « fonctionnel » dans le principe. On peut écrire une signature de foncteur ainsi :

          module type F = S1 -> S2
(* ou S1 et S2 sont des signatures de modules *)

          Si tu te souviens des échanges sur le journal d'Aluminium qui présentait l'encodage de Böhm-Berarducci, celui de ce journal en est une généralisation. Voici le lien vers mon commentaire qui comparait cet encodage avec l'approche classique.

          L'encodage de Böhm-Berarducci, qui utilise des enregistrements, marche bien tant que le langage que l'on plonge a un seul type de données, comme le premier exemple qui n'a que des int. Mais il devient lourd, voir impossible à utiliser quand ce langage a plus d'un type de données : int, bool, fonctions… Alors au lieu d'utiliser des enregistrements, on utilise des modules (ou des objets) qui sont une généralisation et une abstraction supplémentaire au-dessus des enregistrements.

          Pour ce qui est du rapport entre le fold et le vistitor pattern de la POO, Perthmâd l'avait signalé dans la discussion et j'ai donné des liens en réponse à son commentaire.

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

          • [^] # Re: chaud

            Posté par  (site web personnel) . Évalué à 2.

            C'est cela ? Afin de pouvoir mieux comparer les codes et les méthodes ?

            Oui, un fichier pour chaque exemple, bien séparer. Pour pouvoir comparer les évolutions et les différences. Genre je suis bloqué sur le fold appliquée aux parenthèses, mais je bloque surtout sur le principe de précédence, plus que sur le code.

            Un foncteur est au fond une fonction des modules vers les modules, c'est plus « fonctionnel » dans le principe. On peut écrire une signature de foncteur ainsi :

            Mais pourquoi ?! En objet, c'est simplement une injection. Un composant d'un objet qui est construit à l’extérieur de celui-ci et donné en paramètre au constructeur. En quoi instancier un module en fixant un des type paramètre en fait une fonction ?

            Si tu te souviens des échanges sur le journal d'Aluminium qui présentait l'encodage de Böhm-Berarducci

            Oui, et j'ai toujours mal à la tête. Je pense réécrire mon langage de modalisation avec ce genre de technique. J'utilisais un bête AST. Faut que je relise tout à tête reposé.

            "La première sécurité est la liberté"

            • [^] # Re: chaud

              Posté par  . Évalué à 4. Dernière modification le 23 novembre 2016 à 14:40.

              La notion de foncteur a ses origines dans un domaine des maths appelé "théorie des catégorie". C'est une théorie très abstraite dans le sens qu'elle s'intéresse aux transformations qu'on peut faire entre différent pans des mathématiques, principalement.

              Les catégories sont construites à partir d'objets mathématiques (les ensembles, les classes, les théories mathématiques elle même (comme les groupes en algèbre abstraite - les groupes de symétrie entre les solutions du rubix-cube par exemple).

              Pour tenter de donner une idée d'une catégorie, mettons qu'on s'intéresse aux groupes de symétrie du Rubix-cube. La Catégorie_des_groupes c'est la donnée de tous les groupes et de toutes les transformations qu'on peut établir entre les groupes. Le groupe de symétrie du Rubix cube en est un des objet. La notion de Morphisme_de_groupes permet de définir comment on transforme un groupe en un autre groupe.

              Le second exemple de catégorie qu'on peux donner est la catégorie des ensembles, et là le rapport avec les langages de programmations fonctionnel sera plus apparent : La Catégorie_des_ensembles. Dans la catégorie des ensembles, les objets de base sont les ensembles (Les entiers naturels y sont au même niveau que le groupe de symétrie du rubix cube l'était dans la catégorie des groupes). Dans cette catégorie, les transformations qui transforment un ensemble en un autre ensemble sont … les fonctions. Les lambdas, quoi.

              Maintenant pour la notion de foncteur. Un foncteur est une généralisation de ce qu'est une fonction entre deux ensembles, mais pour les catégories. Le "domaine" d'un foncteur est une catégorie, son co-domaine est une autre catégorie. Mais comme on est dans un niveau d'abstraction supérieur, on ne peux pas se contenter de dire quelle est l'image d'un membre d'une catégorie - imaginons que l'image du groupe de symétrie du Rubix-Cube si notre catégorie domaine est la catégorie des groupe soit l'ensemble des entiers naturels - parce que les catégorie ne sont pas QUE ces objets. On doit aussi établir quels morphisme de groupe correspond à quelle fonction.

              Voilà pourquoi la notion de foncteur est intéressante quand on parle de langage de programmation et de compilation / optimisation : on peut avoir des foncteurs dont le "domaine" et le "co-domaine" sont la même catégorie, et comme un foncteur transforme dans ce cadre une fonction en fonction, on trouve naturellement un cadre théorique pour modéliser tout ça. C'est intéressant pour les théoriciens naturellement, parce que l'arsenal théorique des catégorie est applicable pour raisonner sur les programmes, et que le niveau d'abstraction est bon - ainsi, la notion de foncteur est implémentée dans Haskell par exemple, et son analogue (ou plutôt la manière dont c'est implémenté dans Ocaml) sont les modules. Comme les modules sont paramétrée par des type, en l'occurence un type de départ et un type d'arrivée, les fonction définies dans ce modules définissent de facto des foncteurs qui transforment les programmes en programme dans une représentation différente. Oui parce que le truc que j'ai pas dit à propos de la théorie des catégorie c'est qu'on choisit pas les transformations au hasard, on les choisit de manière à ce que certaines structures ou certains invariants soient préservés par les transformations entre les différentes catégories. C'est ce qui fait qu'elles sont intéressantes mathématiquement.

            • [^] # Re: chaud

              Posté par  . Évalué à 2. Dernière modification le 23 novembre 2016 à 17:35.

              Oui, un fichier pour chaque exemple, bien séparer. Pour pouvoir comparer les évolutions et les différences. Genre je suis bloqué sur le fold appliquée aux parenthèses, mais je bloque surtout sur le principe de précédence, plus que sur le code.

              Je vais voir ce que je peux faire pour mettre du code plus détaillé et commenté sur github. Je ne te promets rien, cela dépendra de mon temps libre.

              Pour le principe de précédence qu'est-ce qui te pose problème ? On a d'abord une fonction de mise entre parenthèse sous condition :

              let cparen b = if b then paren else (fun s -> s);;
val cparen : bool -> string -> string = <fun>

              Elle permet de retourner une fonction de type string -> string selon la valeur du booléen : soit cette fonction met des parenthèses si b = true, sinon c'est l'identité et on ne met pas de parenthèses. Ensuite pour le cas de l'addition, on a :

              let add x y = fun p -> cparen (p > 3) @@ show_add (x 3) (y 4)

              Autrement dit, tant que la priorité du contexte est ≤ 3 on ne met pas de parenthèse : 3 représente le degré de priorité de l'opérateur additif. Ensuite comme l'addition est associative à gauche, pour le membre de gauche on reste au degré 3 de l'addition, par contre pour le membre de droite on passe au degré suivant. C'est pour distinguer 1 + 2 + 3 == ((1 + 2) + 3) de 1 + (2 + 3) == (1 + (2 + 3)). Pour la multiplication, son degré de priorité est de 4 : la multiplication est prioritaire sur l'addition.

              Cela étant, c'est plus un code « standard » pour gérer la priorité des opérateurs en programmation fonctionnelle. Si tu ne vois pas trop pourquoi il fait ce qu'on lui demande, ce n'est pas très important pour le reste du journal.

              Mais pourquoi ?! En objet, c'est simplement une injection. Un composant d'un objet qui est construit à l’extérieur de celui-ci et donné en paramètre au constructeur. En quoi instancier un module en fixant un des type paramètre en fait une fonction ?

              J'ai du mal à comprendre où tu veux en venir, et je me suis peut être mal exprimé. Les implémentations de la signature d'un langage corresponde aux différentes interprétations du dit langage. Les foncteurs eux servent à écrire du code dans ses langages (comme les foncteurs d'exemples) ou à transformer les dits programmes (comme les optimiseurs). Pour moi, et comme l'a dit Thomas Douillard, c'est exactement le niveau d'abstraction qu'il me faut pour raisonner sur ce genre de problématique.

              Depuis que j'ai découvert cette méthode, et également suite aux discussions sur le journal de présentation de MetaOCaml, il y a deux comics xkcd qui résument bien mon état du moment :

              nerd snipping

              et celui-ci :

              purity

              J'ai essayé d'éviter le plus possible le recours au vocabulaire et aux concepts abstraits des mathématiques, mais ce n'est pas toujours évident.

              Pour ce qui est de l'approche final avec les objets de OCaml cela pourrait ressemblait au code suivant :

              (* on définit la symantique d'un langage avec litéraux
 * et addition comme un type d'objet paramétré par son interprétation *)
class type ['repr] symAdd = object
  method lit : int -> 'repr
  method add : 'repr -> 'repr
end

(* là on a des fonctions pour créer nos termes
 * du langage à partir de ses implémentations *)
let lit n = fun ro -> ro#lit n
let add x y = fun ro -> ro#add (x ro) (y ro)

(* un terme d'exemple *)
let t1 () = add (lit 1) (add (lit 2) (lit 3))

(* on implémente deux interprétations *)
class eval = object
  method lit n = (n:int)
  method add x y = x + y
end

class view = object
  method lit n = string_of_int n
  method add x y = "(" ^ x ^ " + " ^ y ^ ")"
end

(* on instancie un objet pour chacune *)
let eval = new eval
let view = new view

(* notre exemple est une fonction qui prend une
 * instance de classe, à la manière d'un foncteur *)
t1 () eval;;
- : int = 6

t1 () view;;
- : string = "(1 + (2 + 3))"

              Et pour étendre les langages, par exemple en rajoutant la multiplication, on fait de l'héritage entre objets :

              (* on ajoute un opérateur aux langages *)
class type ['repr] symMul = object
  method mul : 'repr -> 'repr -> 'repr
end

(* la nouvelle fonction pour écrire nos termes *)
let mul x y = fun ro -> ro#mul (x ro) (y ro)

(* on étend par héritage nos précédents interprètes *)
class evalM = object
  inherit eval
  method mul x y = x * y
end

class viewM = object
  inherit view
  method mul x y = "(" ^ x ^ " * " ^  y ^ ")"
end

(* on les instancie *)
let evalM = new evalM
let viewM = new viewM

(* un exemple de test *)
let t2 () = mul (add (lit 1) (lit 2)) (add (lit 3) (lit 4))

t2 () evalM;;
- : int = 21

t2 () viewM;;
- : string = "((1 + 2) * (3 + 4))"

              Cette façon de faire est plus proche de l'encodage en Haskell via les typeclasses.

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

              • [^] # Re: chaud

                Posté par  (site web personnel) . Évalué à 2.

                Merci c'est plus clair. Je dois encore comprendre ce que contiennent les functors de plus qu'une classe. D'un point de vue pratique, je veux dire.

                Est-ce le "code" est dupliqué pour chaque functor ? J'ai du mal à imaginer ce qui va se passer pour une grosse expression (genre un million de terme). Normalement, ocaml ne duplique rien.

                Mais dans le cas de "génération" d'une expression par lecture d'un fichier par exemple, il faut le faire pour chaque functor ? Comment partager une expression qui n'est pas statique ?

                "La première sécurité est la liberté"

                • [^] # Re: chaud

                  Posté par  . Évalué à 2.

                  Un Functor, c'est pas une classe, c'est au niveau d'abstraction d'une classe "template" en C++. Ça permet de lier n'importe quel type "d'entrée" qui respecte certaines propriétés à un type de sortie qui maintient certaines de ces propriétés de manière générique.

                  Du coup pour ce qui est des passes d'optimisation ça permet de les écrire de manière générique et de les chaîner un peu comme tu veux. Dans les articles, ils disent que ce niveau de généricité permet de rendre le système de type content, ce qui serait très compliqué à faire avec des simples classes à ce niveau de généricité - mais j'avoue que ça reste un peu flou pour moi et que je suis pas capable d'expliquer en quoi exactement :) Notamment au niveau de la réutilisation de langage pour en faire des extensions : admettons qu'on ait un langage qui soit complètement implémenté, pour rajouter des constructions sans duplication de code, c'était pas possible jusqu'à présent. La il s'agit simplement d'étendre le module. Mais … pour poser ces questions tu as lu les articles non ?

                  • [^] # Re: chaud

                    Posté par  (site web personnel) . Évalué à 3.

                    Ça permet de lier n'importe quel type "d'entrée" qui respecte certaines propriétés à un type de sortie qui maintient certaines de ces propriétés de manière générique.

                    Tu peux faire la même chose avec des paramètres de constructeur qui fournissent une classe concrète d'un type abstrait interne, non ? La seul différence est que tu es emmerdé si le type abstrait "ressort" de ta classe, car cela veut dire des casts moche.

                    Du coup pour ce qui est des passes d'optimisation ça permet de les écrire de manière générique et de les chaîner un peu comme tu veux.

                    Faut que je rerelise cette partie de toute façon.

                    Mais … pour poser ces questions tu as lu les articles non ?

                    Pas tous, non. J'ai déjà du mal avec le tien :)

                    "La première sécurité est la liberté"

              • [^] # Re: chaud

                Posté par  (site web personnel) . Évalué à 4.

                J'aimerais bien l'avis de kantien sur ces 2 problèmes :

                Est-ce le "code" est dupliqué pour chaque functor ? J'ai du mal à imaginer ce qui va se passer pour une grosse expression (genre un million de terme). Normalement, ocaml ne duplique rien.
                Mais dans le cas de "génération" d'une expression par lecture d'un fichier par exemple, il faut le faire pour chaque functor ? Comment partager une expression qui n'est pas statique ?

                "La première sécurité est la liberté"

                • [^] # Re: chaud

                  Posté par  . Évalué à 1.

                  Je ne suis pas certain de comprendre tes questions.

                  Est-ce le "code" est dupliqué pour chaque functor ?

                  Un foncteur c'est une fonction qui prend des modules comme paramètres et qui renvoie un module (qui pourrait lui-même être un foncteur d'ailleurs). Le système des modules avec ses foncteurs est au fond un langage fonctionnel mais non turing-complet, il est proche du lambda-calcul simplement typé (en). Qu'entends-tu par le code dupliqué pour chaque foncteur ? Il y aura de l'allocation à chaque application du foncteur, mais tout comme avec n'importe quelle application de fonction. Par exemple :

                  let f i = i + 1

let i = f 1
let j = f 2

                  ici, à chaque fois que l'on applique f on alloue de la mémoire pour stocker le résultat dans i et j. C'est pareil avec les foncteurs.

                  Mais dans le cas de "génération" d'une expression par lecture d'un fichier par exemple, il faut le faire pour chaque functor ?

                  Une expression c'est un terme d'un langage. Pour pouvoir l'interpréter, il faut le mettre dans un foncteur paramétré par un module d'interprétation, et en appliquant le foncteur tu obtiendras l'interprétation de ton choix.

                  Comment partager une expression qui n'est pas statique ?

                  Via la directive include. Par exemple si tu as un terme t, tu peux faire :

                  module T(I : SYM) = struct
  let t = (* la désérialisation de ton terme *)
end

                  Et si tu veux l'utiliser avec un autre terme t', tu fais :

                  module T' (I : SYM) = struct
  include T(I)
  let t' = (* expression qui comporte t *)
end

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

                  • [^] # Re: chaud

                    Posté par  (site web personnel) . Évalué à 3.

                    Je viens de comprendre que tu n'as jamais de représentation en mémoire, donc si l'expression est généré dans les faits, la génération est "refaite" à chaque type d’interprétation (eval ou pretty print)

                    "La première sécurité est la liberté"

                    • [^] # Re: chaud

                      Posté par  . Évalué à 2. Dernière modification le 25 novembre 2016 à 11:37.

                      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.

  • # Usage autre des GADTs ?

    Posté par  (site web personnel) . Évalué à 2.

    Merci pour cet article pour le moins étendu et détaillé.

    Petite coquille ? "Lorsque l'on a supprimé les littéraux nuls, on a au fond transformer" J'ai un doute sur "transformer" qui me semblerait plus judicieux en "transformé".

    J'avais lu l'article de Oleg Kiselyov à ce propos et je trouve l'approche tagless très élégante.

    Maintenant j'aurais deux questions, une plus générique et une plus orientée OCaml.

    a) Hormis dans le cas d'un arbre syntaxique pour évaluer des expression pour faire un compilateur, est-ce que tu vois un autre usage des GADTs ? Cela fait partie des fonctionnalités qui me frustrent car elles apparaissent très puissantes mais au final je ne trouve jamais l'occasion de m'en servir.

    b) Est-ce que les modules OCaml peuvent être vu comme un sur-ensemble ou un sous-ensemble (ou rien à voir) des typeclasses d'Haskell.

    • [^] # Re: Usage autre des GADTs ?

      Posté par  . Évalué à 1.

      Petite coquille ? "Lorsque l'on a supprimé les littéraux nuls, on a au fond transformer" J'ai un doute sur "transformer" qui me semblerait plus judicieux en "transformé".

      Effectivement, petite faute d'accord. Si un modérateur pouvait corriger. J'en ai repéré une autre avec un seul « t » au lieu de deux à littéraux : « La première optimisation que l'on va voir est celle qui consiste à supprimer tous les litéraux nuls ».

      J'avais lu l'article de Oleg Kiselyov à ce propos et je trouve l'approche tagless très élégante.

      Sur son site on trouve également une lecture où il expose encore plus en détail toutes les possibilités de l'approche et en Haskell. Les fichiers de code sont accessibles ici.

      Hormis dans le cas d'un arbre syntaxique pour évaluer des expression pour faire un compilateur, est-ce que tu vois un autre usage des GADTs ? Cela fait partie des fonctionnalités qui me frustrent car elles apparaissent très puissantes mais au final je ne trouve jamais l'occasion de m'en servir.

      Les possibilités des GADT mériteraient plus d'un journal pour être présentées. La leçon de Jeremy Yallop sur le sujet illustre des cas d'usage qui vont bien au-delà de l'écriture de compilateur.

      b) Est-ce que les modules OCaml peuvent être vu comme un sur-ensemble ou un sous-ensemble (ou rien à voir) des typeclasses d'Haskell.

      Je dirais un sur-ensemble : tout ce que font les typeclasses peuvent être fait avec les modules, mais la réciproque ne marche pas — il me semble. Pour les différents niveaux d'abstraction accessibles en OCaml, il y a ces deux leçons de Leo White : abstraction et parametricty.

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

  • # Curryfication

    Posté par  . Évalué à 1.

    Bonjour !
    Avant tout je voudrais te remercier pour ce super journal, instructif et très pédagogique (ce qui a certainement demandé beaucoup de temps de ta part).

    Une modeste contribution pour la curryfication (il faut voir si c'est instructif ou non).

    Une fonction est caractérisée par un ensemble de définition (son domaine), un ensemble d'arrivée (son codomaine) et une relation univoque entre un élément du domaine vers un élément du codomaine. Lorsque l'on traite des fonctions de plusieurs variables, le domaine est constitué de n-uplets ou tuples. Le principe de la curryfication consiste à se ramener, dans ce cas, à des fonctions d'une seule variable.

    Il est dommage de construire directement des exemples dans des langages (ocaml/python) qui traitent les fonctions comme des valeurs directement. En langage mathématique, la distinction est plus nette et il est à mon avis plus lisible de comparer A × B -> C et A -> EncodeFonction(B,C), avec A, B, C et EncodeFonction(B,C) qui sont des ensembles « normaux ».

    Cela revient à dire :

    A × B -> C =~= A -> EncodeFonction (B,C)

    En théorie des ensembles on écrit souvent B^C pour parler de cet objet qui encode une fonction de B vers C.

    En python ou en caml, on ne travaille jamais vraiment avec des fonctions, mais toujours avec des codes qui représentent ces fonctions (ordinateur oblige), ainsi, la traduction est « déjà faite », et il suffit de produire une « fonction python ». L'égalité devient 

    EncodeFonction (A × B, C)  === EncodeFonction (A, EncodeFonction (B,C))

    La transformation se fait très naturellement par la suite, et de manière générique (naturelle) en B,

    def bijection (codeFonction1):
    codeFonction2 = lambda a: (lambda b: codeFonction(a,b)) # dans EncodeFonction (A, EncodeFonction (B,C))
    return codeFonction2

    Notons que cela se base sur la capture d'arguments (l'argument a est utilisable dans la fonction dont l'argument est b).
    Cette construction est un cas particulier d'adjonction.

    • [^] # Re: Curryfication

      Posté par  . Évalué à 2.

      Avant tout je voudrais te remercier pour ce super journal, instructif et très pédagogique (ce qui a certainement demandé beaucoup de temps de ta part).

      De rien. Cela m'a demandé effectivement du temps, mais il me fut avant tout profitable à moi même. En vertu du principe : « ce qui se conçoit bien, s'explique bien », il me fallait d'abord bien comprendre la méthode pour pouvoir l'expliquer. Ensuite, s'il peut être utile aux lecteurs du site : c'est du bonus, et c'est pour cela que je partage ma compréhension de la technique.

      Une modeste contribution pour la curryfication (il faut voir si c'est instructif ou non).

      Ton explication est tout à fait correcte, et elle code un principe général de curryfication pour des fonctions sur des couples. Elle explicite un isomorphisme (du moins un des sens) entre les fonction sur des couples et leurs versions curryfiées. C'est au fond ce que l'on fait en mathématique lorsque l'on pratique des applications partielles sur des fonctions de deux variables en en fixant une et en faisant varier la seconde.

      Après j'ai choisi l'approche de comparaison avec python pour ne pas trop rentrer dans des détails formels sur le principe de la curryfication. Ce passage était surtout là pour montrer qu'en rendant le contexte explicite, via la curryfication, alors on pouvait se ramener au cas d'un fold ce qui est nécessaire pour utiliser la technique tagless final. Cette question avait amené de long échanges entre toi et Nicolas Boulay dans ton journal, c'est pour cela que je voulais la traiter. D'autant que j'avais besoin du code obtenu pour la suite du journal. L'exemple du pretty printing est d'ailleurs emprunté à la vidéo de ton journal. ;-)

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

  • # Un cas que gère le tagless mais pas les GADT

    Posté par  (site web personnel) . Évalué à 2.

    Ton approche m'a faite rejouer avec les GADTs et les l'approche tagless finale et je viens enfin de résoudre un problème vieux comme le monde pour moi.

    Je veux representer des expressions, genre "1 + 2 * x", qui peuvent contenir une "variable". Cela nous donne un ADT assez simple (Je le fais en Haskell, ce sera plus lisible que si je le faisais en OCaml, principalement parce que le Haskell est plus lisible, mais surtout parce que je ne maîtrise pas du tout l'écriture du OCaml et donc je ferais des erreurs ;):

    data Expr = Add Expr Expr | Lit Int | Variable

    L'expression "1 + x" précédente étant représentée par Add (Lit 1) Variable.

    Je veux pouvoir évaluer mon expression :

    eval :: Expr -> Int
eval (Lit i) = i
eval (Add e e') = eval e + eval e'
eval Variable = error "cannot evaluate a variable"

    Suivez mon regard, j'aimerais dégager ce cas particulier. On va passer aux GADT pour représenter tout cela :

    data Expr useVariable where
    Add :: Expr aUseVariable -> Expr bUseVariable -> Expr (FOr aUseVariable bUseVariable)
    Lit :: Int -> Expr SansVariable
    Variable :: Expr AvecVariable

    Derrière se cache une fonction au niveau du type FOr :

    type family FOr a b where
   FOr AvecVariable _ = AvecVariable
   For _ AvecVariable = AvecVariable
   For _ _ = SansVariable

    Et ça cela marche, le type de Variable est bien Expr AvecVariable, le type de Add (Lit 1) (Lit 2) est bien Expr SansVariable et le type de Add Variable (Lit 4) est bien Expr AvecVariable.

    Revenons à notre fonction eval :

    eval :: Expr SansVariable -> Int
eval (Lit i) = i
eval (Add e e') = eval e + eval e'

    Le type marque clairement que on ne peut évaluer qu'une expression SansVariable. Et le cas Variable n'est plus à écrire puisque il n'existe plus. Cependant cela ne marche pas. Pourquoi ?

    Parce que Haskell (GHC 8.0) n'est pas capable de prouver que si (Add e e') est Expr SansVariable, alors e et e' le sont aussi. La preuve est triviale pour nous en regardant la fonction FOr, mais pas pour GHC.

    Est-ce que OCaml sait faire ça ?

    Comment feriez vous sinon ?

    Note: la méthode TagLess final marche bien ici puisqu'il suffit de ne pas écrire d’implémentation d'eval pour Variable et le compilateur refusera de compiler un appel à eval sur un type qui contient des Variable. C'est cool ;)

    • [^] # Re: Un cas que gère le tagless mais pas les GADT

      Posté par  . Évalué à 3.

      OCaml n'a pas de "type families" dans ce sens; pour définir une fonction sur les types au cas par cas, on voit la fonction comme une relation entre types (donc un type paramétré ('input1, 'input2, 'output) f_or), et on définit un GADT correspondant à cette relation—dont les habitants sont les témoins dynamiques.

      type open = Open
type closed = Closed
type ('a, 'b, 'c) f_or =
  | Left : (open, _, open)
  | Right : (_, open, open)
  | Closed : (closed, closed, closed)

      C'est en inspectant cette valeur-témoin que tu guides le raisonnement par cas.

      Note cependant que je trouve l'idée de faire une distinction entre deux cas "open" et "closed" très artificielle. On met en valeur les limites des GADTs, qui est qu'il faut penser au moment de la définition de son type à tous les usages dans les types (les fonctions depuis ses valeurs vers les types) dont on va avoir besoin. Il me semblerait plus naturel et plus général d'avoir un typage plus général Expr Env où Env est une représentation, au niveau des types, de l'ensemble des variables libres de l'expression—une représentation assez courante est d'utiliser des emboîtements de Maybe pour "compter" le nombre de variable libres connues dans le terme: Expr (Maybe (Maybe (Maybe a)))) pour un terme à quatre variable libres connues, le type vide pour un environnement clos, et par exemple Add : Expr a -> Expr a -> Expr a et Lam : Expr (Maybe a). Ça reste difficile à utiliser et donc un choix à faire avec soin—j'aurais pour ma part tendance à préférer soit une représentation moins typée soit l'usage d'un langage mieux pensé pour les types riches comme Coq ou Idris.

  • # Joli journal

    Posté par  . Évalué à 5.

    Bon journal; en particulier, le fait de montrer les étapes intermédiaires et "ce qui se fait sans cette technique" me semble très utile pour la compréhension. L'inconvénient bien sûr, c'est que le résultat est très long, trop long je pense pour que quelqu'un qui découvre puisse confortablement le lire en une seule fois. Il faut espérer que les gens ont la discipline de faire des pauses et de reprendre la suite un autre jour, même si la structure ne l'encourage pas forcément. Pour la suite, je t'encouragerais à écrire plusieurs journaux séparés (par exemple un journal par partie de haut niveau), étalés de quelque jours.

    As-tu envisagé de le convertir en un tutoriel sur Zeste de Savoir ? C'est un site avec de bonnes valeurs d'ouverture et de diffusion de la connaisance, une équipe sympathique, et plus adaptée au stockage à long terme des connaissances que les journaux de LinuxFR, il me semble.

    Points de détail:

    • Quand tu dis que le typage des GADTs n'est pas "décidable", tu veux dire qu'il n'est pas "inférable": c'est le fait de deviner le type qui n'est pas décidable, pas le fait de vérifier qu'un type donné est correct (qui est ce qu'on entend par "typage décidable").

    • Un pointeur complémentaire sur les GADTs, francophone, serait le cours de Programmation Fonctionnelle Avancée de Roberto di Cosmo (ou des autres enseignants ayant donné le même cours à Paris 7).

    • [^] # Re: Joli journal

      Posté par  . Évalué à 1.

      Merci pour ton commentaire.

      L'inconvénient bien sûr, c'est que le résultat est très long, trop long je pense pour que quelqu'un qui découvre puisse confortablement le lire en une seule fois. Il faut espérer que les gens ont la discipline de faire des pauses et de reprendre la suite un autre jour, même si la structure ne l'encourage pas forcément.

      Effectivement, l'article est long et dense. Il faudra y revenir plus d'une fois pour les lecteurs qui voudraient le comprendre. Et encore, j'ai fait des coupes : au départ j'abordais la problématique de l'héritage multiple par exemple. J'ai hésité, également, à le couper en plusieurs journaux mais j'ai finalement choisi cette forme en me disant que le lecteur le lirai plus d'une fois.

      As-tu envisagé de le convertir en un tutoriel sur Zeste de Savoir ? C'est un site avec de bonnes valeurs d'ouverture et de diffusion de la connaisance, une équipe sympathique, et plus adaptée au stockage à long terme des connaissances que les journaux de LinuxFR, il me semble.

      Je ne connaissais pas, j'y réfléchirai. Pour un tutoriel comme celui-ci, c'est sans doute une bonne idée.

      Quand tu dis que le typage des GADTs n'est pas "décidable", tu veux dire qu'il n'est pas "inférable": c'est le fait de deviner le type qui n'est pas décidable, pas le fait de vérifier qu'un type donné est correct (qui est ce qu'on entend par "typage décidable").

      Effectivement je me suis mal exprimé, je voulais bien dire que c'est l'inférence qui est indécidable dans le cas général pour les GADT. Vérifier la correction d'une preuve, c'est toujours décidable. Trouver une preuve, en revanche… ;-)

      Un pointeur complémentaire sur les GADTs, francophone, serait le cours de Programmation Fonctionnelle Avancée de Roberto di Cosmo (ou des autres enseignants ayant donné le même cours à Paris 7).

      Merci pour la référence, je n'y avais pas pensé. Pourtant je me suis rendu plus d'une fois sur le site de Roberto Di Cosmo.

      Au passage, une question qui n'a rien à voir avec le thème du journal. Sais-tu pourquoi les where statement ont disparu du langage OCaml ? Je pense à cela car dans le cours de Paris 7, il y a une leçon sur les zipper, et dans son article sur le sujet Gérard Huet en faisait usage. Je trouve cette perte dommage, cela permet d'écrire des codes plus élégants, et la beauté dans le code c'est important ! Comme il répondait dans un interview, sur le blog de la SIF (Société Informatique de France), intitulée Poésie et esthétisme du logiciel :

      — Binaire : […] Mais tu as dépassé l’état de le compréhension. Tu nous parles d’esthétique : un programme informatique peut-il être beau ?

      —Gérard Huet : Bien sûr. Son rôle est d’abord d’exposer la beauté de l’algorithme sous-jacent. L’esthétique, c’est plus important qu’il n’y paraît. Elle a des motivations pratiques, concrètes. D’abord, les programmes les plus beaux sont souvent les plus efficaces. Ils vont à l’essentiel sans perdre du temps dans des détails, des circonvolutions inutiles. Et puis un système informatique est un objet parfois très gros qui finit par avoir sa propre vie. Les programmeurs vont et viennent. Le système continue d’être utilisé. La beauté, la lisibilité des programmes est essentielle pour transmettre les connaissances qui s’accumulent dans ces programmes d’une génération de programmeurs à l’autre qui ont comme mission de pérenniser le fonctionnement du système.

      Pour les programmes, de même que pour les preuves, il ne faut jamais se satisfaire du premier jet. On est content quand ça marche, bien sûr, mais c’est à ce moment là que le travail intéressant commence, qu’on regarde comment nettoyer, réorganiser le programme, et c’est souvent dans ce travail qu’on découvre les bonnes notions. On peut avoir à le réécrire tout ou en partie, l’améliorer, le rendre plus beau.

      Et je suis bien d'accord avec lui : un théorème vrai, c'est important. Mais une belle démonstration l'est tout autant ! Elle permet de mieux saisir les raisons profondes de la vérité du résultat et d'éclairer son harmonie sous-jacente.

      On est accoutumé à nommer beauté les propriétés évoquées des figures géométriques aussi bien que des nombres […] C'est bien plutôt une démonstration de telles propriétés que l'on serait en droit de nommer belle, parce que, par son intermédiaire, l'entendement comme pouvoir des concepts et l'imagination comme pouvoir de leur présentation a priori se sentent renforcés (ce qui, combiné avec la précision que donne la raison, se nomme l'élégance de la démonstration); car, en tout ceci, du moins la satisfaction, bien que le fondement s'en trouve dans des concepts, est-elle subjective, tandis que la perfection implique une satisfaction objective.

      Kant, Critique de la faculté de juger.

      Et comme les programmes sont des preuves. :-)

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

      • [^] # Re: Joli journal

        Posté par  . Évalué à 4.

        Sur la question de where, il y a deux niveaux de réponse.

        1. Pourquoi ça a été enlevé. Ça a été enlevé parce que Xavier Leroy a conçu Caml Light comme un sous-ensemble simplifié du Caml existant à l'époque, en retirant tout ce qui lui semblait peu utilisé en pratique ou redondant. Donc where a sauté parce qu'on avait déjà let pour faire la même chose.

        2. Pourquoi ça n'a pas été remis. J'aime bien where aussi et si j'étais convaincu de pouvoir fournir une argumentation solide pour le remettre, je l'aurais fait. Le problème c'est que where pose plein de questions délicates sur les précédences de la grammaire qui n'ont pas de réponses claires—je m'en suis rendu compte en implémentant une extension de syntaxe pour where, pa_where. let <p> = <e1> in <e2> est une construction qu'on peut appeler "ouverte à droite", il y a un délimiteur qui ferme la construction sur la gauche mais pas sur la droite (comme if <e1> then <e2> else <e3> ou d'autres, mais au contraire de begin <e> end qui n'est ouvert d'aucun côté). Au contraire, <e1> where <p> = <e2> est ouverte à gauche; mélanger des constructions ouvertes à gauche et ouverte à droite pose de nombreux problèmes de précédence à décider. Par exemple, quelle est la signification de let x = e1 in e2 where y = e3 ? Un autre cas délicat est la gestion du and qui est commun à where et let: let x1 = e1 where x2 = e2 and x3 = e3 in e4, à qui est attaché le and ?

        Dans un langage à indentation significative, on a beaucoup moins de problèmes de précédence puisque le parenthésage apporté par l'indentation ferme beaucoup plus les constructions. C'est un avantage notable de ces langages en terme d'évolutions possibles de la syntaxe.

        • [^] # Re: Joli journal

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

          Je dois avouer que je n'ai jamais creusé la question. Mais les premières questions qui me viennent à l'esprit sont : comment le mot-clé where était-il géré avant sa disparition ? comment font-ils en Haskell ?

          Ensuite pour ce qui relève de son intérêt et de son utilité : la construction est certes redondante avec la forme let res = let x = e1 in e2, mais d'un autre côté écrire let res = e2 where e2 = e3 permet de comprendre au premier coup d'œil où l'on veut en venir. C'est du même acabit que lorsque dans mon journal j'ai traité la question du pretty printing. En commençant par écrire la conclusion à laquelle je voulais arriver, il me semble plus simple de comprendre le développement qui s'ensuit. Tandis que si je n'avais pas procédé ainsi, le lecteur se serait sans doute demandé où je voulais en venir. C'est souvent ce qui m'arrive avec la forme let ... in lorsqu'elle sert à définir des termes auxiliaires : une fois arrivée à la fin, je dois reprendre la lecture pour comprendre.

          Pour ce qui est de la gestion de la précédence : pourquoi ne pas mettre les let et where au même niveau et les voir comme une parenthèse ouvrante pour le premier et une parenthèse fermante pour le second ? Cela ne marche pas ? N'est-ce pas ce que tu as fait dans ton extension de syntaxe ?

          Pour les cas que tu proposes, je les lis ainsi :

          let x = y + 1 in 2 * x where y = 3
(* devient *)
let y = 3 in let x = y + 1 in 2 * x

let x1 = x2 + x3 where x2 = 1 and x3 = 2 in 2 * x1
(* devient *)
let x2 = 1 and x3 = 2 in let x1 = x2 + x3 in 2 * x1

          Une petite précision terminologique : j'ai tendance à qualifier de syntaxique ce genre de problématique, et de réserver le qualificatif grammatical pour ce qui relève des problématiques de typage. Pour comparer avec le domaine de la physique, l'équation P = U * I² est syntaxiquement correcte mais grammaticalement erronée car il n'est pas possible d'unifier le deux membres de l'équation : ils n'ont pas la même unité de mesure; ce qui en fait une proposition vide de sens.

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

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.