An ordinary variant gives every constructor the same return type. A GADT lets each constructor fix the type parameter to something specific, so the type checker learns facts about a value just from which constructor built it. This builds up from a typed expression evaluator to a typed printf, which is the example that actually needs everything GADTs provide.
Turning it on
Unlike Haskell, OCaml needs no language pragma at all: GADT syntax has been part of the language since 4.00. The only thing to opt into is the syntax itself - a colon and a concrete return type per constructor, instead of a shared type variable.
The problem an ordinary variant cannot express
A plain variant for a small expression language. Every constructor produces the same expr, regardless of what it computes.
type expr =| Int of int| Bool of bool| Add of expr * expr| If of expr * expr * expr
Nothing stops a nonsensical term from being built. An interpreter for this type has to handle cases that should be impossible, at runtime, with a failure path.
let bad = Add (Bool true, Int 1) (* typechecks fine *)let rec eval = function| Int n -> `Int n| Bool b -> `Bool b| Add (l, r) ->(match eval l, eval r with| `Int a, `Int b -> `Int (a + b)| _ -> failwith "type error at runtime") (* the case we want gone *)| If (c, t, e) ->(match eval c with| `Bool true -> eval t| `Bool false -> eval e| _ -> failwith "type error at runtime")
A typed expression GADT
Same language, indexed by the OCaml type of the value it produces. Each constructor's return type is expr followed by a concrete type argument, not a shared type variable.
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 : 'a expr * 'a expr -> bool expr
Add (Bool true, Int 1) is now a compile error, not a runtime failure. The constructor's declared type requires int expr on both sides.
Error: This expression has type bool exprbut an expression was expected of type int exprType bool is not compatible with type int
The evaluator, with no failure case anywhere. eval\'s own return type is \'a, tied to the expr\'s index, and every branch produces exactly the type the pattern proves it must.
let rec eval : type a. a expr -> a = function| Int n -> n| Bool b -> b| Add (l, r) -> eval l + eval r| If (c, t, e) -> if eval c then eval t else eval e| Eq (l, r) -> eval l = eval r
A well-typed program by construction: if it builds, it evaluates without a type error, because the constructors that could produce one do not exist.
let prog = If (Eq (Int 1, Int 1), Add (Int 2, Int 3), Int 0)# eval prog;;- : int = 5
The type: type a. annotation, and why it is required
eval above needed let rec eval : type a. a expr -> a = function rather than a plain type signature. This is not stylistic. Without it, OCaml's ordinary type inference tries to unify a single 'a across every branch of the match, which cannot work when each branch locally refines that variable to something different.
What happens without the annotation.
let rec eval = function| Int n -> n| Bool b -> b (* rejected: unifies with the int branch above *)| ...
The error, which is really OCaml telling you it cannot generalize inside the match without help.
Error: This expression has type bool but an expression wasexpected of type int
type a. introduces a fresh, locally abstract type for the duration of the function, which is what lets each branch instantiate it differently while still proving the same universal statement about eval as a whole.
let rec eval : type a. a expr -> a = function ...
With more than one indexed parameter, list them all after type.
let rec compare_expr : type a. a expr -> a expr -> int = fun l r -> ...
Refutation: cases the checker proves cannot occur
A length-indexed vector, using Peano-style phantom types to carry the length in the type itself.
type z = Ztype 'n s = Stype (_, _) vec =| Nil : ('a, z) vec| Cons : 'a * ('a, 'n) vec -> ('a, 'n s) vec
A safe head that only accepts a vector proven non-empty. There is no Nil case to write, because (\'a, \'n s) vec has no constructor that produces Nil - the type checker can see that the pattern match is exhaustive without it.
let head : type a n. (a, n s) vec -> a = function| Cons (x, _) -> x(* no Nil case needed: Nil : ('a, z) vec, which does not unify with (a, n s) vec *)
Confirm it really is exhaustive - compile with warnings as errors and there is no complaint about a missing pattern.
$ ocamlfind ocamlopt -package none -w +8 -warn-error +8 -c vec.ml
Calling head on a value the type system already knows is empty is rejected before head ever runs.
# head Nil;;
The rejection, which is a real type error rather than a wildcard match failure at runtime.
Error: This expression has type ('a, z) vecbut an expression was expected of type ('b, 'c s) vecType z is not compatible with type 'c s
A second use of refutation: equality witnesses
A GADT that is itself a proof: a value of (a, b) eq exists only when a and b are the same type, and its single constructor is the reflexivity proof.
type (_, _) eq = Refl : ('a, 'a) eq
cast uses the witness to change a value\'s apparent type, safely - the only way to construct eq at all is Refl, which only typechecks when the two sides are already equal, so cast can never be misused to coerce unrelated types.
let cast : type a b. (a, b) eq -> a -> b =fun Refl x -> x
A runtime type representation, and a total type-equality check built on it. This is the pattern behind Dynamic/Typeable-style libraries.
type _ ty =| TInt : int ty| TBool : bool ty| TList : 'a ty -> 'a list tylet rec eq_ty : type a b. a ty -> b ty -> (a, b) eq option =fun a b ->match a, b with| TInt, TInt -> Some Refl| TBool, TBool -> Some Refl| TList a, TList b ->(match eq_ty a b with| Some Refl -> Some Refl| None -> None)| _ -> None
Using it: a heterogeneous cell that only unpacks if the requested type matches what was actually stored.
let try_cast : type a b. a ty -> b ty -> b -> a option =fun want have x ->match eq_ty have want with| Some Refl -> Some x| None -> None# try_cast TInt TInt 5;;- : int option = Some 5# try_cast TInt TBool true;;- : int option = None
Existentials: hiding the index
A GADT indexed by a type is precise but closed: a list of exprs all has to share one index. Packing the index away with an existential lets a collection hold values of genuinely different, unknown types, at the cost of no longer being able to recover that type without more work.
A box hiding which type expr is indexed by. Note the constructor's own type variable a, existentially quantified rather than a parameter of the box type itself - that is what makes it existential rather than universal.
type any_expr = Any : 'a expr -> any_expr
Now a heterogeneous list is possible, at the price of the specific type being erased at each element.
let exprs : any_expr list =[ Any (Int 1); Any (Bool true); Any (Add (Int 2, Int 3)) ]
Unpacking one still lets you compute with it, since eval only needs to know the value is well-typed at some type, not which one.
let show (Any e) =match e with| Int _ -> Printf.sprintf "int: %d" (eval e)| Bool _ -> Printf.sprintf "bool: %b" (eval e)| _ -> "expr"
What you lose: the type a is not in scope outside the match that destructures Any, so you cannot write a function returning \'a expr option and expect the caller to know what \'a is.
(* will not typecheck: a escapes its scope *)let unpack (Any e) = e
GADTs plus polymorphic variants: a small interpreter
Extend the expression language with variables and a typed environment, using a GADT to key the environment itself.
type _ var =| VInt : int var| VBool : bool vartype _ 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| Var : string * 'a var -> 'a expr
A heterogeneous environment, using the same box-and-witness pattern from section 5 to answer lookups safely.
type binding = B : string * 'a var * 'a -> bindingtype env = binding listlet rec lookup : type a. string -> a var -> env -> a =fun name want env ->match env with| [] -> failwith ("unbound: " ^ name)| B (n, have, value) :: rest ->if n = name thenmatch have, want with| VInt, VInt -> value| VBool, VBool -> value| _ -> failwith ("type mismatch on " ^ name)else lookup name want rest
The evaluator, extended by one case, unchanged everywhere else.
let rec eval : type a. env -> a expr -> a =fun env -> function| Int n -> n| Bool b -> b| Add (l, r) -> eval env l + eval env r| If (c, t, e) -> if eval env c then eval env t else eval env e| Var (name, v) -> lookup name v env
Running it.
let env : env = [ B ("x", VInt, 10); B ("flag", VBool, true) ]let prog = If (Var ("flag", VBool), Add (Var ("x", VInt), Int 1), Int 0)# eval env prog;;- : int = 11
A typed printf, built from nothing
This is the example that needs the whole toolkit at once: a GADT indexed by both the arguments a format string still expects and the type its final consumer returns, so %d and %s compose into a function type the compiler checks against the call site.
The format GADT. (input, output) fmt means: apply a function of type input to get output. %d prepends an int argument; Lit appends a literal string with no argument; End closes the format at type r -> r.
type (_, _) fmt =| Int : ('r, 'r) fmt -> (int -> 'r, 'r) fmt| Str : ('r, 'r) fmt -> (string -> 'r, 'r) fmt| Lit : string * ('r, 'r) fmt -> ('r, 'r) fmt| End : ('r, 'r) fmt
Interpreting a format into an actual function, by structural recursion on the GADT. Each case both consumes one piece of the format and produces exactly the function arity the type says it must.
let rec sprintf : type a r. (a, string -> r) fmt -> a =fun fmt -> failwith "see full version below"
The version that actually compiles, carrying an accumulator through the recursion since the result is built left to right.
let rec run : type a r. (a, r) fmt -> (string -> r) -> a =fun fmt k ->match fmt with| End -> k ""| Lit (s, rest) -> run rest (fun acc -> k (s ^ acc))| Int rest -> fun n -> run rest (fun acc -> k (string_of_int n ^ acc))| Str rest -> fun s -> run rest (fun acc -> k (s ^ acc))let sprintf fmt = run fmt (fun s -> s)
A format value, built by hand rather than parsed from a string literal - this is the same object OCaml's own %d %s syntax desugars to internally.
let fmt = Lit ("x=", Int (Lit (", y=", Str End)))# sprintf fmt;;- : int -> string -> string = <fun># sprintf fmt 5 "hi";;- : string = "x=5, y=hi"
The type of sprintf fmt is exactly int -> string -> string, inferred from the shape of fmt itself, not written down anywhere. Passing the arguments in the wrong order or with the wrong type is a compile error at the call site, not a runtime format mismatch.
# sprintf fmt "hi" 5;;
Which fails exactly the way a normal type error fails - because by this point it is one.
Error: This expression has type string but an expressionwas expected of type int
Where this stops paying off
Explicit type annotations become mandatory the moment recursion is involved, as seen with type a. throughout. A GADT match without one produces a confusing unification error rather than a clean one.
(* This compiles: *)let rec eval : type a. a expr -> a = function ...(* This does not, even though it looks equivalent: *)let rec eval e = match e with ...
Existentials erase the type they hide, so a function receiving an any_expr cannot recover a expr and return it - the pattern in section 6 that will not typecheck is not a bug, it is the actual boundary of what existential packing gives you.
(* still will not typecheck, and for the same reason as before *)let identity (Any e) : any_expr = Any e (* this one is fine *)let unwrap (Any e) : 'a expr = e (* this one is not *)
The shape of it: reach for an ordinary variant first, and move to a GADT only once you have a concrete invalid state you want gone at compile time rather than checked at runtime - a mismatched pair of operands, an out-of-bounds index, an environment lookup at the wrong type. Every example here started as the plain variant with a failwith in it, and the GADT is what removed the failwith. For the same technique applied to writing code rather than data, see ppx in Practice, where a deriver walks the AST instead of a value.