Generalised algebraic data types (GADTs)

Writing an evaluator for a tiny language with integers, booleans and additions, in an ordinary variant, usually ends in a run-time guard: Add has to assert that both sub-terms are integers, and If has to assert that its condition is a boolean. A bad input finds the hole as Failure "int in Add", not as a type error. A GADTGADT (generalised algebraic data type): A variant whose constructors can each give a different return type on the right of a colon, which pattern matching then refines; the index tells OCaml which arms are reachable for which value. gives each constructor its own return type, so the compiler already knows that Add makes an int expr and Bool true is a bool expr, and the two cannot be mixed.

Every output on this page was printed by OCaml 5.5.1. The four sessions build a small typed language, a list of mixed values that carry their own printers, a heterogeneous list in the style the new 5.5 Printf.lprintf reads, and a type-safe key-value store.

A constructor’s return type refines the index

In a plain variant, every constructor builds the same type: type t = A of int | B of string makes A and B both values of t. In a GADT, each constructor declares its own return type, so the type indexA type parameter whose value, inside a GADT, picks which cases of a match are reachable. after the arrow is different per case:

"""A typed expression language built with a GADT: typed-expr.ml runs, and two broken siblings fail at compile time."""

from session import files, run, toplevel, write

files("typed-expr.ml")

run("""
ocaml typed-expr.ml
""")

toplevel("""
#use "typed-expr.ml";;
eval (Add (Int 2, Int 3));;
eval (Eq (Int 1, Int 1));;
eval (If (Bool false, Int 10, Int 20));;
""")

# A match without the locally abstract type annotation, and an ill-typed term: both are refused.
write("no_annot.ml", """type _ expr =
  | Int : int -> int expr
  | Bool : bool -> bool expr
  | Add : int expr * int expr -> int expr

let rec eval = function
  | Int n -> n
  | Bool b -> b
  | Add (a, b) -> eval a + eval b
""")
write("ill_typed.ml", """type _ expr = Int : int -> int expr | Bool : bool -> bool expr | Add : int expr * int expr -> int expr
let _ = Add (Int 1, Bool true)
""")
run("""
!ocamlc -c no_annot.ml
!ocamlc -c ill_typed.ml
""")

$ ocaml typed-expr.ml
If (Eq (Int 1, Add (Int 0, Int 1)), Int 10, Int 20) => 10
$ ocaml
OCaml version 5.5.1
Enter #help;; for help.

# #use "typed-expr.ml";;
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
val eval : 'a expr -> 'a = <fun>
If (Eq (Int 1, Add (Int 0, Int 1)), Int 10, Int 20) => 10
# eval (Add (Int 2, Int 3));;
- : int = 5
# eval (Eq (Int 1, Int 1));;
- : bool = true
# eval (If (Bool false, Int 10, Int 20));;
- : int = 20
$ ocamlc -c no_annot.ml
File "no_annot.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
[exit status 2]
$ ocamlc -c ill_typed.ml
File "ill_typed.ml", line 2, characters 20-29:
2 | let _ = Add (Int 1, Bool true)
                        ^^^^^^^^^
Error: This constructor has type bool expr
       but an expression was expected of type int expr
       Type bool is not compatible with type int
[exit status 2]

Int : int -> int expr says the constructor takes an int and gives an int expr, while Bool : bool -> bool expr gives a bool expr. Add says both sub-terms must be int expr and the result is one too. If is parametric on the branches: bool expr * 'a expr * 'a expr -> 'a expr, so an If is an int expr when its branches are, and a bool expr when they are, but the condition is always a bool expr. The compiler used the indices to reject Add (Int 1, Bool true) with “This constructor has type bool expr but an expression was expected of type int expr”. No run-time check ever runs for that term, because no run time happens: the file does not compile. Step through what each sub-term’s type is:

Pattern matching needs a locally abstract type

Matching a GADT asks the type-checker to refine the match’s own type at each arm. OCaml refuses to guess that refinement, so a plain let rec eval = function | Int n -> n | Bool b -> b | ... fails to compile with “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”. The compiler saw the first arm Int n -> n as pinning the input to int expr, and then rejected the Bool b -> b arm. The first session recorded this message when the file no_annot.ml was built.

The fix is a locally abstract typelocally abstract type: A type a function introduces with 'type a.', kept abstract inside the body and refined per arm, which lets pattern matching on a GADT type-check each arm against its own case's type. written on the function: let rec eval : type a. a expr -> a = function .... The a is a fresh type inside the function body, kept abstract so each arm can pin it: in | Int n -> n the compiler reads a = int, and in | Bool b -> b it reads a = bool. Each arm is type-checked against its own a, and the function has the general type 'a expr -> 'a outside. OCaml 5.5.1 printed that signature when the full typed-expr.ml was loaded with #use, and eval (If (Bool false, Int 10, Int 20)) returned the integer 20. The same shape works for a typed size, a printer or a serialiser over the GADT: the function is the only place that needs the annotation.

An existential type packs a value with its printer

A GADT can also hide a type inside a constructor. The constructor introduces a type variable that no caller can name, called an existential typeexistential type: A type variable a constructor introduces for its own fields that no caller can name, so values of different inner types share one visible type.; the value and anything that operates on it travel together. The classic shape is one visible type that holds mixed inner types:

"""One list of mixed values that each know how to print themselves: the existential type showable keeps the printer with the value."""

from session import files, run, toplevel, write

files("existential.ml")

run("""
ocaml existential.ml
""")

# At the toplevel: what the type looks like, and what cannot be done with an unpacked value.
toplevel("""
#use "existential.ml";;
List.length items;;
""")

# Trying to look at the inner value: the existential type variable 'a leaks out of its scope.
write("escape.ml", """type showable = Show : 'a * ('a -> string) -> showable
let get_value (Show (v, _)) = v
""")
run("""
!ocamlc -c escape.ml
""")

$ ocaml existential.ml
42
"Thiruvananthapuram"
3.140
[1; 2; 3]
$ ocaml
OCaml version 5.5.1
Enter #help;; for help.

# #use "existential.ml";;
type showable = Show : 'a * ('a -> string) -> showable
val items : showable list =
  [Show (<poly>, <fun>); Show (<poly>, <fun>); Show (<poly>, <fun>);
   Show (<poly>, <fun>)]
42
"Thiruvananthapuram"
3.140
[1; 2; 3]
# List.length items;;
- : int = 4
$ ocamlc -c escape.ml
File "escape.ml", line 2, characters 30-31:
2 | let get_value (Show (v, _)) = v
                                  ^
Error: The value v has type $a but an expression was expected of type 'a
       The type constructor $a would escape its scope
       Hint: $a is an existential type bound by the constructor Show.
[exit status 2]

type showable = Show : 'a * ('a -> string) -> showable reads as “a Show carries a value and a function that prints that value, agreeing on their type, and gives back a showable”. The 'a is bound by the constructor, so outside the box there is no 'a to name. The first list in the session held an int with string_of_int, a string with a quoting printer, a float with %.3f and an int list with a joiner, and List.iter ran the right printer on each entry. The toplevel showed each inner value as <poly> because its own printer does not know what to do with a hidden type.

Trying to take the value back out, let get_value (Show (v, _)) = v, was refused with “The type constructor $a would escape its scope. Hint: $a is an existential type bound by the constructor Show.” The only safe move is to use the companion function inside the box: here pp v, which returns a string for every element whatever its hidden type was. That is often enough: a logger, a diff viewer, a form renderer or a (string * Yojson.t) list builder each wants a type back out, not the value itself.

Where GADTs earn their keep, and where they do not

GADTs power two features of the 5.5 standard library that this track meets elsewhere, and they let you build a type-safe store where each key names its value’s type. Printf.lprintf reads its arguments as a heterogeneous list driven by its format string, so the type of the list is pinned by the format: the third session’s Printf.lprintf "%s %d %.02f %c\n" [ "ocaml"; 42; 3.14; 'c' ] printed ocaml 42 3.14 c, and a list whose types do not match the format would be a compile-time error. Effect declarations extend an open GADT: type _ Effect.t += Ask : string -> int Effect.t adds Ask with the result type int. A type-safe key-value store, like the one the fourth session builds, lets get Age return an int option and get Emails a string list option, one get for every type.

"""A heterogeneous list and the 5.5 Printf.Args list: a GADT lets one type describe lists whose cells have different types."""

from session import files, run, toplevel, write

files("hlist.ml")

run("""
ocaml hlist.ml
""")

toplevel("""
#use "hlist.ml";;
HCons (42, HNil);;
let h2 = HCons ("hi", HCons (true, HNil));;
length h2;;
""")

# A mismatched use rejected: a list whose type says (int * unit) hlist cannot be used where unit hlist is expected.
write("mismatch.ml", """type _ hlist = HNil : unit hlist | HCons : 'a * 'b hlist -> ('a * 'b) hlist
let h = HCons (42, HNil)
let bad : unit hlist = h
""")
run("""
!ocamlc -c mismatch.ml
""")

$ ocaml hlist.ml
length = 3
Printf.lprintf gives: ocaml 42 3.14 c
$ ocaml
OCaml version 5.5.1
Enter #help;; for help.

# #use "hlist.ml";;
type _ hlist = HNil : unit hlist | HCons : 'a * 'b hlist -> ('a * 'b) hlist
val length : 'a hlist -> int = <fun>
val h : (int * (string * (float * unit))) hlist =
  HCons (42, HCons ("ocaml", HCons (3.14, HNil)))
length = 3
Printf.lprintf gives: ocaml 42 3.14 c
# HCons (42, HNil);;
- : (int * unit) hlist = HCons (42, HNil)
# let h2 = HCons ("hi", HCons (true, HNil));;
val h2 : (string * (bool * unit)) hlist = HCons ("hi", HCons (true, HNil))
# length h2;;
- : int = 2
$ ocamlc -c mismatch.ml
File "mismatch.ml", line 3, characters 23-24:
3 | let bad : unit hlist = h
                           ^
Error: The value h has type (int * unit) hlist
       but an expression was expected of type unit hlist
       Type int * unit is not compatible with type unit
[exit status 2]

"""A GADT key-value store: each key names the type of its value, and the compiler types every get by the key passed."""

from session import files, run, toplevel

files("kv_store.ml")

run("""
ocaml kv_store.ml
""")

toplevel("""
#use "kv_store.ml";;
get Name store;;
get Age store;;
get Emails store;;
let n = (match get Age store with Some n -> n | None -> 0) + 1;;
""")

$ ocaml kv_store.ml
name: Asha
age: 32
emails: asha@example.in, a2@example.in
$ ocaml
OCaml version 5.5.1
Enter #help;; for help.

# #use "kv_store.ml";;
type _ key = Name : string key | Age : int key | Emails : string list key
type entry = Entry : 'a key * 'a -> entry
type (_, _) eq = Eq : ('a, 'a) eq
val key_eq : 'a key -> 'b key -> ('a, 'b) eq option = <fun>
val get : 'a key -> entry list -> 'a option = <fun>
val store : entry list =
  [Entry (Name, <poly>); Entry (Age, <poly>); Entry (Emails, <poly>)]
name: Asha
age: 32
emails: asha@example.in, a2@example.in
# get Name store;;
- : string option = Some "Asha"
# get Age store;;
- : int option = Some 32
# get Emails store;;
- : string list option = Some ["asha@example.in"; "a2@example.in"]
# let n = (match get Age store with Some n -> n | None -> 0) + 1;;
val n : int = 33

The hlist’s three elements lived under the type (int * (string * (float * unit))) hlist, and the mismatched use let bad : unit hlist = HCons (42, HNil) was refused with “Type int * unit is not compatible with type unit”. The lesson’s kv_store.ml kept three entries, one per key, and the toplevel typed get Age store as int option and get Emails store as string list option; the helper key_eq handles each key’s type by pattern matching. The hlist was loaded with #use on OCaml 5.5.1 and compiled under ocamlc -c to probe the mismatch.

GADTs come with a cost. A type a. annotation is extra text, the error messages involve existential names such as $a, and small changes in the type index can push a function over the point where the compiler stops guessing. For a status variant such as Ok | Warn | Fail, or a tree whose nodes all carry the same payload, a plain variant stays simpler and faster to read. Reach for a GADT when the compiler could rule out a case for you, when payloads differ by type, or when the standard library already asks for one.

Practise: types that each constructor pins

The questions come from the three sessions: the typed evaluator and its two refusals, the showable existential, and the heterogeneous list with Printf.lprintf.

Interview questions

Warm-up (fresher to 2–5 years): what is a GADT, and how does it differ from a plain variant?

A GADT, or generalised algebraic data type, is a variant whose constructors can each have a different return type, written on the right of a colon: Int : int -> int expr and Bool : bool -> bool expr build values of two different index types that share the name expr. A plain variant forces every constructor into one type, so a match’s cases all return the same thing and the compiler cannot rule out a case by its payload. In the GADT, pattern matching on an int expr only type-checks arms that return an int expr, which lets eval be total without a run-time guard, and Add (Int 1, Bool true) is a compile-time error rather than a Failure from assert.

Two harder questions follow, about a typed evaluator whose match the compiler refuses, and about choosing between a GADT and a plain variant for an expression language that is growing. For each, say what the first error message reads like and what you would change to make it compile, then open its first step:

Key takeaways

• A GADT puts a type on each constructor’s return: Add : int expr * int expr -> int expr makes Add (Int 1, Bool true) a compile-time error, not a run-time failure.
• A function that matches a GADT needs a locally abstract type, let f : type a. a expr -> a = function ..., so each arm can refine a to the type its constructor built.
• An existential constructor hides a type variable inside the box: type showable = Show : 'a * ('a -> string) -> showable holds a value and its printer, and the only safe move is to call that printer.
• The 5.5 standard library uses GADTs in a few places: Printf.lprintf reads a heterogeneous list driven by its format string, and type _ Effect.t += Ask : string -> int Effect.t extends an open GADT.