Evaluation d'expressions & gestion des types

Pour ta première solution, tu ne pourras pas l'utiliser pour écrire une fonction eval qui renvoie directement un int ou un float. Éventuellement, tu peux avoir (j'oublie les variables) :

1
2
3
4
5
6
7
8

let rec eval = function
  | Int n -> Int n
  | Float n -> Float n
  | Add (e1, e2) ->
    match eval e1, eval e2 with
    | Int a, Int b -> Int (a + b)
    | Float a, Float b -> Float (a +. b)
    | _ -> failwith "eval"

Cette fonction va « réduire » les noeuds Add, jusqu'à n'avoir plus qu'un noeud Int ou Float dans ton arbre. Si jamais ton arbre est mal construit (il mélange flottants et entiers), tu auras une erreur à l'exécution. Tu ne peux pas vraiment faire mieux. Ensuite, tu peux avoir des fonctions unbox_int et unbox_float qui prennent respectivement en paramètre un Int n et un Float n et te donnent le n correspondant (et échouent sur les autres constructeurs, ce qui leur permet d'être bien typé).

La solution de catamorphisme ne te permettra pas non plus d'avoir eval, pour une raison encore plus simple : les valeurs du type exp ne gardent plus aucune information sur le type (entier ou flottant) de l'expression que tu manipules, tu ne peux donc pas savoir quel opérateur utiliser pour écrire le cas Add. D'ailleurs, rien ne t'empêche de construire une string exp avec le type qu'il propose, ou n'importe quelle autre chose qui n'aurait pas de sens par rapport à la définition que tu as en tête. Par contre, tu peux écrire des fonctions eval_int et eval_float, qui restreignent le type de l'expression d'entrée. L'avantage par rapport à la solution précédente, c'est qu'ici les vérifications ne sont plus dynamiques, mais statiques : tu ne peux plus mélanger des Int et des Float dans une expression (le type te l'interdit), et il est alors possible de type précisément chaque expression bien construite (et de refuser les autres à compile time), donc de vérifier statiquement que les appels à eval_{int,float} se font bien sur des expressions qui ont le bon type. L'inconvénient, c'est que tu retrouves de la duplication de code : tu es obligé de coder plusieurs fonctions eval différentes. Ça peut se simplifier en remarquant qu'elles ont toutes la même structure (c'est un fold sur ton arbre), et qu'on peut donc les coder en utilisant une seule fonction eval_generic : ('a -> 'a -> 'a) -> 'a exp -> 'a qui prend en paramètre un opérateur que tu peux utiliser pour le cas Add. Tu as ensuite let eval_int = eval_generic ( + ) and eval_float = eval_generic ( +. ). Ça devrait normalement fonctionner correctement avec Menhir : si tu n'y arrives pas, tu peux montrer un code minimal pour qu'on voie ce qui ne va pas.

Ta dernière solution revient presque exactement à la première que j'ai développée, sauf qu'au lieu d'utiliser le même type exp pour les expressions « évaluées », tu as un type qui représente ces expressions évaluées. C'est une amélioration de ta première solution.

La solution finale pour faire ce que tu souhaites demande d'utiliser des GADT. Le code peut alors ressembler à ça

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20

type _ eval_exp =
  | EInt : int -> int eval_exp
  | EFloat : float -> float eval_exp

type _ exp =
  | Int : int -> int exp
  | Float : float -> float exp
  | Add : 'a exp * 'a exp -> 'a exp

let rec eval : type a. a exp -> a eval_exp = function
  | Int n -> EInt n
  | Float n -> EFloat n
  | Add (a, b) ->
    match (eval a, eval b) with
    | EInt x, EInt y -> EInt (x + y)
    | EFloat x, EFloat y -> EFloat (x +. y)

let full_eval : type a. a eval_exp -> a = function
  | EInt n -> n
  | EFloat n -> n

Je ne vais pas m'étendre là dessus très longtemps, juste le mentionner pour que tu voies que ça existe et que tu te renseignes dessus si ça t'intéresse. L'idée est d'attacher des informations/contraintes de type aux constructeurs de exp, que le pattern matching peut ensuite utiliser pour s'assurer que le filtrage est bien exhaustif. Ici, tout est vérifié statiquement, et tu n'as qu'une seule fonction eval à écrire (qui est ici découpée en deux, mais ça revient au même).

J'avais oublié l'existence de l'article Detecting use-cases for GADTs in OCaml, mais c'est une bonne lecture sur le sujet (et d'ailleurs, son exemple d'utilisation correspond presque exactement au tien).

Bon, je m'y attendais un peu mais du coup je dois faire un truc du genre:

1 2 3 4 5 6 7 8 9 10 11

module IntSet = Set.Make(struct type t = int Value.t let compare = Pervasives.compare end) module FloatSet = Set.Make(struct type t = float Value.t let compare = Pervasives.compare end) (* ... *)

Je ne sais pas si c'est ce que tu voulais mais ici, on est d'accord que tu vas comparer par exemple Value.Int 0 avec Value.Int 2 et non 0 avec 2 ? Bon, Pervasives.compare semble «bien» se comporter de ce point de vue là en testant rapidement donc admettons (pas trouvé de source qui explique comment Pervasives.compare se comporte avec les constructeurs, avec une recherche rapide).

Si je ne dis pas de bêtise, un constructeur défini avant un autre est considéré comme inférieur, et en cas de constructeur identique on compare les paramètres avec une sorte d'ordre lexicographique. Ce qu'il faut retenir, c'est qu'en pratique c'est relativement utilisable quand on sait qu'on n'a pas besoin d'un comportement précis mais juste d'une fonction de comparaison qui marche (par exemple pour mettre dans un Set), mais que si on veut faire les choses de façon propre c'est effectivement une bonne idée de la définir soi-même (ou d'utiliser ppx_deriving pour l'avoir pour pas cher).

Mais ça m'oblige à écrire:

1 2 3 4 5 6

module Exp = struct type _ t = | ISet : int Value.t list -> IntSet.t t | FSet : float Value.t list -> FloatSet.t t (* ... *) end

D'ailleurs je trouve étrange de pouvoir écrire Exp.ISet [Value.Int 1; Value.Int 2] et de voir que j'ai IntSet.t Exp.t comme type puisque je ne manipule pas vraiment de Set là.

Le type utilisé pour décorer t dans Exp est juste un «tag». Ça ne veut pas dire que tu as une valeur du type en question. La valeur que tu obtiens est bien du type IntSet.t Exp.t mais le fait que ce soit IntSet.t à cette position dit juste qu'elle a été construite avec le constructeur ISet plutôt que le constructeur FSet. Du coup, je ne pense pas que c'était ce que tu voulais faire.

Le nom habituellement utilisé est « type fantôme » : c'est effectivement un paramètre de type qui ne correspond à aucun paramètre des valeurs de ton type exp, mais qui sert à faire vérifier au typeur certaines propriétés. Tu peux lire ça (c'est assez bien fait) ou chercher « type fantôme ocaml ».

D'ailleurs je suis tombé sur un autre truc gênant:

1 2 3 4 5 6 7 8 9

type _ exp = | Int : int -> int exp | Float : float -> float exp | Add : 'a exp * 'a exp -> 'a exp let rec eval : type a. a exp -> a = function | Int x -> x | Float x -> x | Add (x,y) -> (* (eval x) + (eval y) ou (eval x) +. (eval y) *)

Et là, c'est vraiment chiant. Une solution serait de tout convertir en float.

Une solution serait d'écrire :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21

type final
type non_final

type (_, _) exp =
  | Int : int -> (int, final) exp
  | Float : float -> (float, final) exp
  | Add : ('a, 'b) exp * ('a, 'c) exp -> ('a, non_final) exp

let rec eval : type a b. (a, b) exp -> (a, final) exp = function
  | Int x -> Int x
  | Float x -> Float x
  | Add (x, y) ->
    begin match eval x, eval y with
      | Int x', Int y' -> Int (x' + y')
      | Float x', Float y' -> Float (x' +. y')
    end

let full_eval : type a. (a, 'b) exp -> a = function x ->
  match eval x with
  | Int x -> x
  | Float x -> x

Tu remarqueras que j'ai utilisé un autre type fantôme qui indique si une expression est pleinement évaluée ou pas, ce qui me permet de ne pas avoir de warning sans avoir traité les motifs Int _, Add (_, _). Tu remarqueras aussi que le type a encore grossi : les GADT, c'est quelque chose de très rigolo et d'assez puissant, mais dans des programmes réels, il faut bien peser leur utilisation pour ne pas se retrouver avec des types énormes pour des vérifications dont on n'a pas besoin. Cela dit, ici on a un joli exemple de ce qu'on peut faire avec, donc si ça n'est pas trop pénible à utiliser dans le reste de ton code, ce serait dommage de s'en priver.

Mais dans tous les cas, ici tu n'as surtout pas envie de tout convertir en float : c'est tentant dans ce cas particulier parce qu'on a envie de dire que « int c'est des entiers et float des réels, et un entier ça peut bien être un réel », mais d'une part ce n'est pas tout à fait vrai, d'autre part tu pourrais vouloir avoir d'autres types complètement différents dans ton arbre (par exemple des string, et l'addition serait la concaténation), et ça n'est pas très satisfaisant de se dire que ça ne marche que parce qu'en agitant un peu les mains on peut faire semblant qu'un int c'est un float. Tout le principe de cette discussion est d'arriver à faire la différence proprement entre une expression entière et une expression flottante, après tout.

Note PS : dans le code que je t'ai donné, il n'est pas nécessaire de spécifier dans le type que Int et Float sont final. Par contre il est nécessaire de garder tout le reste, et notamment la définition d'un type final, pour dire que eval renvoie une expression d'un type différent de celui de Add (_, _). Et l'annotation type b. devient alors nécessaire pour une autre raison : dans le code ci-dessus, elle indique au typeur qu'il s'agit d'une récursion polymorphe, et là elle deviendrait nécessaire à cause des GADT. Ce sont des détails que je ne connais que superficiellement, et il est possible que la deuxième raison soit en fait aussi vraie dans le premier cas.