Skip to content

Instantly share code, notes, and snippets.

@aluqas
Last active April 30, 2026 22:27
Show Gist options
  • Select an option

  • Save aluqas/c7209b8990762db72620a87200f3e2aa to your computer and use it in GitHub Desktop.

Select an option

Save aluqas/c7209b8990762db72620a87200f3e2aa to your computer and use it in GitHub Desktop.
//! A self-contained type-level programming example in Rust.
//!
//! This file demonstrates:
//! - type-level booleans and branching
//! - Peano naturals and arithmetic
//! - a type-level HList-style array
//! - a `While` encoded with trait resolution
//! - Fibonacci sequence generation at compile time
//!
//! ## Why no const generics?
//! ¯\_(ツ)_/¯
#![allow(dead_code)]
#![recursion_limit = "1024"]
use std::marker::PhantomData;
/// Generic Paramator can't have type paramaters,
/// so Opcode structs such as `OpAdd` are empty, and the actual types are passed in the `Args` tuple of `Apply`.
trait Apply<Op, Args> {
type Output;
}
// ---------------------------------------------------------------------
// Type-level booleans and If
struct True;
struct False;
trait Bool {
const VAL: bool;
}
impl Bool for True {
const VAL: bool = true;
}
impl Bool for False {
const VAL: bool = false;
}
trait IfHelper<Then, Else> {
type Output;
}
impl<Then, Else> IfHelper<Then, Else> for True {
type Output = Then;
}
impl<Then, Else> IfHelper<Then, Else> for False {
type Output = Else;
}
type If<Cond, Then, Else> = <Cond as IfHelper<Then, Else>>::Output;
trait Not {
type Output;
}
impl Not for True {
type Output = False;
}
impl Not for False {
type Output = True;
}
struct OpIf;
impl<Cond, Then, Else> Apply<OpIf, (Cond, Then, Else)> for ()
where
Cond: IfHelper<Then, Else>,
{
type Output = <Cond as IfHelper<Then, Else>>::Output;
}
struct OpNot;
impl<T> Apply<OpNot, T> for ()
where
T: Not,
{
type Output = <T as Not>::Output;
}
// ---------------------------------------------------------------------
// Peano naturals
struct Zero;
struct Succ<T>(PhantomData<T>);
trait Nat {
const VAL: usize;
}
impl Nat for Zero {
const VAL: usize = 0;
}
impl<T: Nat> Nat for Succ<T> {
const VAL: usize = T::VAL + 1;
}
trait IsZero {
type Output;
}
impl IsZero for Zero {
type Output = True;
}
impl<T: Nat> IsZero for Succ<T> {
type Output = False;
}
trait Add<Rhs> {
type Output;
}
impl<Rhs: Nat> Add<Rhs> for Zero {
type Output = Rhs;
}
impl<Lhs: Nat, Rhs: Nat> Add<Rhs> for Succ<Lhs>
where
Lhs: Add<Rhs>,
{
type Output = Succ<<Lhs as Add<Rhs>>::Output>;
}
trait Mul<Rhs> {
type Output;
}
impl<Rhs: Nat> Mul<Rhs> for Zero {
type Output = Zero;
}
impl<Lhs: Nat, Rhs: Nat> Mul<Rhs> for Succ<Lhs>
where
Lhs: Mul<Rhs>,
Rhs: Add<<Lhs as Mul<Rhs>>::Output>,
{
type Output = <Rhs as Add<<Lhs as Mul<Rhs>>::Output>>::Output;
}
trait Pow<Rhs> {
type Output;
}
impl<N: Nat> Pow<Zero> for N {
type Output = Succ<Zero>;
}
impl<N: Nat, Exp: Nat> Pow<Succ<Exp>> for N
where
N: Pow<Exp>,
<N as Pow<Exp>>::Output: Mul<N>,
{
type Output = <<N as Pow<Exp>>::Output as Mul<N>>::Output;
}
trait Pred {
type Output;
}
impl Pred for Zero {
type Output = Zero;
}
impl<T: Nat> Pred for Succ<T> {
type Output = T;
}
trait Sub<Rhs> {
type Output;
}
impl<Rhs: Nat> Sub<Rhs> for Zero {
type Output = Zero;
}
impl<Lhs: Nat> Sub<Zero> for Succ<Lhs> {
type Output = Succ<Lhs>;
}
impl<Lhs: Nat, Rhs: Nat> Sub<Succ<Rhs>> for Succ<Lhs>
where
Lhs: Sub<Rhs>,
{
type Output = <Lhs as Sub<Rhs>>::Output;
}
struct OpAdd;
struct OpMul;
struct OpPow;
struct OpPred;
struct OpSub;
struct OpIsZero;
impl<Lhs, Rhs> Apply<OpAdd, (Lhs, Rhs)> for ()
where
Lhs: Add<Rhs>,
{
type Output = <Lhs as Add<Rhs>>::Output;
}
impl<Lhs, Rhs> Apply<OpMul, (Lhs, Rhs)> for ()
where
Lhs: Mul<Rhs>,
{
type Output = <Lhs as Mul<Rhs>>::Output;
}
impl<Lhs, Rhs> Apply<OpPow, (Lhs, Rhs)> for ()
where
Lhs: Pow<Rhs>,
{
type Output = <Lhs as Pow<Rhs>>::Output;
}
impl<T> Apply<OpPred, T> for ()
where
T: Pred,
{
type Output = <T as Pred>::Output;
}
impl<Lhs, Rhs> Apply<OpSub, (Lhs, Rhs)> for ()
where
Lhs: Sub<Rhs>,
{
type Output = <Lhs as Sub<Rhs>>::Output;
}
impl<T> Apply<OpIsZero, T> for ()
where
T: IsZero,
{
type Output = <T as IsZero>::Output;
}
// ---------------------------------------------------------------------
// Type-level variadic array / HList
trait TypeArray {}
struct TTerm;
struct TArr<Val, Arr: TypeArray>(PhantomData<(Val, Arr)>);
impl TypeArray for TTerm {}
impl<Val, Arr: TypeArray> TypeArray for TArr<Val, Arr> {}
#[macro_export]
macro_rules! tarr {
() => ($crate::TTerm);
($head:ty) => ($crate::TArr<$head, $crate::TTerm>);
($head:ty,) => ($crate::TArr<$head, $crate::TTerm>);
($head:ty, $($tail:ty),+) => ($crate::TArr<$head, tarr![$($tail),+]>);
($head:ty, $($tail:ty),+,) => ($crate::TArr<$head, tarr![$($tail),+]>);
($head:ty | $rest:ty) => ($crate::TArr<$head, $rest>);
($head:ty, $($tail:ty),+ | $rest:ty) => ($crate::TArr<$head, tarr![$($tail),+ | $rest]>);
}
trait Len {
type Output;
}
impl Len for TTerm {
type Output = Zero;
}
impl<Val, Arr: TypeArray> Len for TArr<Val, Arr>
where
Arr: Len,
{
type Output = Succ<<Arr as Len>::Output>;
}
trait Get<Idx: Nat> {
type Output;
}
impl<Val, Arr: TypeArray> Get<Zero> for TArr<Val, Arr> {
type Output = Val;
}
impl<Val, Arr: TypeArray, Idx: Nat> Get<Succ<Idx>> for TArr<Val, Arr>
where
Arr: Get<Idx>,
{
type Output = <Arr as Get<Idx>>::Output;
}
trait Set<T, Idx: Nat> {
type Output;
}
impl<Val, Arr: TypeArray, T> Set<T, Zero> for TArr<Val, Arr> {
type Output = TArr<T, Arr>;
}
impl<Val, Arr: TypeArray, T, Idx: Nat> Set<T, Succ<Idx>> for TArr<Val, Arr>
where
Arr: Set<T, Idx>,
<Arr as Set<T, Idx>>::Output: TypeArray,
{
type Output = TArr<Val, <Arr as Set<T, Idx>>::Output>;
}
trait Append<T> {
type Output;
}
impl<T> Append<T> for TTerm {
type Output = TArr<T, TTerm>;
}
impl<Val, Arr: TypeArray, T> Append<T> for TArr<Val, Arr>
where
Arr: Append<T>,
<Arr as Append<T>>::Output: TypeArray,
{
type Output = TArr<Val, <Arr as Append<T>>::Output>;
}
// ---------------------------------------------------------------------
// While
struct OpWhile;
trait WhileHelper<Pred, Step, State, Cond> {
type Output;
}
// If Cond is False, stop and return State
impl<Pred, Step, State> WhileHelper<Pred, Step, State, False> for () {
type Output = State;
}
// If Cond is True, apply Step to State, then loop again with the new state.
impl<Pred, Step, State> WhileHelper<Pred, Step, State, True> for ()
where
(): Apply<Step, State>,
(): Apply<Pred, <() as Apply<Step, State>>::Output>,
(): WhileHelper<
Pred,
Step,
<() as Apply<Step, State>>::Output,
<() as Apply<Pred, <() as Apply<Step, State>>::Output>>::Output,
>,
{
type Output = <() as WhileHelper<
Pred,
Step,
<() as Apply<Step, State>>::Output,
<() as Apply<Pred, <() as Apply<Step, State>>::Output>>::Output,
>>::Output;
}
impl<Pred, Step, State> Apply<OpWhile, (Pred, Step, State)> for ()
where
(): Apply<Pred, State>,
(): WhileHelper<Pred, Step, State, <() as Apply<Pred, State>>::Output>,
{
type Output = <() as WhileHelper<
Pred,
Step,
State,
<() as Apply<Pred, State>>::Output,
>>::Output;
}
// ---------------------------------------------------------------------
// Fibonacci function
type N0 = Zero;
type N1 = Succ<N0>;
type N2 = Succ<N1>;
struct FibPred<N: Nat>(PhantomData<N>);
// FibPred implementation
// counter == 0 => False, so stop
// counter != 0 => True, so continue
impl<N: Nat, State: TypeArray> Apply<FibPred<N>, State> for ()
where
State: Len,
<State as Len>::Output: Sub<N>,
<<State as Len>::Output as Sub<N>>::Output: IsZero,
{
type Output =
<<<State as Len>::Output as Sub<N>>::Output as IsZero>::Output;
}
// Read the last two elements from Result
type IdxLast<Arr> = <<Arr as Len>::Output as Sub<N1>>::Output;
type LastValue<Arr> =
<Arr as Get<IdxLast<Arr>>>::Output;
type IdxPrev<Arr> = <<Arr as Len>::Output as Sub<N2>>::Output;
type PrevValue<Arr> =
<Arr as Get<IdxPrev<Arr>>>::Output;
type NextFib<Arr> = <PrevValue<Arr> as Add<LastValue<Arr>>>::Output;
struct FibStep;
// FibStep implementation
// Append NextFib
impl<Arr: TypeArray> Apply<FibStep, Arr> for ()
where
Arr: Len,
<Arr as Len>::Output: Sub<N1> + Sub<N2>,
IdxLast<Arr>: Nat,
IdxPrev<Arr>: Nat,
Arr: Get<IdxLast<Arr>>,
Arr: Get<IdxPrev<Arr>>,
PrevValue<Arr>: Add<LastValue<Arr>>,
Arr: Append<NextFib<Arr>>,
{
type Output = <Arr as Append<NextFib<Arr>>>::Output;
}
// If you do not like hardcoding tarr![N0, N1], you could implement
// Apply<FibStep, TTail> and Apply<FibStep, TArr<N0, TTail>> instead.
// This example keeps the simpler version.
type Fib<N> = <() as Apply<OpWhile, (FibPred<N>, FibStep, tarr![N0, N1])>>::Output;
fn main() {}
#[cfg(test)]
mod tests {
use super::*;
trait Same<T> {}
impl<T> Same<T> for T {}
fn assert_same<A, B>()
where
A: Same<B>,
{
}
type N0 = Zero;
type N1 = Succ<N0>;
type N2 = Succ<N1>;
type N3 = Succ<N2>;
type N4 = Succ<N3>;
type N5 = Succ<N4>;
type N6 = Succ<N5>;
type N7 = Succ<N6>;
type N8 = Succ<N7>;
type N9 = Succ<N8>;
type N10 = Succ<N9>;
#[test]
fn test_if_and_bool() {
assert_same::<If<True, N2, N3>, N2>();
assert_same::<If<False, N2, N3>, N3>();
assert_eq!(True::VAL, true);
assert_eq!(False::VAL, false);
assert_eq!(<() as Apply<OpNot, True>>::Output::VAL, false);
assert_eq!(<() as Apply<OpNot, False>>::Output::VAL, true);
}
#[test]
fn test_nat_operations() {
assert_eq!(N3::VAL, 3);
assert_eq!(<N2 as Add<N3>>::Output::VAL, 5);
assert_eq!(<N2 as Mul<N3>>::Output::VAL, 6);
assert_eq!(<N2 as Pow<N3>>::Output::VAL, 8);
assert_eq!(<N6 as Sub<N2>>::Output::VAL, 4);
assert_eq!(<N2 as Sub<N3>>::Output::VAL, 0);
}
#[test]
fn test_apply_wrappers() {
assert_eq!(<() as Apply<OpAdd, (N2, N3)>>::Output::VAL, 5);
assert_eq!(<() as Apply<OpMul, (N2, N3)>>::Output::VAL, 6);
assert_eq!(<() as Apply<OpPow, (N2, N3)>>::Output::VAL, 8);
assert_eq!(<() as Apply<OpPred, N3>>::Output::VAL, 2);
assert_eq!(<() as Apply<OpSub, (N3, N2)>>::Output::VAL, 1);
assert_eq!(<() as Apply<OpIsZero, Zero>>::Output::VAL, true);
assert_eq!(<() as Apply<OpIsZero, N1>>::Output::VAL, false);
assert_same::<
<() as Apply<OpIf, (True, N2, N3)>>::Output,
N2,
>();
}
#[test]
fn test_type_array() {
type Numbers = tarr![N2, N1, N0];
type Updated = <Numbers as Set<N3, N1>>::Output;
type Appended = <Numbers as Append<N3>>::Output;
assert_eq!(<Numbers as Len>::Output::VAL, 3);
assert_eq!(<Numbers as Get<N0>>::Output::VAL, 2);
assert_eq!(<Numbers as Get<N1>>::Output::VAL, 1);
assert_eq!(<Updated as Get<N1>>::Output::VAL, 3);
assert_eq!(<Updated as Get<N2>>::Output::VAL, 0);
assert_eq!(<Appended as Len>::Output::VAL, 4);
assert_eq!(<Appended as Get<N3>>::Output::VAL, 3);
}
#[test]
fn test_fibonacci_sequence_as_tarr() {
type Seq0 = Fib<N0>;
type Seq1 = Fib<N1>;
type Seq2 = Fib<N2>;
type Seq6 = Fib<N6>;
type Seq10 = Fib<N10>;
assert_same::<Seq0, tarr![N0, N1]>();
assert_same::<Seq1, tarr![N0, N1]>();
assert_same::<Seq2, tarr![N0, N1, N1]>();
assert_same::<Seq6, tarr![N0, N1, N1, N2, N3, N5, N8]>();
assert_eq!(<Seq10 as Get<N9>>::Output::VAL, 34);
assert_eq!(<Seq10 as Get<N10>>::Output::VAL, 55);
let result = "
TArr<
Zero,
TArr<
Succ<Zero>,
TArr<
Succ<Zero>,
TArr<
Succ<Succ<Zero>>,
TArr<
Succ<Succ<Succ<Zero>>>,
TArr<
Succ<Succ<Succ<Succ<Succ<Zero>>>>>,
TArr<
Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>,
TArr<
Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>,
TArr<
Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>,
TArr<
Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>,
TArr<
Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>,
TTerm
>
>
>
>
>
>
>
>
>
>
>";
let prefix = std::any::type_name::<TTerm>()
.strip_suffix("TTerm")
.unwrap();
assert_eq!(
std::any::type_name::<Seq10>().replace(prefix, "").replace(" ", ""),
result.replace(" ", "").replace("\n", "")
);
println!("Fib<10> = {}", std::any::type_name::<Seq10>());
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment