Adding two natural numbers in rust the typesafe way.

main.rs

trait Nat {}

#[derive(Debug, PartialEq, Copy, Clone)] enum Zero{Zero}
#[derive(Debug, PartialEq, Copy, Clone)] enum Suc<N>{Suc(N)}

impl Nat for Zero{}
impl<N: Nat> Nat for Suc<N>{}

fn add_two<N: Nat>(n: N) -> Suc<Suc<N>> { Suc::Suc(Suc::Suc(n)) }

fn compiletime_equal<T>(_a: T, _b: T){}

trait Adder<M: Nat, R: Nat>{
    fn add(&self, m: M) -> R;
}
impl<M: Nat> Adder<M, M> for Zero {
    fn add(&self, m: M) -> M { m }
}
impl<N, M: Nat, R: Nat> Adder<M, Suc<R>> for Suc<N>
    where N: Nat + Adder<M, R> {
    fn add(&self, m: M) -> Suc<R> {
        let Suc::Suc(n) = self;
        Suc::Suc(n.add(m))
    }
}

trait MachineNat { fn to(&self) -> u32; }
impl MachineNat for Zero { fn to(&self) -> u32 { 0 } }
impl<N: Nat + MachineNat> MachineNat for Suc<N> {
    fn to(&self) -> u32 { let Suc::Suc(n) = self; n.to() + 1 }
}

fn main() {
    use Suc::Suc as S;
    use Zero::Zero as Z;
    
    let three: Suc<Suc<Suc<Zero>>>                          = S(S(S(Z)));
    let five : Suc<Suc<Suc<Suc<Suc<Zero>>>>>                = S(S(S(S(S(Z)))));
    let eight: Suc<Suc<Suc<Suc<Suc<Suc<Suc<Suc<Zero>>>>>>>> = S(S(S(S(S(S(S(S(Z))))))));
    
    println!("add_two(three): add_two({}) = {}", three.to(), add_two(three).to());
    assert_eq!(add_two(three), five);
    compiletime_equal(add_two(three), five);
    
    let _: Suc<Suc<Suc<Suc<Suc<Suc<Suc<Suc<Zero>>>>>>>> = three.add(five);
    println!("three.add(five): {}.add({}) = {}", three.to(), five.to(), three.add(five).to());
    assert_eq!(three.add(five), eight);
    compiletime_equal(three.add(five), eight);
}