129 Advanced

Type-Level Natural Numbers — Peano Arithmetic

Functional Programming

Tutorial

The Problem

Type-level naturals extend the type system to encode numbers as types: Zero, Succ<Zero> (= 1), Succ<Succ<Zero>> (= 2). This enables length-indexed containers where the compiler rejects out-of-bounds access, type-safe matrix operations where dimension mismatches are compile errors, and statically checked protocol sequences. The technique originates from dependent type theory (Agda, Coq, Idris) and is approximated in Rust and OCaml using type-level programming.

🎯 Learning Outcomes

• Understand Peano arithmetic and how it encodes numbers as nested types

• Learn how PhantomData<N> carries type-level information with zero runtime cost

• See how type-level addition and comparison enable compile-time arithmetic

• Understand the limitation compared to true dependent types (Rust/OCaml vs. Idris/Agda)

Code Example

use std::marker::PhantomData;

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

pub 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; }

pub type One   = Succ<Zero>;
pub type Two   = Succ<One>;
pub type Three = Succ<Two>;

type zero = Zero_t
type 'n succ = Succ_t

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

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

(* Length-indexed list — 'n encodes the length *)
type (_, _) vec =
  | Nil  : ('a, zero nat) vec
  | Cons : 'a * ('a, 'n nat) vec -> ('a, 'n succ nat) vec

Key Differences

GADTs vs. traits: OCaml's GADT encoding is direct and ergonomic; Rust's requires a chain of Add trait impls with associated types.

Const generics alternative: Rust's const N: usize (example 126) is a simpler alternative for most practical uses; type-level Peano naturals are needed only when arithmetic over type parameters is required.

Compile-time errors: Both produce compile errors for invalid operations, but OCaml's GADT error messages are often more informative than Rust's trait-bound errors.

Runtime reflection: Rust's Nat::VALUE reflects to usize; OCaml's GADT length is similarly reflected through a length function returning an integer.

OCaml Approach

OCaml with GADTs can encode similar length-indexed types:

type zero = Zero
type 'n succ = Succ
type ('a, 'n) vec =
  | Nil  : ('a, zero) vec
  | Cons : 'a * ('a, 'n) vec -> ('a, 'n succ) vec

This is more ergonomic than the Rust encoding because GADTs provide direct type refinement in pattern matches, while Rust must use trait bounds and associated types.

Full Source

#![allow(clippy::all)]
//! Example 129: Type-Level Natural Numbers — Peano Arithmetic
//!
//! Encode natural numbers as *types* using Peano arithmetic so that the length
//! of a collection becomes part of its type.  Operations like `pop` on an empty
//! list, or calling a function that requires exactly 3 elements with a
//! 2-element list, become compile errors — no runtime checks needed.

use std::marker::PhantomData;

// ── Approach 1: Peano numbers as marker types ─────────────────────────────────

/// The zero natural number at the type level.
pub struct Zero;

/// The successor of `N` — represents N+1.
pub struct Succ<N>(PhantomData<N>);

/// Reflect a type-level natural number to a runtime `usize`.
pub 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;
}

/// Convenient type aliases.
pub type One = Succ<Zero>;
pub type Two = Succ<One>;
pub type Three = Succ<Two>;
pub type Four = Succ<Three>;
pub type Five = Succ<Four>;

// ── Approach 2: Type-level addition ──────────────────────────────────────────
//
// `Add<B>` computes `Self + B` at the type level.
// Base case:  Zero + B  = B
// Step case:  Succ<A> + B = Succ<A + B>

pub 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 ────────────────────────────────────────
//
// `TypeVec<T, N>` stores T values and carries the exact count N in its type.
// * `push` increments the length type: TypeVec<T,N> → TypeVec<T, Succ<N>>
// * `pop`  only exists for TypeVec<T, Succ<N>>, so popping an empty vec is a
//   *compile* error — the method simply isn't defined on TypeVec<T, Zero>.
// * `first` only exists for non-empty vecs for the same reason.

pub struct TypeVec<T, N: Nat> {
    data: Vec<T>,
    _len: PhantomData<N>,
}

/// Create an empty length-indexed vector.
pub fn empty<T>() -> TypeVec<T, Zero> {
    TypeVec {
        data: Vec::new(),
        _len: PhantomData,
    }
}

// Methods available for *any* length (including zero).
impl<T, N: Nat> TypeVec<T, N> {
    /// Returns the runtime length (always equals N::VALUE).
    pub fn len(&self) -> usize {
        self.data.len()
    }

    /// True only for the empty vector.
    pub fn is_empty(&self) -> bool {
        self.data.is_empty()
    }

    /// Returns a slice of all elements.
    pub fn as_slice(&self) -> &[T] {
        &self.data
    }

    /// Push an element, returning a vector of length Succ<N>.
    pub fn push(mut self, value: T) -> TypeVec<T, Succ<N>> {
        self.data.push(value);
        TypeVec {
            data: self.data,
            _len: PhantomData,
        }
    }
}

// Methods that require at least one element — defined only for Succ<N>.
impl<T, N: Nat> TypeVec<T, Succ<N>> {
    /// Remove and return the last element, returning the shorter vector.
    pub fn pop(mut self) -> (TypeVec<T, N>, T) {
        // The type Succ<N> guarantees `data` is non-empty.
        let value = self.data.pop().expect("type guarantees non-empty");
        let shorter = TypeVec {
            data: self.data,
            _len: PhantomData,
        };
        (shorter, value)
    }

    /// Reference to the first element — safe because the vec is non-empty.
    pub fn first(&self) -> &T {
        self.data.first().expect("type guarantees non-empty")
    }

    /// Reference to the last element — safe because the vec is non-empty.
    pub fn last(&self) -> &T {
        self.data.last().expect("type guarantees non-empty")
    }
}

// ── Approach 4: Statically-sized function argument ────────────────────────────
//
// Functions can require a vec of *exactly* the right length.
// Passing a vec of the wrong size is a compile error.

/// Sum a length-3 vector of i32 values.
pub fn sum_three(v: &TypeVec<i32, Three>) -> i32 {
    v.as_slice().iter().sum()
}

/// Return the pair from a length-2 vector.
pub fn pair_to_tuple<T: Copy>(v: &TypeVec<T, Two>) -> (T, T) {
    (v.as_slice()[0], v.as_slice()[1])
}

// ── Tests ─────────────────────────────────────────────────────────────────────

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

    // ── Nat trait ────────────────────────────────────────────────────────────

    #[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);
        assert_eq!(Five::VALUE, 5);
    }

    #[test]
    fn test_nat_const_eval() {
        const N: usize = Three::VALUE;
        assert_eq!(N, 3);
    }

    // ── Type-level addition ───────────────────────────────────────────────────

    #[test]
    fn test_add_zero_identity() {
        assert_eq!(<Zero as Add<Three>>::Sum::VALUE, 3);
        assert_eq!(<Three as Add<Zero>>::Sum::VALUE, 3);
    }

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

    // ── TypeVec: empty ────────────────────────────────────────────────────────

    #[test]
    fn test_empty_vec() {
        let v: TypeVec<i32, Zero> = empty();
        assert_eq!(v.len(), 0);
        assert!(v.is_empty());
        assert_eq!(v.len(), Zero::VALUE);
    }

    // ── TypeVec: push increments the type ─────────────────────────────────────

    #[test]
    fn test_push_increments_type() {
        let v0: TypeVec<i32, Zero> = empty();
        let v1: TypeVec<i32, One> = v0.push(10);
        let v2: TypeVec<i32, Two> = v1.push(20);
        let v3: TypeVec<i32, Three> = v2.push(30);

        assert_eq!(v3.len(), 3);
        assert_eq!(v3.len(), Three::VALUE);
        assert_eq!(v3.as_slice(), &[10, 20, 30]);
    }

    // ── TypeVec: pop decrements the type ──────────────────────────────────────

    #[test]
    fn test_pop_decrements_type() {
        let v3: TypeVec<i32, Three> = empty().push(1).push(2).push(3);
        let (v2, last): (TypeVec<i32, Two>, i32) = v3.pop();
        assert_eq!(last, 3);
        assert_eq!(v2.len(), 2);

        let (v1, mid): (TypeVec<i32, One>, i32) = v2.pop();
        assert_eq!(mid, 2);
        assert_eq!(v1.len(), 1);

        let (v0, first): (TypeVec<i32, Zero>, i32) = v1.pop();
        assert_eq!(first, 1);
        assert_eq!(v0.len(), 0);
        // v0.pop() would not compile — pop is not defined for TypeVec<T, Zero>.
    }

    // ── TypeVec: first / last ─────────────────────────────────────────────────

    #[test]
    fn test_first_and_last() {
        let v: TypeVec<&str, Three> = empty().push("a").push("b").push("c");
        assert_eq!(*v.first(), "a");
        assert_eq!(*v.last(), "c");
    }

    // ── Statically-sized function arguments ───────────────────────────────────

    #[test]
    fn test_sum_three() {
        let v: TypeVec<i32, Three> = empty().push(10).push(20).push(30);
        assert_eq!(sum_three(&v), 60);
    }

    #[test]
    fn test_pair_to_tuple() {
        let v: TypeVec<i32, Two> = empty().push(7).push(13);
        assert_eq!(pair_to_tuple(&v), (7, 13));
    }

    // ── Type-level length matches runtime length ──────────────────────────────

    #[test]
    fn test_type_level_equals_runtime() {
        let v4: TypeVec<u8, Four> = empty().push(0).push(1).push(2).push(3);
        assert_eq!(v4.len(), Four::VALUE);
        assert_eq!(v4.len(), 4);
    }
}

(* 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"

✓ Tests Rust test suite

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

    // ── Nat trait ────────────────────────────────────────────────────────────

    #[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);
        assert_eq!(Five::VALUE, 5);
    }

    #[test]
    fn test_nat_const_eval() {
        const N: usize = Three::VALUE;
        assert_eq!(N, 3);
    }

    // ── Type-level addition ───────────────────────────────────────────────────

    #[test]
    fn test_add_zero_identity() {
        assert_eq!(<Zero as Add<Three>>::Sum::VALUE, 3);
        assert_eq!(<Three as Add<Zero>>::Sum::VALUE, 3);
    }

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

    // ── TypeVec: empty ────────────────────────────────────────────────────────

    #[test]
    fn test_empty_vec() {
        let v: TypeVec<i32, Zero> = empty();
        assert_eq!(v.len(), 0);
        assert!(v.is_empty());
        assert_eq!(v.len(), Zero::VALUE);
    }

    // ── TypeVec: push increments the type ─────────────────────────────────────

    #[test]
    fn test_push_increments_type() {
        let v0: TypeVec<i32, Zero> = empty();
        let v1: TypeVec<i32, One> = v0.push(10);
        let v2: TypeVec<i32, Two> = v1.push(20);
        let v3: TypeVec<i32, Three> = v2.push(30);

        assert_eq!(v3.len(), 3);
        assert_eq!(v3.len(), Three::VALUE);
        assert_eq!(v3.as_slice(), &[10, 20, 30]);
    }

    // ── TypeVec: pop decrements the type ──────────────────────────────────────

    #[test]
    fn test_pop_decrements_type() {
        let v3: TypeVec<i32, Three> = empty().push(1).push(2).push(3);
        let (v2, last): (TypeVec<i32, Two>, i32) = v3.pop();
        assert_eq!(last, 3);
        assert_eq!(v2.len(), 2);

        let (v1, mid): (TypeVec<i32, One>, i32) = v2.pop();
        assert_eq!(mid, 2);
        assert_eq!(v1.len(), 1);

        let (v0, first): (TypeVec<i32, Zero>, i32) = v1.pop();
        assert_eq!(first, 1);
        assert_eq!(v0.len(), 0);
        // v0.pop() would not compile — pop is not defined for TypeVec<T, Zero>.
    }

    // ── TypeVec: first / last ─────────────────────────────────────────────────

    #[test]
    fn test_first_and_last() {
        let v: TypeVec<&str, Three> = empty().push("a").push("b").push("c");
        assert_eq!(*v.first(), "a");
        assert_eq!(*v.last(), "c");
    }

    // ── Statically-sized function arguments ───────────────────────────────────

    #[test]
    fn test_sum_three() {
        let v: TypeVec<i32, Three> = empty().push(10).push(20).push(30);
        assert_eq!(sum_three(&v), 60);
    }

    #[test]
    fn test_pair_to_tuple() {
        let v: TypeVec<i32, Two> = empty().push(7).push(13);
        assert_eq!(pair_to_tuple(&v), (7, 13));
    }

    // ── Type-level length matches runtime length ──────────────────────────────

    #[test]
    fn test_type_level_equals_runtime() {
        let v4: TypeVec<u8, Four> = empty().push(0).push(1).push(2).push(3);
        assert_eq!(v4.len(), Four::VALUE);
        assert_eq!(v4.len(), 4);
    }
}

Deep Comparison

OCaml vs Rust: Type-Level Natural Numbers

Side-by-Side Code

OCaml (GADT approach)

type zero = Zero_t
type 'n succ = Succ_t

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

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

(* Length-indexed list — 'n encodes the length *)
type (_, _) vec =
  | Nil  : ('a, zero nat) vec
  | Cons : 'a * ('a, 'n nat) vec -> ('a, 'n succ nat) vec

Rust (marker-type approach)

use std::marker::PhantomData;

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

pub 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; }

pub type One   = Succ<Zero>;
pub type Two   = Succ<One>;
pub type Three = Succ<Two>;

Rust (length-indexed vector — `pop` only on non-empty)

pub struct TypeVec<T, N: Nat> {
    data: Vec<T>,
    _len: PhantomData<N>,
}

// push is available for any N — returns Succ<N>
impl<T, N: Nat> TypeVec<T, N> {
    pub fn push(mut self, value: T) -> TypeVec<T, Succ<N>> { … }
}

// pop is ONLY available for Succ<N> — popping Zero is a compile error
impl<T, N: Nat> TypeVec<T, Succ<N>> {
    pub fn pop(mut self) -> (TypeVec<T, N>, T) { … }
}

Rust (type-level addition)

pub 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>;
}

// 2 + 3 = 5, verified at compile time:
assert_eq!(<Two as Add<Three>>::Sum::VALUE, 5);

Type Signatures

Concept	OCaml	Rust
Zero	`type zero = Zero_t`	`pub struct Zero;`
Successor	`type 'n succ = Succ_t`	`pub struct Succ<N>(PhantomData<N>);`
Nat reflection	`val to_int : 'n nat -> int`	`trait Nat { const VALUE: usize; }`
Length-indexed vec	`('a, 'n nat) vec`	`TypeVec<T, N: Nat>`
Type-level addition	type-level via GADTs	`trait Add<B>: Nat { type Sum: Nat; }`
Non-empty constraint	encoded in GADT constructor	`impl<T,N:Nat> TypeVec<T,Succ<N>>`

Key Insights

GADTs vs marker structs: OCaml uses GADTs to relate value-level constructors

(Zero, Succ) to type-level witnesses, giving a single unified term that carries both the value and its type index. Rust instead uses zero-sized marker structs (Zero, Succ<N>) — the type is the witness, and PhantomData ensures the struct is zero-cost.

Trait-based reflection: OCaml reads off the Peano number with a

pattern-matching function (to_int). Rust uses a trait constant Nat::VALUE, which the compiler evaluates at compile time; no runtime dispatch occurs.

Method-level safety: OCaml enforces non-emptiness through exhaustiveness of

the GADT pattern — the Nil case just isn't present in the function. Rust achieves the same by scoping the pop, first, and last methods to impl<T,N:Nat> TypeVec<T,Succ<N>>: calling them on TypeVec<T,Zero> is a hard compile error because the method literally doesn't exist for that type.

Associated-type arithmetic: Type-level addition in OCaml requires a GADT

proof term that the compiler carries through. In Rust, associated types on a trait (type Sum: Nat) let the compiler compute Add::Sum entirely at the type level — no value is constructed, only types are resolved.

Zero cost at runtime: Both approaches impose zero overhead. Rust's marker

structs and PhantomData are erased entirely; TypeVec<T,N> is representation-equivalent to Vec<T> — the length type parameter exists only during compilation.

When to Use Each Style

Use idiomatic Rust (marker structs + trait constants) when you need compile-time length guarantees without a dependently-typed language — e.g., safe API contracts for fixed-size buffers, cryptographic keys, matrix dimensions, or protocol framing fields where the wrong size must be a build error, not a panic.

Use the recursive/GADT style (closer to OCaml) when you are porting dependently typed OCaml/Haskell code and want to preserve the structural correspondence, or when you need type-level arithmetic (addition, comparison) that benefits from the inductive structure being explicit in the trait implementations.

Exercises

Implement type Three = Succ<Two> and verify Three::VALUE == 3 in a test.

Add a Sub trait for type-level subtraction, defining Succ<N> - Succ<M> = N - M and Succ<N> - Zero = Succ<N>.

Implement a SafeStack<T, N: Nat> where push returns SafeStack<T, Succ<N>> and pop returns (T, SafeStack<T, N>), preventing pop on empty stack.

Open Source Repos

functional-rust

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

Rust