Re: Dans l'art voluptueuse de ne rien comprendre

D'ailleurs, est-ce que dans les gadt, on peut mettre no propre type fantome ?

Je ne vois pas trop ce que tu veux, les GADT sont des types fantômes : on les appelle aussi first-class phantom type.

Tu veux un truc dans le genre ?

module GADT = struct
 type _ term =
 | Lit : int -> int term
 | Add : int term * int term -> int term
 | Div : 'a term * [`NZ] term -> 'b term
 | Nz : 'a term -> [`NZ] term
 let rec eval:type a. a term -> int = function
 | Lit n -> n
 | Nz t -> eval t
 | Add (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 div t t' = Div (t,t')
 let nz t = assert (eval t <> 0); Nz t
end
open GADT;;
let t1 = add (lit 3) (lit 2);;
val t1 : int GADT.term = Add (Lit 3, Lit 2)
let t2 = lit 3;;
val t2 : int GADT.term = Lit 3
let t3 = div t2 t1;;
Error: This expression has type int GADT.term
 but an expression was expected of type [ `NZ ] GADT.term
 Type int is not compatible with type [ `NZ ]
let t3 = div t2 (nz t1);;
val t3 : '_a GADT.term = Div (Lit 3, Nz (Add (Lit 3, Lit 2)))
eval t1, eval t2, eval t3;;
- : int * int * int = (5, 3, 0)
nz t3;;
Exception: Assert_failure ("gadt.ml", 17, 13).

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