129: Type-Level Natural Numbers

Difficulty: ⭐⭐⭐ Level: Advanced Encode the length of a collection as part of its type so operations like `pop` on an empty list, or calling a function that requires exactly 3 elements with a 2-element list, are compile errors.

The Problem This Solves

A classic runtime bug: you call `.pop()` on a stack, but the stack is empty. Or you pass a 2-element list to a function that documents "requires at least 3 elements." Both are runtime panics — and the type `Vec<T>` gives you no help, because `Vec<T>` with 2 elements and `Vec<T>` with 3 elements are the same type. What if the length were part of the type? Then `Vec_<T, Two>` and `Vec_<T, Three>` would be different types. A function that takes `Vec_<T, Three>` simply cannot be called with a 2-element vector — the types don't match. And `pop()` could only exist on `Vec_<T, Succ<N>>` (a vector with at least one element), never on `Vec_<T, Zero>`. You can't pop an empty list because the method isn't defined for that type. This is the core idea behind length-indexed vectors (also called "vectors" in dependently typed languages). It's a building block for safe APIs that document their preconditions in types rather than doc comments.

The Intuition

Peano arithmetic defines natural numbers using two rules: zero is a number, and the successor of any number is also a number. In code: `Zero` and `Succ<N>`. So `Succ<Zero>` is one, `Succ<Succ<Zero>>` is two, and so on. These are just empty structs — they hold no data. Their purpose is to be counted by the type system. When you have a `Vec_<T, Succ<Succ<Zero>>>`, the compiler knows at compile time that this vector contains exactly 2 elements. When you call `.push()`, it returns `Vec_<T, Succ<Succ<Succ<Zero>>>>` — a 3-element vector. The magic is that each `push` changes the type. The old value is consumed and a new one with an incremented type is returned. The type is a proof of length.

How It Works in Rust

use std::marker::PhantomData;

// Peano encoding: numbers as nested types, not values
struct Zero;
struct Succ<N>(PhantomData<N>);  // PhantomData: we don't store N, just use it as a type param

trait Nat {
 const VALUE: usize;  // optional: convert to a runtime number
}
impl Nat for Zero { const VALUE: usize = 0; }
impl<N: Nat> Nat for Succ<N> { const VALUE: usize = N::VALUE + 1; }

// Convenient aliases
type One   = Succ<Zero>;
type Two   = Succ<One>;
type Three = Succ<Two>;

// Length-indexed vector — length N is in the type, not stored at runtime
struct Vec_<T, N: Nat> {
 data: Vec<T>,
 _len: PhantomData<N>,
}

// Create: only Zero-length vectors can be created empty
impl<T> Vec_<T, Zero> {
 fn new() -> Self { Vec_ { data: vec![], _len: PhantomData } }
}

// push: consumes Vec_<T, N> and returns Vec_<T, Succ<N>>
// The length in the type increments with every push
impl<T, N: Nat> Vec_<T, N> {
 fn push(mut self, val: T) -> Vec_<T, Succ<N>> {
     self.data.push(val);
     Vec_ { data: self.data, _len: PhantomData }
 }
 fn len(&self) -> usize { N::VALUE }
}

// pop: only exists for Succ<N> — can't pop an empty Vec_<T, Zero>!
impl<T, N: Nat> Vec_<T, Succ<N>> {
 fn pop(mut self) -> (T, Vec_<T, N>) {  // returns element AND shorter vector
     let val = self.data.pop().unwrap();
     (val, Vec_ { data: self.data, _len: PhantomData })
 }
 fn head(&self) -> &T { &self.data[0] }
}

// This function requires EXACTLY 3 elements — enforced by the type
fn needs_three<T>(v: &Vec_<T, Three>) -> usize { v.len() }

Usage:

let v = Vec_::<i32, Zero>::new()
 .push(10)   // returns Vec_<i32, One>
 .push(20)   // returns Vec_<i32, Two>
 .push(30);  // returns Vec_<i32, Three>

needs_three(&v);  // compiles ✓

let two_elem = Vec_::<i32, Zero>::new().push(1).push(2);
// needs_three(&two_elem);  // compile error: expected Vec_<i32, Three>, found Vec_<i32, Two>

What This Unlocks

Safe stack APIs — a `Stack<T, N>` where `pop()` and `peek()` are absent on `Stack<T, Zero>` eliminates an entire class of underflow panics.
Typed matrices — combine with const generics or type-level nats to build matrices where row/column counts are tracked in types.
Protocol sequencing — model protocols where certain operations require a minimum number of prior steps to have been performed.

Key Differences

Concept	OCaml	Rust
Peano encoding	GADT: `type _ nat = Zero : zero nat \	Succ : 'n nat -> 'n succ nat`	Structs: `struct Zero; struct Succ<N>(PhantomData<N>)`
Length-indexed vec	Recursive GADT type `('a, 'n) vec` with native pattern matching	Struct with `PhantomData<N>`; different `impl` blocks per length constraint
Safe head/tail	GADT ensures `hd` only works on `succ` vectors	`head()` and `pop()` only in `impl Vec_<T, Succ<N>>` — absent for `Zero`
Runtime value	`let n = match v with Succ (Succ Zero) -> 2 ...`	`N::VALUE` — reads the const from the trait impl

// Example 129: Type-Level Natural Numbers — Peano Arithmetic
use std::marker::PhantomData;

// Approach 1: Peano numbers as types
struct Zero;
struct Succ<N>(PhantomData<N>);

trait Nat {
    const VALUE: usize;
}

impl Nat for Zero {
    const VALUE: usize = 0;
}

impl<N: Nat> Nat for Succ<N> {
    const VALUE: usize = N::VALUE + 1;
}

// Type aliases for convenience
type One = Succ<Zero>;
type Two = Succ<One>;
type Three = Succ<Two>;
type Four = Succ<Three>;

// Approach 2: Type-level addition
trait Add<B: Nat>: Nat {
    type Sum: Nat;
}

impl<B: Nat> Add<B> for Zero {
    type Sum = B;
}

impl<A: Nat + Add<B>, B: Nat> Add<B> for Succ<A> {
    type Sum = Succ<<A as Add<B>>::Sum>;
}

// Approach 3: Length-indexed vector
struct Vec_<T, N: Nat> {
    data: Vec<T>,
    _len: PhantomData<N>,
}

impl<T> Vec_<T, Zero> {
    fn new() -> Self {
        Vec_ { data: vec![], _len: PhantomData }
    }
}

impl<T, N: Nat> Vec_<T, N> {
    fn push(mut self, val: T) -> Vec_<T, Succ<N>> {
        self.data.push(val);
        Vec_ { data: self.data, _len: PhantomData }
    }

    fn len(&self) -> usize {
        N::VALUE
    }
}

impl<T, N: Nat> Vec_<T, Succ<N>> {
    fn pop(mut self) -> (T, Vec_<T, N>) {
        let val = self.data.pop().unwrap();
        (val, Vec_ { data: self.data, _len: PhantomData })
    }

    fn head(&self) -> &T {
        &self.data[0]
    }
}

// Require exactly N elements
fn needs_three<T>(v: &Vec_<T, Three>) -> usize {
    v.len()
}

fn main() {
    println!("Zero = {}", Zero::VALUE);
    println!("Three = {}", Three::VALUE);
    println!("2 + 3 = {}", <Two as Add<Three>>::Sum::VALUE);

    let v = Vec_::<i32, Zero>::new()
        .push(10)
        .push(20)
        .push(30);
    println!("Vec length: {}", v.len());
    println!("Needs three: {}", needs_three(&v));
    println!("Head: {}", v.head());
}

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

    #[test]
    fn test_nat_values() {
        assert_eq!(Zero::VALUE, 0);
        assert_eq!(One::VALUE, 1);
        assert_eq!(Two::VALUE, 2);
        assert_eq!(Three::VALUE, 3);
        assert_eq!(Four::VALUE, 4);
    }

    #[test]
    fn test_addition() {
        assert_eq!(<Zero as Add<Three>>::Sum::VALUE, 3);
        assert_eq!(<Two as Add<Three>>::Sum::VALUE, 5);
        assert_eq!(<One as Add<One>>::Sum::VALUE, 2);
    }

    #[test]
    fn test_vec_length() {
        let v = Vec_::<&str, Zero>::new()
            .push("a")
            .push("b");
        assert_eq!(v.len(), 2);
    }

    #[test]
    fn test_vec_push_pop() {
        let v = Vec_::<i32, Zero>::new().push(1).push(2).push(3);
        assert_eq!(v.len(), 3);
        let (val, v) = v.pop();
        assert_eq!(val, 3);
        assert_eq!(v.len(), 2);
    }

    #[test]
    fn test_vec_head() {
        let v = Vec_::<i32, Zero>::new().push(42).push(99);
        assert_eq!(*v.head(), 42);
    }
}

(* Example 129: Type-Level Natural Numbers — Peano Arithmetic *)

(* Approach 1: GADT-based Peano numbers *)
type zero = Zero_t
type 'n succ = Succ_t

(* Type-level nat witness *)
type _ nat =
  | Zero : zero nat
  | Succ : 'n nat -> 'n succ nat

let zero = Zero
let one = Succ Zero
let two = Succ (Succ Zero)
let three = Succ (Succ (Succ Zero))

let rec to_int : type n. n nat -> int = function
  | Zero -> 0
  | Succ n -> 1 + to_int n

(* Approach 2: Module-level Peano *)
module type NAT = sig
  type t
  val value : int
end

module Zero_m : NAT = struct type t = zero let value = 0 end

module Succ_m (N : NAT) : NAT = struct
  type t = N.t succ
  let value = N.value + 1
end

module One = Succ_m(Zero_m)
module Two = Succ_m(One)
module Three = Succ_m(Two)

(* Approach 3: Type-safe vectors with length *)
type ('a, 'n) vec =
  | VNil : ('a, zero) vec
  | VCons : 'a * ('a, 'n) vec -> ('a, 'n succ) vec

let v_empty : ('a, zero) vec = VNil
let v_single x : ('a, zero succ) vec = VCons (x, VNil)

let v_head : type a n. (a, n succ) vec -> a = function
  | VCons (x, _) -> x

let v_tail : type a n. (a, n succ) vec -> (a, n) vec = function
  | VCons (_, rest) -> rest

let rec v_length : type a n. (a, n) vec -> int = function
  | VNil -> 0
  | VCons (_, rest) -> 1 + v_length rest

(* Tests *)
let () =
  assert (to_int zero = 0);
  assert (to_int three = 3);
  assert (Zero_m.value = 0);
  assert (Three.value = 3);
  let v = VCons (1, VCons (2, VCons (3, VNil))) in
  assert (v_head v = 1);
  assert (v_length v = 3);
  assert (v_head (v_tail v) = 2);
  Printf.printf "✓ All tests passed\n"

📊 Detailed Comparison

Comparison: Type-Level Natural Numbers

Peano Encoding

OCaml

🐪 Show OCaml equivalent

type zero = Zero_t
type 'n succ = Succ_t

type _ nat =
| Zero : zero nat
| Succ : 'n nat -> 'n succ nat

let three = Succ (Succ (Succ Zero))

Rust

struct Zero;
struct Succ<N>(PhantomData<N>);

trait Nat { const VALUE: usize; }
impl Nat for Zero { const VALUE: usize = 0; }
impl<N: Nat> Nat for Succ<N> { const VALUE: usize = N::VALUE + 1; }

type Three = Succ<Succ<Succ<Zero>>>;

Length-Indexed Vector

OCaml

🐪 Show OCaml equivalent

type ('a, 'n) vec =
| VNil : ('a, zero) vec
| VCons : 'a * ('a, 'n) vec -> ('a, 'n succ) vec

let v_head : type a n. (a, n succ) vec -> a = function
| VCons (x, _) -> x

Rust

impl<T, N: Nat> Vec_<T, N> {
 fn push(self, val: T) -> Vec_<T, Succ<N>> { /* ... */ }
}

impl<T, N: Nat> Vec_<T, Succ<N>> {
 fn head(&self) -> &T { &self.data[0] }
}

129: Type-Level Natural Numbers

The Problem This Solves

The Intuition

How It Works in Rust

What This Unlocks

Key Differences

📊 Detailed Comparison

Comparison: Type-Level Natural Numbers

Peano Encoding

OCaml

Rust

Length-Indexed Vector

OCaml

Rust

Related Examples