141 Expert

Singleton Types

Functional Programming

Tutorial Video

Text description (accessibility)

This video demonstrates the "Singleton Types" functional Rust example. Difficulty level: Expert. Key concepts covered: Functional Programming. A singleton type has exactly one value — the type and its single inhabitant are isomorphic. Key difference from OCaml: 1. **Pattern matching**: OCaml's GADT singletons can be matched to recover the underlying value; Rust's trait

Tutorial

The Problem

A singleton type has exactly one value — the type and its single inhabitant are isomorphic. Singleton types bridge the gap between values and types, enabling dependent-type-like programming where a runtime value is "promoted" to the type level. This is used in type-safe array indexing (a bound checked once becomes a type-level certificate), in protocol specifications, and in any setting where you want to carry proof of a runtime fact in the type system.

🎯 Learning Outcomes

• Understand what singleton types are and how they connect runtime values to type-level information

• Learn the Singleton trait pattern in Rust: a type with a unique VALUE constant

• See how singletons enable safe array access without repeated bounds checks

• Understand the relationship to dependent types in Agda, Coq, and Idris

Code Example

#![allow(clippy::all)]
// Stub — awaiting conversion from OCaml source.

(* Singleton types: each type has exactly one value.
   Used for type-level tags and phantom types. *)

(* Unit type — the canonical singleton *)
let () =
  let u : unit = () in
  Printf.printf "unit value: %s\n" (if u = () then "()" else "impossible");

  (* Phantom type tags as singletons *)
  ()

(* GADT encoding of type-level naturals as singletons *)
type zero  = ZERO
type 'n succ = SUCC

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

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

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

let () =
  Printf.printf "zero = %d\n" (to_int zero);
  Printf.printf "one  = %d\n" (to_int one);
  Printf.printf "two  = %d\n" (to_int two)

(* Singleton bool: type-level true/false *)
type tru = TRU
type fls = FLS

type _ bool_s =
  | True  : tru bool_s
  | False : fls bool_s

let () =
  let _t : tru bool_s = True  in
  let _f : fls bool_s = False in
  Printf.printf "Singleton types compile and run\n"

Key Differences

Pattern matching: OCaml's GADT singletons can be matched to recover the underlying value; Rust's trait-based singletons use const VALUE for recovery.

Dependent functions: OCaml's GADT singletons enable locally dependent functions; Rust achieves similar effects but with more boilerplate.

Erasure: Both approaches erase singleton types at runtime (zero-sized types in Rust, phantom types in OCaml); the singleton value is recovered from VALUE or pattern matching, not stored.

Practical limit: Rust's const generics (example 126) often serve as a more ergonomic alternative to singleton types for numeric domains.

OCaml Approach

OCaml can encode singleton types using GADTs where each constructor carries a unique type index:

type 'a sing =
  | STrue : bool sing
  | SFalse : bool sing
  | SZero : int sing
  | SSucc : 'n sing -> (int) sing

OCaml's GADTs allow the singleton value to be recovered from the type directly in pattern matches, making the bridge between types and values more natural than in Rust.

Full Source

#![allow(clippy::all)]
// Stub — awaiting conversion from OCaml source.

(* Singleton types: each type has exactly one value.
   Used for type-level tags and phantom types. *)

(* Unit type — the canonical singleton *)
let () =
  let u : unit = () in
  Printf.printf "unit value: %s\n" (if u = () then "()" else "impossible");

  (* Phantom type tags as singletons *)
  ()

(* GADT encoding of type-level naturals as singletons *)
type zero  = ZERO
type 'n succ = SUCC

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

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

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

let () =
  Printf.printf "zero = %d\n" (to_int zero);
  Printf.printf "one  = %d\n" (to_int one);
  Printf.printf "two  = %d\n" (to_int two)

(* Singleton bool: type-level true/false *)
type tru = TRU
type fls = FLS

type _ bool_s =
  | True  : tru bool_s
  | False : fls bool_s

let () =
  let _t : tru bool_s = True  in
  let _f : fls bool_s = False in
  Printf.printf "Singleton types compile and run\n"

Deep Comparison

OCaml vs Rust: Singleton Types

Overview

See the example.rs and example.ml files for detailed implementations.

Key Differences

Aspect	OCaml	Rust
Type system	Hindley-Milner	Ownership + traits
Memory	GC	Zero-cost abstractions
Mutability	Explicit ref	mut keyword
Error handling	Option/Result	Result<T, E>

See README.md for detailed comparison.

Exercises

Implement struct True; struct False; as Rust boolean singletons with a BoolSingleton trait and const VALUE: bool.

Write a BoundedIndex<const N: usize> type that can only be constructed when the index is less than N, providing a compile-time certificate of validity.

Implement to_runtime<S: Singleton<bool>>(s: S) -> bool that recovers the runtime value from the singleton type.

Open Source Repos

functional-rust

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

Rust