176 Expert

Introduction to GADTs

Functional Programming

Tutorial

The Problem

Generalized Algebraic Data Types (GADTs) extend ordinary algebraic data types by allowing each constructor to specify a different return type for the type parameter. This enables type-safe expression trees where eval on int expr always returns int, not int | bool. GADTs were introduced in OCaml to bring the expressiveness of dependent types to mainstream functional programming. Rust simulates them via phantom types and sealed trait hierarchies.

🎯 Learning Outcomes

• Understand what GADTs are and why they extend ordinary ADTs

• Learn Rust's GADT simulation: phantom type parameters + sealed marker types

• See how the ExprType sealed trait restricts valid type indices

• Understand why Rust's simulation requires unreachable!() branches that OCaml's GADTs eliminate

Code Example

use std::marker::PhantomData;

enum ExprInner {
    Int(i64),
    Bool(bool),
    Add(Box<ExprInner>, Box<ExprInner>),
    If(Box<ExprInner>, Box<ExprInner>, Box<ExprInner>),
}

struct Expr<T> {
    inner: ExprInner,
    _phantom: PhantomData<T>,
}

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

Key Differences

Exhaustiveness: OCaml's GADT pattern matching is exhaustive per index — impossible cases are excluded; Rust's phantom type simulation requires unreachable!() for dead branches.

Constructor syntax: OCaml's : type expr syntax is built into the language; Rust requires phantom parameters and smart constructors.

Type variable scope: OCaml's type a. a expr -> a scopes the type variable per clause; Rust uses trait bounds and associated types.

Safety guarantee: Both prevent constructing ill-typed expressions at compile time; OCaml's guarantee is stronger (no runtime dead-code branches).

OCaml Approach

OCaml's GADTs express this directly:

type _ expr =
  | IntLit : int -> int expr
  | BoolLit : bool -> bool expr
  | Add : int expr * int expr -> int expr
  | Equal : int expr * int expr -> bool expr
let rec eval : type a. a expr -> a = function
  | IntLit n -> n
  | BoolLit b -> b
  | Add (l, r) -> eval l + eval r
  | Equal (l, r) -> eval l = eval r

The compiler knows that eval on int expr cannot match BoolLit — no unreachable!() needed.

Full Source

#![allow(clippy::all)]
// Example 176: Introduction to GADTs
// Rust doesn't have native GADTs, but we can simulate them with
// PhantomData, traits, and sealed type-level markers.

use std::marker::PhantomData;

// === Approach 1: PhantomData + sealed traits to simulate GADTs ===

mod sealed {
    pub trait ExprType {}
    impl ExprType for i64 {}
    impl ExprType for bool {}
}

#[derive(Debug)]
enum ExprInner {
    Int(i64),
    Bool(bool),
    Add(Box<ExprInner>, Box<ExprInner>),
    If(Box<ExprInner>, Box<ExprInner>, Box<ExprInner>),
}

#[derive(Debug)]
struct Expr<T: sealed::ExprType> {
    inner: ExprInner,
    _phantom: PhantomData<T>,
}

impl Expr<i64> {
    fn int(n: i64) -> Self {
        Expr {
            inner: ExprInner::Int(n),
            _phantom: PhantomData,
        }
    }
    fn add(a: Expr<i64>, b: Expr<i64>) -> Self {
        Expr {
            inner: ExprInner::Add(Box::new(a.inner), Box::new(b.inner)),
            _phantom: PhantomData,
        }
    }
    fn eval(&self) -> i64 {
        match &self.inner {
            ExprInner::Int(n) => *n,
            ExprInner::Add(a, b) => {
                let a = Expr::<i64> {
                    inner: *a.clone(),
                    _phantom: PhantomData,
                };
                let b = Expr::<i64> {
                    inner: *b.clone(),
                    _phantom: PhantomData,
                };
                a.eval() + b.eval()
            }
            ExprInner::If(c, t, f) => {
                let c = Expr::<bool> {
                    inner: *c.clone(),
                    _phantom: PhantomData,
                };
                let t = Expr::<i64> {
                    inner: *t.clone(),
                    _phantom: PhantomData,
                };
                let f = Expr::<i64> {
                    inner: *f.clone(),
                    _phantom: PhantomData,
                };
                if c.eval() {
                    t.eval()
                } else {
                    f.eval()
                }
            }
            _ => unreachable!(),
        }
    }
}

impl Expr<bool> {
    fn bool_val(b: bool) -> Self {
        Expr {
            inner: ExprInner::Bool(b),
            _phantom: PhantomData,
        }
    }
    fn eval(&self) -> bool {
        match &self.inner {
            ExprInner::Bool(b) => *b,
            _ => unreachable!(),
        }
    }
}

impl Clone for ExprInner {
    fn clone(&self) -> Self {
        match self {
            ExprInner::Int(n) => ExprInner::Int(*n),
            ExprInner::Bool(b) => ExprInner::Bool(*b),
            ExprInner::Add(a, b) => {
                ExprInner::Add(Box::new((**a).clone()), Box::new((**b).clone()))
            }
            ExprInner::If(a, b, c) => ExprInner::If(
                Box::new((**a).clone()),
                Box::new((**b).clone()),
                Box::new((**c).clone()),
            ),
        }
    }
}

fn if_expr(cond: Expr<bool>, then: Expr<i64>, else_: Expr<i64>) -> Expr<i64> {
    Expr {
        inner: ExprInner::If(
            Box::new(cond.inner),
            Box::new(then.inner),
            Box::new(else_.inner),
        ),
        _phantom: PhantomData,
    }
}

// === Approach 2: Enum-based with trait for evaluation ===

trait Eval {
    type Output;
    fn eval(&self) -> Self::Output;
}

struct IntLit(i64);
struct BoolLit(bool);
struct AddExpr(Box<dyn Eval<Output = i64>>, Box<dyn Eval<Output = i64>>);

impl Eval for IntLit {
    type Output = i64;
    fn eval(&self) -> i64 {
        self.0
    }
}

impl Eval for BoolLit {
    type Output = bool;
    fn eval(&self) -> bool {
        self.0
    }
}

impl Eval for AddExpr {
    type Output = i64;
    fn eval(&self) -> i64 {
        self.0.eval() + self.1.eval()
    }
}

// === Approach 3: Type-safe heterogeneous list with tuples ===

// Rust's type system naturally supports this via nested tuples
// (42, ("hello", (true, ())))  is the HList equivalent

trait HList {}
impl HList for () {}
impl<H, T: HList> HList for (H, T) {}

trait Head {
    type Item;
    fn head(&self) -> &Self::Item;
}

impl<H, T: HList> Head for (H, T) {
    type Item = H;
    fn head(&self) -> &H {
        &self.0
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_phantom_gadt_int() {
        assert_eq!(Expr::int(42).eval(), 42);
    }

    #[test]
    fn test_phantom_gadt_add() {
        assert_eq!(Expr::add(Expr::int(1), Expr::int(2)).eval(), 3);
    }

    #[test]
    fn test_phantom_gadt_bool() {
        assert_eq!(Expr::bool_val(true).eval(), true);
    }

    #[test]
    fn test_phantom_gadt_if() {
        let e = if_expr(Expr::bool_val(true), Expr::int(10), Expr::int(20));
        assert_eq!(e.eval(), 10);
        let e2 = if_expr(Expr::bool_val(false), Expr::int(10), Expr::int(20));
        assert_eq!(e2.eval(), 20);
    }

    #[test]
    fn test_trait_eval() {
        assert_eq!(IntLit(5).eval(), 5);
        assert_eq!(BoolLit(false).eval(), false);
        assert_eq!(AddExpr(Box::new(IntLit(3)), Box::new(IntLit(4))).eval(), 7);
    }

    #[test]
    fn test_hlist() {
        let hlist = (42, ("hello", (true, ())));
        assert_eq!(*hlist.head(), 42);
        assert_eq!(*hlist.1.head(), "hello");
        assert_eq!(*hlist.1 .1.head(), true);
    }
}

(* Example 176: Introduction to GADTs *)
(* GADTs (Generalized Algebraic Data Types) allow constructors to return
   different type instantiations of the same type *)

(* Approach 1: Basic GADT with type-safe expressions *)
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

let rec eval : type a. a expr -> a = function
  | Int n -> n
  | Bool b -> b
  | Add (a, b) -> eval a + eval b
  | If (cond, t, f) -> if eval cond then eval t else eval f

(* Approach 2: GADT for type-safe formatting *)
type _ fmt =
  | Lit  : string -> string fmt
  | FInt : int fmt
  | FStr : string fmt
  | Cat  : 'a fmt * 'b fmt -> ('a * 'b) fmt

let rec format_to_string : type a. a fmt -> a -> string = fun fmt v ->
  match fmt with
  | Lit s -> s
  | FInt -> string_of_int v
  | FStr -> v
  | Cat (a, b) ->
    let (va, vb) = v in
    format_to_string a va ^ format_to_string b vb

(* Approach 3: GADT for type-safe heterogeneous lists *)
type _ hlist =
  | HNil  : unit hlist
  | HCons : 'a * 'b hlist -> ('a * 'b) hlist

let example_list = HCons (42, HCons ("hello", HCons (true, HNil)))

let hd : type a b. (a * b) hlist -> a = function
  | HCons (x, _) -> x

(* Tests *)
let () =
  (* Test Approach 1 *)
  assert (eval (Int 42) = 42);
  assert (eval (Bool true) = true);
  assert (eval (Add (Int 1, Int 2)) = 3);
  assert (eval (If (Bool true, Int 10, Int 20)) = 10);
  assert (eval (If (Bool false, Int 10, Int 20)) = 20);

  (* Test Approach 2 *)
  assert (format_to_string (Lit "hello") "hello" = "hello");
  assert (format_to_string FInt 42 = "42");
  assert (format_to_string FStr "world" = "world");
  assert (format_to_string (Cat (Lit "n=", FInt)) ("n=", 42) = "n=42");

  (* Test Approach 3 *)
  assert (hd example_list = 42);

  print_endline "✓ All tests passed"

✓ Tests Rust test suite

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_phantom_gadt_int() {
        assert_eq!(Expr::int(42).eval(), 42);
    }

    #[test]
    fn test_phantom_gadt_add() {
        assert_eq!(Expr::add(Expr::int(1), Expr::int(2)).eval(), 3);
    }

    #[test]
    fn test_phantom_gadt_bool() {
        assert_eq!(Expr::bool_val(true).eval(), true);
    }

    #[test]
    fn test_phantom_gadt_if() {
        let e = if_expr(Expr::bool_val(true), Expr::int(10), Expr::int(20));
        assert_eq!(e.eval(), 10);
        let e2 = if_expr(Expr::bool_val(false), Expr::int(10), Expr::int(20));
        assert_eq!(e2.eval(), 20);
    }

    #[test]
    fn test_trait_eval() {
        assert_eq!(IntLit(5).eval(), 5);
        assert_eq!(BoolLit(false).eval(), false);
        assert_eq!(AddExpr(Box::new(IntLit(3)), Box::new(IntLit(4))).eval(), 7);
    }

    #[test]
    fn test_hlist() {
        let hlist = (42, ("hello", (true, ())));
        assert_eq!(*hlist.head(), 42);
        assert_eq!(*hlist.1.head(), "hello");
        assert_eq!(*hlist.1 .1.head(), true);
    }
}

Deep Comparison

Comparison: Example 176 — Introduction to GADTs

GADT Type Definition

OCaml

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

Rust

use std::marker::PhantomData;

enum ExprInner {
    Int(i64),
    Bool(bool),
    Add(Box<ExprInner>, Box<ExprInner>),
    If(Box<ExprInner>, Box<ExprInner>, Box<ExprInner>),
}

struct Expr<T> {
    inner: ExprInner,
    _phantom: PhantomData<T>,
}

Type-Safe Evaluation

OCaml

let rec eval : type a. a expr -> a = function
  | Int n -> n
  | Bool b -> b
  | Add (a, b) -> eval a + eval b
  | If (cond, t, f) -> if eval cond then eval t else eval f

Rust

impl Expr<i64> {
    fn eval(&self) -> i64 {
        match &self.inner {
            ExprInner::Int(n) => *n,
            ExprInner::Add(a, b) => { /* reconstruct typed wrappers */ }
            _ => unreachable!(),
        }
    }
}

impl Expr<bool> {
    fn eval(&self) -> bool {
        match &self.inner {
            ExprInner::Bool(b) => *b,
            _ => unreachable!(),
        }
    }
}

Trait-Based Alternative (Rust)

Rust

trait Eval {
    type Output;
    fn eval(&self) -> Self::Output;
}

struct IntLit(i64);
impl Eval for IntLit {
    type Output = i64;
    fn eval(&self) -> i64 { self.0 }
}

struct AddExpr(Box<dyn Eval<Output = i64>>, Box<dyn Eval<Output = i64>>);
impl Eval for AddExpr {
    type Output = i64;
    fn eval(&self) -> i64 { self.0.eval() + self.1.eval() }
}

Heterogeneous Lists

OCaml

type _ hlist =
  | HNil  : unit hlist
  | HCons : 'a * 'b hlist -> ('a * 'b) hlist

let hd : type a b. (a * b) hlist -> a = function
  | HCons (x, _) -> x

Rust

trait HList {}
impl HList for () {}
impl<H, T: HList> HList for (H, T) {}

trait Head {
    type Item;
    fn head(&self) -> &Self::Item;
}

impl<H, T: HList> Head for (H, T) {
    type Item = H;
    fn head(&self) -> &H { &self.0 }
}

// Usage: (42, ("hello", (true, ())))

Exercises

Add a Neg : int expr -> int expr constructor and implement its evaluation.

Add IfThenElse : bool expr -> 'a expr -> 'a expr -> 'a expr — how does the type constraint on the two branches affect the Rust simulation?

Verify at compile time that add(bool_lit(true), int_lit(1)) is rejected.

Open Source Repos

functional-rust

View the source for this example on GitHub — OCaml and Rust side by side in the repo.

Rust