Evaluation d'expressions & gestion des types

L'auteur de ce sujet a trouvé une solution à son problème.
Auteur du sujet

Bonjour/soir,

J'ai un type (simplifié ici) représentant des expressions arithmétiques:

1
2
3
4
5
type exp =
  | Int   of int
  | Float of float
  | Var   of string
  | Add   of (exp * exp)

Si je veux évaluer mes expressions:

1
2
3
4
5
let rec eval env = function
  | Int x     -> x
  | Float x   -> x (* boom *)
  | Var v     -> (* ... *)
  | Add (x,y) -> (* re-boom *)

Le problème c'est que je ne peux pas renvoyer un int ou un float.
J'ai pensé à wrapper le retour de eval mais je suis pas vraiment fan de l'idée:

1
2
3
4
5
let rec eval env = function
  | Int x     -> `Int x
  | Float x   -> `Float x
  | Var v     -> (* ... *)
  | Add (x,y) -> (* ... *)

Une autre solution serait de séparer mes expressions entières et flottantes:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
type op =
  | If of (bool_exp * exp * exp)
and exp =
  | Int_exp of int_exp
  | Float_exp of float_exp
and int_exp =
  | Int of int
  | Var of string
  | Add of (int_exp * int_exp)
and float_exp =
  | Float of float
  | FVar of string
  | FAdd of (float_exp * float_exp)

Mais là ça devient le bordel au niveau des noms des constructeurs (puis c'est surtout que j'écris presque 2 fois la même chose, notamment pour mes fonctions d'évaluation)…
Voilà, je sais pas trop comment faire puisqu'aucune solution ne me semble vraiment correcte. En fait, j'ai l'impression que je m'y prends mal ^^ .

+0 -0

Salut,

je vois deux conceptions possibles. La première est de convertir tous tes Int en Float. La deuxième est de considérer que ce sont deux types indépendants qui ne peuvent pas co-exister (à moins de faire appel explicitement à des fonctions de conversion) et ça revient à ta séparation en expressions entières et flottantes. Sauf que tu peux éviter ta duplication de code en utilisant le polymorphisme paramétrique :

1
2
3
4
type 'a exp =
  | Scalar of 'a
  | Var of string
  | Add of ('a exp * 'a exp)

Petit test :

1
2
Add (Scalar 1.3, Scalar 3.7);;
- : float exp = Add (Scalar 1.3, Scalar 3.7)

Édité par Catamorphisme

+0 -0
Auteur du sujet

@Catamorphisme: J'y avais pensé, sauf que ça merde lorsque j'écris le parser (avec menhir). J'ai des règles paramétriques et j'arrive pas à faire marcher tout ça ^^ .

Sinon je fais un truc du genre:

1
2
3
4
5
module Type = struct
  type t =
    | Int of int
    | Float of float
end

Et j'ai ce que je veux, plus ou moins:

1
2
3
4
let rec eval env = function
  | Int of x -> Type.Int x
  | Float of f -> Type.Float f
  (* ... *)
+0 -0

Cette réponse a aidé l'auteur du sujet

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).

+1 -0
Auteur du sujet

Woah, merci pour cette réponse détaillée, j'irai voir les GADTs de plus près. Du coup je vais préciser plus en détail ce que je cherche à faire (d'ailleurs j'aurais du commencer par ça).

Mon but est de pouvoir générer des fichiers au format DIMACS-CNF.

J'ai donc besoin de définir un langage de "haut niveau" qui me permette de générer des clauses. Par exemple:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
$a = [a ; b ; c] ;; un set contenant les variables a, b et c
$b = [b ; ~d] ;; un set contenant les variables b et non d
$c = card($a) ;; $b = 3

bigand $i, $j in $a, $b do
  $i | $j ;; | represente un OU
end

;; le bigand ci-dessus est equivalent a
;; bigand $i in $a do
;;   bigand $j in $b do
;;     $i | $j
;;   end
;; end

Avec ça, j'ai $$((a \lor b) \land (a \lor \neg d)) \land ((b \lor b) \land (b \lor \neg d)) \land ((c \lor b) \land (c \lor \neg d))$$ Je simplifie/transforme ensuite (si nécessaire) en CNF et je génère mon fichier DIMACS.

En fait, je sais pas vraiment quelle tête devrait avoir mon AST ni comment évaluer tout ça. Je peux toujours faire un truc du genre:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
module Ast = struct
  type t =
    | Unit
    | Int of int
    | Float of float
    | Term of string
    | Var of (string * t option)
    | Set of t list
    | Card of t
    | Bigand of (t * t * t)
    | Bigor of (t * t * t)
    | And of (t * t)
    | Or of (t * t)
    | Xor of (t * t)
    | Implies of (t * t)
    | Equiv of (t * t)
    | Top
    | Bottom
    | Add of (t * t)
    (* ... *)
end

module Type = struct
  let t =
    | Unit
    | Int
    | Float
    | Bool
    | Clause
    | Set
end

let toplevel = Hashtbl.create 10

let rec eval = function
  | Ast.Int x -> Ast.Int x, Type.Int
  | Ast.Float x -> Ast.Float x, Type.Float
  | Ast.Var (x, None) ->
      try Hashtbl.find toplevel x
      with Not_found -> failwith ("unbound variable: " ^ x)
  | Ast.Var (x,Some y) -> 
      if Hashtbl.mem toplevel x then
        Hashtbl.replace toplevel x (eval y)
      else
        Hashtbl.add toplevel x (eval y) ; Unit, Type.Unit
  | Bigand (x,y,z) as b -> eval_bigand [] b
  (* ... *)
and eval_bigand env = function
  | Bigand (vars, sets, body) -> (* ... *)

Sachant qu'après évaluation je dois me retrouver avec quelque chose du genre
And (Or (Term "a", Term "b"), Not (Term "c")).

Édité par olzd

+0 -0
Auteur du sujet

J'ai commencé à jouer avec les GADTs mais j'ai un problème:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
module Value = struct
  type _ t =
    | Int   : int    -> int    t
    | Float : float  -> float  t
    | Bool  : bool   -> bool   t
    | Var   : string -> string t

  let compare : type a. a t -> a t -> int = fun x y ->
    match x, y with
    | Int a, Int b     -> Pervasives.compare a b
    | Float a, Float b -> Pervasives.compare a b
    | Bool a, Bool b   -> Pervasives.compare a b
    | Var a, Var b     -> Pervasives.compare a b
end

module ValueSet = Set.Make(Value)

J'ai ça comme erreur:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
Error: Signature mismatch:
       ...
       Type declarations do not match:
         type 'a t =
           'a Value.t =
             Int : int -> int t
           | Float : float -> float t
           | Bool : bool -> bool t
           | Var : string -> string t
       is not included in
         type t
       File "ast2.ml", line 2, characters 7-127: Actual declaration
       They have different arities.

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)

(* ... *)

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à.

Édité par olzd

+0 -0

Salut,

J'ai pas énormément d'expérience avec les GADTs mais comme tu n'as plus beaucoup de réponses je vais tenter ma chance.

J'ai commencé à jouer avec les GADTs mais j'ai un problème:

1
2
3
4
5
6
7
module Value = struct
  type _ t = (* ... *)

  let compare : type a. a t -> a t -> int = (* ... *)
end

module ValueSet = Set.Make(Value)

J'ai ça comme erreur:

1
2
3
4
5
6
7
8
Error: Signature mismatch:
       ...
       Type declarations do not match:
         type 'a t = (* ... *)
       is not included in
         type t
       File "ast2.ml", line 2, characters 7-127: Actual declaration
       They have different arities.

Ça me semble effectivement normal, la signature demande ici un type sans paramètre. D'ailleurs, si on pouvait faire ce que tu as écris, la signature de add permettrait a priori d'ajouter d'abord une valeur construite avec Float, puis une autre construite avec Int, or ta fonction de comparaison ne sait pas traiter deux valeurs construites avec un constructeur différent.

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).

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.

Tu voulais peut-être faire quelque chose dans ce goût-là ?

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
type _ value =
  | Int   : int ->   int value
  | Float : float -> float value

module ValueSet = struct

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

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

  type _ t =
    | FromIntSet   : IntSet.t   -> int t
    | FromFloatSet : FloatSet.t -> float t

  let add : type a. a value -> a t -> a t = fun v s ->
    (match v with
     | Int v'   -> (match s with | FromIntSet s' ->   FromIntSet (IntSet.add v' s'))
     | Float v' -> (match s with | FromFloatSet s' -> FromFloatSet (FloatSet.add v' s')))

  let mem : type a. a value -> a t -> bool = fun v s ->
    (match v with
     | Int v'   -> (match s with | FromIntSet s'   -> IntSet.mem v' s')
     | Float v' -> (match s with | FromFloatSet s' -> FloatSet.mem v' s'))

  (* ... *)

end

(* Exemple : *)
let i = Int 10 in
ValueSet.(
  let s = FromIntSet IntSet.empty in
  let s' = add i s in
  mem i s'
)

Note qu'il y a peut-être moyen de faire ça plus joliment.

+0 -0
Auteur du sujet

Salut,

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.

Ok, j'avais pas vraiment compris que c'était juste un tag. Par contre avec ta solution il faut réécrire les fonctions add, mem… Après je vois pas trop comment éviter ça.

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.

+0 -0

Cette réponse a aidé l'auteur du sujet

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.

Édité par anonyme

+0 -0
Auteur du sujet

Ta solution est intéressante, j'aurais jamais pensé à introduire les types final et non_final. Après je suis d'accord que convertir en float n'est pas du tout satisfaisant comme solution. En fait, j'étais arrivé à un truc comme ça;

1
2
3
4
5
type _ exp =
  | Int : int -> int exp
  | Float : float -> float exp
  | Add : int exp * int exp -> int exp
  | FAdd : float exp * float exp -> float exp

Du coup ça règle le problème mais je duplique mes constructeurs.

+0 -0

Effectivement, tu perds ici l'intérêt du constructeur Add unique, et tant qu'à partir comme ça, autant avoir deux types classiques int_exp et float_exp. Par ailleurs, il me semble que c'est un problème orthogonal au final : ici tu résous juste le choix de l'opérateur pour additionner, que ma solution plus haut règle en gardant le tag ont/float pour les expressions évaluées.

+0 -0
Vous devez être connecté pour pouvoir poster un message.
Connexion

Pas encore inscrit ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte