GADTs

With normal variants, eval can't return different types per constructor.

28.1 Motivation: a typed expression language

With normal variants, eval can't return different types per constructor. GADTs let each constructor specify its return type index.

type a. a expr -> a is a locally abstract type with polymorphic annotation — required for functions over GADTs (polymorphic recursion + type refinement).

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
  | Pair : 'a expr * 'b expr -> ('a * 'b) expr
  | Fst : ('a * 'b) 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
  | If (c, t, e) -> if eval c then eval t else eval e
  | Eq (x, y) -> eval x = eval y
  | Pair (a, b) -> (eval a, eval b)
  | Fst p -> fst (eval p)

let r : int = eval (If (Eq (Int 1, Int 1), Add (Int 2, Int 3), Int 0))   (* 5 *)
(* Add (Int 1, Bool true) is rejected at compile time! *)

28.2 Existential types

Type variables appearing only in arguments are existentially hidden:

type printable = Printable : 'a * ('a -> string) -> printable

let items = [ Printable (42, string_of_int); Printable ("hi", Fun.id) ]
let print_all = List.iter (fun (Printable (v, show)) -> print_endline (show v))

28.3 Type equality witness

type (_, _) eq = Refl : ('a, 'a) eq
let cast : type a b. (a, b) eq -> a -> b = fun Refl x -> x
(* Stdlib 5.1+: Type.eq and Type.Id for runtime type identifiers *)

28.4 Length-indexed vectors (type-level naturals)

type z = Z
type 'n s = S

type (_, _) vec =
  | Nil : ('a, z) vec
  | Cons : 'a * ('a, 'n) vec -> ('a, 'n s) vec

let head : type a n. (a, n s) vec -> a = function Cons (x, _) -> x
(* head Nil does not type-check; no runtime error possible *)

let rec map : type a b n. (a -> b) -> (a, n) vec -> (b, n) vec = fun f -> function
  | Nil -> Nil
  | Cons (x, xs) -> Cons (f x, map f xs)

28.5 Refutation and exhaustiveness

let only_cons : type a. (a, z s) vec -> a = function
  | Cons (x, Nil) -> x
  (* Nil case is impossible; the compiler knows. You can write: | _ -> . *)

28.6 Typed format strings, heterogeneous lists

type _ hlist =
  | [] : unit hlist
  | ( :: ) : 'a * 'b hlist -> ('a * 'b) hlist

let l : (int * (string * (bool * unit))) hlist = [1; "two"; true]

28.7 Practical GADT uses

Typed DSLs / interpreters, typed SQL query builders Protocol state machines ((open_, closed) door)

Efficient unboxed representations, typed printf (Printf uses GADTs internally: CamlinternalFormatBasics)

Type-safe heterogeneous maps (Hmap, Univ_map)