A single GADT constructor accepting some specific type parameters?

Learning
1

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 es? 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 eand 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
2

The simple approach is to use a type variable:

type _ term =
  | Bool : bool -> bool term
  | Int : int -> int term
  | ...
  | If : bool term * 'a term * 'a term -> 'a term
3

I’d like to statically ensure that Ite cannot be of type a t but only f t or e t.

4

Mmm. Well, you could do this:

type _ e_or_f =
  | E : e e_or_f
  | F : f e_or_f

type _ t =
  ...
  | If : 'a e_or_f * f t * 'a t * 'a t -> 'a t

Which is structurally very similar to having two If constructors, of course.

Expressing arbitrary refinements in this way can get quite ugly and mechanism heavy, so be aware that you might be in for some work if the design has to change.

5

Indeed this is isomorphic to my first example.
As a matter of fact, I’d prefer this:

type a = [ `A ]
type e = [ `E ]
type f = [ `F ]
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 t * 'a t * 'a t -> ([< `E | `F ] as 'a) t

Then:

utop # Ite (True, True, True);;
- : f t = Ite (True, True, True)
utop # Ite (True, Sort "s", Sort "t");;
- : e t = Ite (True, Sort "s", Sort "t")
utop # Ite (True, True, Sort "s");;
Error: This expression has type e t but an expression was expected of type f t
       Type e = [ `E ] is not compatible with type f = [ `F ] 
       These two variant types have no intersection
utop # Ite (True, True, Num 5);;
Error: This expression has type a t but an expression was expected of type f t
       Type a = [ `A ] is not compatible with type f = [ `F ] 
       These two variant types have no intersection
utop # Ite (True, Num 5, Num 3);;
Error: This expression has type a t but an expression was expected of type
         ([< `E | `F ] as 'a) t
       Type a = [ `A ] is not compatible with type [< `E | `F ] as 'a 
       These two variant types have no intersection

But I seem to remember that using polymorphic variants and subtyping inside GADTs is not recommended at all. Or is it?

6

I tried this a while ago, and did run into some trouble with subtyping. I can’t say I remember the exact details.

I do remember that you run into trouble when writing functions like this:

let rec is_truthy : [< `E | `F ] t -> bool =
  function
  | Sort _ -> false
  | All _ -> false
  | True -> true
  | False -> false
  | Ite (_, a, b) -> is_truthy a && is_truthy b

where the parameter needs to be locally abstract, but also needs to be constrained to being some polymorphic variant type.

There may well be other difficulties that I am forgetting or was never aware of.

7

Right, thanks for this example.