peano_arithmetic_in_rust_type_system.rs

use std::any::type_name;
use std::marker::PhantomData;

trait Ordering {}
struct Less;
struct Equal;
struct Greater;
impl Ordering for Less {}
impl Ordering for Equal {}
impl Ordering for Greater {}

trait N {}
struct Z;
struct S<X: N>(PhantomData<X>);
impl N for Z {}
impl<X: N> N for S<X> {}

type N0 = Z;
type N1 = S<N0>;
type N2 = S<N1>;
type N3 = S<N2>;

trait Compare<B: N> {
    type Result: Ordering;
}

impl<A: N> Compare<S<A>> for Z {
    type Result = Less;
}

impl Compare<Z> for Z {
    type Result = Equal;
}

impl<A: N> Compare<Z> for S<A> {
    type Result = Greater;
}

impl<A: N + Compare<B>, B: N> Compare<S<B>> for S<A> {
    type Result = <A as Compare<B>>::Result;
}

trait Add<B: N> {
    type Result: N;
}

impl<A: N> Add<Z> for A {
    type Result = A;
}

impl<A: N + Add<B>, B: N> Add<S<B>> for A {
    type Result = S<<A as Add<B>>::Result>;
}

trait Mul<B: N> {
    type Result: N;
}

impl<A: N> Mul<Z> for A {
    type Result = Z;
}

impl<A: N + Mul<B> + Add<<A as Mul<B>>::Result>, B: N> Mul<S<B>> for A {
    type Result = <A as Add<<A as Mul<B>>::Result>>::Result;
}

fn main() {
    println!("{}", type_name::<<N1 as Compare<N3>>::Result>());
    println!("{}", type_name::<<N2 as Compare<N2>>::Result>());
    println!("{}", type_name::<<N3 as Compare<N1>>::Result>());
    println!("{}", type_name::<<N2 as Add<N3>>::Result>());
    println!("{}", type_name::<<N2 as Mul<N3>>::Result>());
}