Re: Dans l'art voluptueuse de ne rien comprendre

Où sinon, plutôt que de mettre un constructeur en plus dans ton langage (qui ne correspond sans doute à rien dans ta grammaire), il y a peut être moyen de mixer les GADT avec un usage plus « standard » des types fantômes. Comme dans cet exemple :

module GADT = struct
 type (_,_) term =
 | Lit : int -> (int,_) term
 | Add : (int,_) term * (int,_) term -> (int,_) term
 | Mult : (int,_) term * (int,_) term -> (int,_) term
 | Div : (int,_) term * (int,[`NZ]) term -> (int,_) term
 let rec eval:type a b. (a,b) term -> int = function
 | Lit n -> n
 | Add (t,t') -> (eval t) + (eval t')
 | Mult (t,t') -> (eval t) * (eval t')
 | Div (t,t') -> (eval t ) / (eval t')
 let lit n = Lit n
 let add t t' = Add (t,t')
 let mult t t' = Mult (t,t')
 let div t t' = Div (t,t')
 let square_add_one t:(int,[`NZ]) term = (add (mult t t) (lit 1))
end
open GADT;;
let t1 = square_add_one (lit (-3));;
val t1 : (int, [ `NZ ]) term = Add (Mult (Lit (-3), Lit (-3)), Lit 1)
let t2 = lit 23;;
val t2 : (int, '_a) term = Lit 23
let t3 = div t2 t1;;
val t3 : (int, '_a) term = Div (Lit 23, Add (Mult (Lit (-3), Lit (-3)), Lit 1))
eval t1, eval t2, eval t3;;
- : int * int * int = (10, 23, 2)
(* et si tu veux convertir au bon type dans la REPL, tu peux faire *)
((lit 4):>(int, [`NZ]) term);;
- : (int, [ `NZ ]) term = Lit 4

Ainsi tu n'obtiendras des termes non nuls qu'à partir de fonctions dont tu es certain que c'est ce qu'elles produisent.

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