GADTs

A GADT lets each constructor fix the type parameter: type _ expr = Int : int -> int expr | Bool : bool -> bool expr | Add : int expr * int expr -> int expr | If : bool expr * 'a expr * 'a expr -> 'a expr.

Matching a constructor refines the type: in the Int n branch, the compiler knows 'a = int. That is how eval : type a. a expr -> a returns an int in one branch and a bool in another.

The annotation type a. introduces a locally abstract type and makes the function polymorphic in it, which GADT matching needs.

Ill-typed programs cannot be built: Add (Bool true, Int 1) is rejected at compile time, so eval needs no runtime type checks.

GADTs also encode existential types (hiding a type inside a constructor) and type-safe printf-style formats.

type _ expr =
  | Int : int -> int expr
  | Bool : bool -> bool expr
  | Add : int expr * int expr -> int expr
  | If : bool expr * 'a expr * 'a expr -> 'a expr
  | Eq : int expr * int expr -> bool expr

let rec eval : type a. a expr -> a = function
  | Int n -> n
  | Bool b -> b
  | Add (x, y) -> eval x + eval y
  | If (c, t, e) -> if eval c then eval t else eval e
  | Eq (x, y) -> eval x = eval y

let () =
  print_endline (string_of_int (eval (If (Eq (Int 2, Add (Int 1, Int 1)), Int 10, Int 20))));
  print_endline (string_of_bool (eval (Eq (Int 1, Int 2))))