Say I want to create a GADT t
for terms, the latter being of 3 different sorts (say a
, e
and f
). Now is there a way to state than one constructor may only accept f
or e
s? I know how to do this with two different constructors (see Ite_f
and Ite_e
below) but I wondered if there is another good practice to handle this kind of situations (from what I gathered, using polymorphic variants for f
and e
and then playing with subtyping is discouraged when using GADTs).
type e (* expressions *)
type f (* formulas *)
type a (* arithmetic terms *)
type 'a t =
Num : int -> a t
| Sort : string -> e t
| True : f t
| False : f t
| All : string * e t * f t -> f t
| Ite_f : f t * f t * f t -> f t (* can I get a *single* Ite constructor *)
| Ite_e : f t * e t * e t -> e t