Learn

GADTs (Generalized Algebraic Data Types) let constructor types vary — a constructor can return a more specific type than the family. Phantom types parameterize types without storing values. OCaml's manual treats them as the apex of the type system.

Phantom types

A type parameter that doesn't appear in any constructor — pure type-level marker:

type 'state email = string

type validated
type unvalidated

let validate (e : unvalidated email) : validated email option =
    if String.contains e '@' then Some (e : validated email)
    else None

let send (e : validated email) =
    Printf.printf "sending to %s\n" e

let () =
    match validate "[email protected]" with
    | Some valid -> send valid
    | None -> print_endline "invalid"

The state parameter is a phantom — never stored, only enforced at type level. send requires a validated email — you can't pass an unvalidated one without going through validate. Compile-time enforcement of "must be validated."

Classic pattern for state machines and validation pipelines.

GADTs

With the gadt syntax (-rectypes or per-constructor type signatures), constructors can constrain 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

Now:

• Int 5 has type int expr
• Bool true has type bool expr
• Add (Int 3, Bool true) is a TYPE ERROR

The interpreter is type-safe by construction:

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

Return type depends on which constructor — compiler tracks the relationship.

type a. — explicit polymorphism

GADT pattern matches need explicit polymorphic annotations:

let rec eval : type a. a expr -> a = function ...

The type a. introduces a fresh type variable that the compiler can refine in each case. Without it, OCaml can't infer the return type per branch.

Singleton types

GADTs can carry type-level values:

type zero = Zero
type 'n succ = Succ of 'n

type (_, _) eq = Refl : ('a, 'a) eq

(* Length-indexed lists: *)
type (_, _) vec =
    | Nil : ('a, zero) vec
    | Cons : 'a * ('a, 'n) vec -> ('a, 'n succ) vec

Length-indexed vectors — the type tracks the length. head on an empty vec is a type error.

This is approaching dependent types — powerful but heavy.

Practical patterns

Type-safe state machines:

type open_t
type closed_t

type 'state file = { name : string }

let open_file path : open_t file = { name = path }
let close (f : open_t file) : closed_t file = { name = f.name }
let read (f : open_t file) = (* ... *) ()

(* read on a closed_t file is a TYPE ERROR *)

The state lives in the type. Operations require the right state.

Type-safe DSL ASTs (the eval example above) — your DSL's type system runs at OCaml compile time.

When to use GADTs / phantom types

Yes:

• Domain-specific languages with strict type rules
• State machines where wrong-state operations should be compile errors
• Validation pipelines with state tracking
• Foundations for type-driven libraries

No:

• Everyday code — regular variants work fine
• When the complexity outweighs the safety
• Quick prototypes

GADTs and phantom types are advanced. Reach for them when type-level guarantees genuinely matter — for libraries, DSLs, safety-critical code.

Common mistakes

• Forgetting type a. in GADT pattern matches — compile error or type unification failure.
• Phantom type without enforcement — if every function ignores the phantom, the safety is illusory.
• GADT explosion — each constructor with a different type adds complexity. Keep it focused.
• Mixing GADTs with polymorphism naively — the constraint relationships matter; spend time on the types.
• Reaching for GADTs to express things regular variants do — overkill. Use the simpler tool.