GADT

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) type-checks, and eval has to return a tagged union and fail at run time. A GADT writes the return type of each constructor explicitly, and that type may be more specific than the declared parameter^[1][2]. Matching on a constructor then tells the type checker what the parameter was, which lets one function return an int in one branch and a bool in another. GADTs were introduced around 2003 under several names: guarded recursive datatypes by Xi, Chen and Chen^[1], first-class phantom types by Cheney and Hinze^[3], and equality-qualified types by Sheard and Pasalic^[7]. GHC has supported them since 2006^[2] and OCaml since 2012^[4]. They generalize phantom types, whose parameter constrains callers but tells a pattern match nothing.

(* Each constructor states the type its value has: Int builds an int expr,
   Eq a bool expr, and If an expression of whatever type its branches have. *)
type _ expr =
  | Int : int -> int expr
  | Bool : bool -> bool expr
  | Add : int expr * int expr -> int expr
  | Eq : int expr * int expr -> bool expr
  | If : bool expr * 'a expr * 'a expr -> 'a expr
  | Pair : 'a expr * 'b expr -> ('a * 'b) expr
  | Fst : ('a * 'b) expr -> 'a expr
 
(* Matching on a constructor tells the type checker what a is in that
   branch, so each branch can return a value of a different type. *)
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
  | Pair (x, y) -> (eval x, eval y)
  | Fst p -> fst (eval p)

5
true
10
(2, false)
7

open Expr
let bad = Add (Bool true, Int 1)

File "ill.ml", line 2, characters 15-24:
2 | let bad = Add (Bool true, Int 1)
                   ^^^^^^^^^
Error: This expression has type bool Expr.expr
       but an expression was expected of type int Expr.expr
       Type bool is not compatible with type int

A constructor of a GADT can be read as a polymorphic function with a type equation attached^[2][6]. Eq has type $\mathtt{int}\mathtt{expr}\times \mathtt{int}\mathtt{expr}\to \mathtt{bool}\mathtt{expr}$, which is the same as

Building a value requires proving the equation, which holds only at bool expr. Matching on the constructor provides it: in the Eq branch of a match on an a expr, the type checker may assume $a=\mathtt{bool}$, so returning a bool where an a is expected is well typed.

A constructor whose result type is $a\mathtt{expr}$ for a variable $a$ carries no equation; if every constructor has this form, the type is an ordinary algebraic data type, or a phantom type if the parameter is unused.

Refinement also works in the other direction. A function on int expr need not handle Bool, Eq or Pair, because no value of type int expr can be built with them, and the compiler's exhaustiveness check knows this.

open Expr
 
(* Only constructors that can build an int expr need cases: Bool, Eq and
   Pair cannot, and the compiler knows it. *)
let rec size : int expr -> int = function
  | Int _ -> 1
  | Add (x, y) -> 1 + size x + size y
  | If (_, t, e) -> 1 + size t + size e
  | Fst _ -> 1

no warnings

Typed format strings

The type of printf depends on its format string. With a GADT indexed by the type of the function a format expects, a typed sprintf can be written as an ordinary function. OCaml's own format strings have been represented this way since version 4.02.

(* Typed format strings. The first parameter is the type of the function
   the format expects, the second the final result: ("x = %d", 'b) fmt has
   type (int -> 'b, 'b) fmt. *)
type (_, _) fmt =
  | Lit : string * ('a, 'b) fmt -> ('a, 'b) fmt
  | Int : ('a, 'b) fmt -> (int -> 'a, 'b) fmt
  | Str : ('a, 'b) fmt -> (string -> 'a, 'b) fmt
  | End : ('b, 'b) fmt
 
(* The result type of sprintf is computed from the format. *)
let sprintf (f : ('a, string) fmt) : 'a =
  let rec go : type a. string -> (a, string) fmt -> a =
   fun acc -> function
    | Lit (s, k) -> go (acc ^ s) k
    | Int k -> fun n -> go (acc ^ string_of_int n) k
    | Str k -> fun s -> go (acc ^ s) k
    | End -> acc
  in
  go "" f

hello Ada, you are 36 years old
2 + 3

Type representations and equality

A GADT a ty can describe the type a, one constructor per type former. Functions over it are generic: one show prints values of any represented type. The equality GADT, with the single constructor Refl : (a, a) eq, is a proof that two types are the same; matching on Refl makes the type checker use the equation. Together they give a type-safe cast and dynamically typed values that can be inspected safely^[3][8].

(* Type representations: a value of type a ty describes the type a. *)
type _ ty =
  | TInt : int ty
  | TString : string ty
  | TList : 'a ty -> 'a list ty
  | TPair : 'a ty * 'b ty -> ('a * 'b) ty
 
(* A proof that two types are equal: Refl can only be built at ('a, 'a). *)
type (_, _) eq = Refl : ('a, 'a) eq
 
let rec equal : type a b. a ty -> b ty -> (a, b) eq option =
 fun a b ->
  match (a, b) with
  | TInt, TInt -> Some Refl
  | TString, TString -> Some Refl
  | TList a, TList b -> (match equal a b with Some Refl -> Some Refl | None -> None)
  | TPair (a1, a2), TPair (b1, b2) -> (
      match (equal a1 b1, equal a2 b2) with Some Refl, Some Refl -> Some Refl | _ -> None)
  | _ -> None
 
(* A generic printer, driven by the representation. *)
let rec show : type a. a ty -> a -> string =
 fun t v ->
  match t with
  | TInt -> string_of_int v
  | TString -> Printf.sprintf "%S" v
  | TList t -> "[" ^ String.concat "; " (List.map (show t) v) ^ "]"
  | TPair (a, b) -> "(" ^ show a (fst v) ^ ", " ^ show b (snd v) ^ ")"
 
(* A dynamically typed value: a value packed with its type. *)
type dyn = Dyn : 'a ty * 'a -> dyn
 
let cast : type a. a ty -> dyn -> a option =
 fun t (Dyn (t', v)) -> match equal t' t with Some Refl -> Some v | None -> None

42
["a"; "b"]
(1, [2; 3])
the ints among them: [42]

Other uses

GADTs index data by properties such as length or balance, as in length-indexed vectors and red-black trees whose invariants are checked by the compiler, approaching dependent types; they type the syntax of embedded languages, including typed abstract syntax with variables represented by typed de Bruijn indices; and they describe the effects of an effect handler in OCaml, where type _ Effect.t is an extensible GADT indexed by each effect's result type.

The equations make inference hard. In a branch, the type checker has local assumptions such as $a=\mathtt{int}$, and the type of an unannotated function is no longer determined uniquely: a branch returning n could be of type int or of type a. Principal types can be lost, so both GHC and OCaml require annotations^[2][5][6]. GHC's OutsideIn(X) algorithm infers types only from information outside the branches and requires signatures on functions that match on GADTs^[6]; OCaml requires a locally abstract type, type a., for polymorphic recursion and for the result type to vary^[4][5].

type _ expr =
  | Int : int -> int expr
  | Bool : bool -> bool expr
 
(* Without the annotation "type a. a expr -> a" *)
let eval = function
  | Int n -> n
  | Bool b -> b

File "noannot.ml", line 8, characters 4-10:
8 |   | Bool b -> b
        ^^^^^^
Error: This pattern matches values of type bool expr
       but a pattern was expected which matches values of type int expr
       Type bool is not compatible with type int

Augustsson and Petersson described the idea in an unpublished note in 1994. Xi, Chen and Chen formalized guarded recursive datatype constructors in 2003^[1]; Cheney and Hinze's first-class phantom types^[3] and Sheard and Pasalic's equality-qualified types in the language Ωmega^[7] appeared at the same time. The name generalized algebraic data type came into use with Peyton Jones, Vytiniotis, Weirich and Washburn's inference algorithm, implemented in GHC 6.4 and published in 2006^[2], later refined into OutsideIn(X)^[6]. Garrigue and Le Normand added GADTs to OCaml 4.00 in 2012^[4], and Garrigue and Rémy gave their inference a principal-types account in 2013^[5].

• Phantom typeA phantom type is a type parameter that appears in a type's declaration but in none of its fields, used to keep otherwise identical representations apart: lengths in metres and in feet, validated and unvalidated strings, read-only and writable handles, SQL expressions of different result types. It carries no data and costs nothing at run time. Combined with an abstract type whose constructors are hidden, it lets a library enforce invariants through the type checker. Unlike a GADT index it tells a pattern match nothing; it constrains what callers may do, not what the compiler can learn.
• Dependent typeA dependent type is a type that may mention values, so that a vector's length can appear in its type and a function's result type can be computed from its arguments. Function types generalize to dependent products Π(x : A). B(x), and pairs to dependent sums Σ(x : A). B(x). Because types can express propositions and programs can be proofs, languages with dependent types, such as Agda, Coq (Rocq), Lean and Idris, double as proof assistants. The price is that type checking involves evaluating programs, so these languages require functions to terminate, and type equality is decided up to computation.
• Algebraic data typeAn algebraic data type is a type built from sums, where a value is one of several alternatives, and products, where a value has several components at once, possibly recursively. The name comes from counting: the number of values of a sum is the sum of the counts, and of a product their product, so types obey the laws of algebra. Values are taken apart by pattern matching, which the compiler checks for missing cases.
• Effect handlerAn effect handler runs code that may perform effects, and handles each effect by receiving it together with the continuation from the point where it was performed, which it can resume, discard or store. Handlers generalize exception handlers, and let generators, async I/O, schedulers, state and nondeterminism be written as libraries while the code that uses them stays in direct style. They come from the theory of algebraic effects of Plotkin, Power and Pretnar. OCaml 5 implements them with one-shot continuations: each can be resumed at most once, which keeps them cheap, since a continuation is the suspended stack itself.
• Polymorphic variantA polymorphic variant is a variant whose constructors, called tags and written with a backquote in OCaml, exist independently of any type declaration. Their types are sets of tags with bounds: [> `A] means at least `A, [< `A | `B] means at most those two, and unification works out unions and intersections of those sets using row variables. They let functions share constructors across types, be extended with new cases without editing old code, and encode subtyping, at the cost of longer types and error messages and of typos in open types going unnoticed.
• Constraint kindsConstraintKinds is the GHC extension that gives constraints their own kind, Constraint, so that the thing to the left of => becomes a first-class type-level entity that can be named with a synonym, passed as a parameter, returned by a type family, and stored in a data type. It lets a class leave to each instance what that instance needs of its element types, as when a container class requires Ord for sets and nothing for lists, and it lets dictionaries be packaged as ordinary values with Dict.
• Free monadThe free monad on a functor F is the monad whose values are trees of F-shaped instructions with results at the leaves: Pure a | Free (F (Free F a)). It adds exactly the monad structure and nothing else, so a program written in it is a description of a sequence of instructions that different interpreters can run, inspect or transform. Any mapping from F into a monad M extends uniquely to an interpreter from the free monad into M. Left-nested binds take quadratic time, which the Church-encoded form avoids.
• Red-black treeA red-black tree is a binary search tree whose nodes are coloured red or black so that no red node has a red child and every path from the root to a leaf passes through the same number of black nodes. The two rules keep the height at most 2 log2(n + 1), so search, insertion and deletion take O(log n) time. Red-black trees are an encoding of 2-3-4 trees as binary trees, and Okasaki's functional version reduces insertion to one rebalancing rule with four cases.
• Refinement typeA refinement type is a base type paired with a logical predicate that its values must satisfy, such as {v : Int | v > 0}, the positive integers. Type checking generates verification conditions, implications between predicates, and discharges them with an SMT solver, so a program can be checked against preconditions, postconditions and invariants without the programmer writing proof terms. The predicates are restricted to a decidable logic, typically linear arithmetic with uninterpreted functions, which is what keeps checking automatic. LiquidHaskell, F* and Liquid Types are the best-known systems.
• Value restrictionThe value restriction is the rule, in ML-family languages, that a let-bound expression has its type variables generalized only if it is a syntactic value, such as a function, a constant or a constructor applied to values. An application such as List.map f or ref [] is not a value, so its type variables stay weak and are fixed by their first use. Without the restriction, a reference could be given a polymorphic type and used to store a value at one type and read it at another. OCaml relaxes the rule for type variables that occur only covariantly.

• GADTs in OCamlMaking illegal states unrepresentable: typed expression evaluators, refined pattern matching, existentials, and a typed printf from scratch.

1. [1]H. Xi, C. Chen, G. Chen, “Guarded recursive datatype constructors”, POPL (2003).
2. [2]S. Peyton Jones, D. Vytiniotis, S. Weirich, G. Washburn, “Simple unification-based type inference for GADTs”, ICFP (2006).
3. [3]J. Cheney, R. Hinze, “First-class phantom types”, Technical Report TR2003-1901, Cornell University (2003).
4. [4]J. Garrigue, J. Le Normand, “Adding GADTs to OCaml: the direct approach”, ML Workshop (2011).
5. [5]J. Garrigue, D. Rémy, “Ambivalent types for principal type inference with GADTs”, APLAS (2013).
6. [6]D. Vytiniotis, S. Peyton Jones, T. Schrijvers, M. Sulzmann, “OutsideIn(X): modular type inference with local assumptions”, Journal of Functional Programming 21 (2011).
7. [7]T. Sheard, E. Pasalic, “Meta-programming with built-in type equality”, Workshop on Logical Frameworks and Meta-Languages (2004).
8. [8]S. Weirich, “Type-safe cast: functional pearl”, Journal of Functional Programming 14 (2004).

last updated 29 September 2026