addition_on_types.rs

use std::marker::PhantomData;

trait Nat { }

struct _0 { }
impl Nat for _0 { }

struct Suc<T: Nat> {
    n: PhantomData<T>,
}
impl<T: Nat> Nat for Suc<T> { }

type _1 = Suc<_0>;
type _2 = Suc<_1>;
type _3 = Suc<_2>;
type _4 = Suc<_3>;
type _5 = Suc<_4>;
type _6 = Suc<_5>;
type _7 = Suc<_6>;
type _8 = Suc<_7>;
type _9 = Suc<_8>;

trait Eval {
    fn eval() -> i32;
}
impl Eval for _0 {
    fn eval() -> i32 { 0 }
}
impl<T: Nat + Eval> Eval for Suc<T> {
    fn eval() -> i32 { T::eval() + 1 }
}

struct Plus<Lhs: Nat, Rhs: Nat> {
    lhs: PhantomData<Lhs>,
    rhs: PhantomData<Rhs>,
}

trait Sum {
    type Type: Nat;
}

impl<T: Nat> Sum for Plus<_0, T> {
    type Type = T;
}
impl<S: Nat, T: Nat> Sum for Plus<Suc<S>, T> where Plus<S, Suc<T>>: Sum {
    type Type = <Plus<S, Suc<T>> as Sum>::Type;
}

impl<T: Sum> Eval for T where T::Type: Eval {
    fn eval() -> i32 { T::Type::eval() }
}

fn main() {
    println!("{}", _9::eval());
    println!("{}", <Plus<_4, _2>>::eval());
}