GADT

also: gadts, generalized algebraic data type

Generalized Algebraic Data Type: an ADT whose constructors may each refine the type parameter of the value they build, instead of every constructor sharing one polymorphic return type. This lets a single well-typed eval return an int for an Add node and a bool for an Eq node, checked at compile time rather than by an unchecked cast.

An ordinary variant gives every constructor the same return type, so a term language and its evaluator cannot agree on anything. Add (Bool true, Int 1) typechecks, and eval has to return a tagged union and fail at runtime.

A GADT writes the return type of each constructor explicitly, and that type may be more specific than the declared parameter. $Int : int \to int expr$ but $Eq :^{'} a expr \times^{'} a expr \to bool expr$ . Matching on a constructor now tells the typechecker what the parameter was, which is what lets one function return an int in one branch and a bool in another.

The evaluator that cannot be written without one. The `type a.` annotation is required: it makes the function polymorphic in the recursive calls, which is what lets each branch refine `a` differently.

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

Compiled with ocamlopt 4.14.1. Three calls to one function, three different result types, no tag check anywhere.

eval (Add (Int 2, Int 3))              ->  5
eval (Eq (Int 2, Int 2))               ->  true
eval (If (Eq (Int 1, Int 1), Int 10, Int 20))  ->  10

The cost is that inference gives up: OCaml will not guess a GADT's type, so annotations become mandatory rather than optional, and exhaustiveness checking gets harder for the compiler to report usefully.