Type-level add

add_types.rs

#[allow(dead_code)]
use std::default::Default;
use std::fmt::{Show, Formatter, Error};

trait Value: Default + Show {}

trait Church: Value {
    fn as_int(self) -> int;
}

#[deriving(Default)]
struct Zero;
impl Value for Zero {}
impl Church for Zero {
    fn as_int(self) -> int { 0 }
}

#[deriving(Default)]
struct Succ<P: Church>;
impl<P: Church> Value for Succ<P> {}
impl<P: Church> Church for Succ<P> {
    fn as_int(self) -> int {
        let p: P = Default::default();
        p.as_int() + 1
    }
}

impl Show for Zero {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        write!(f, "0")
    }
}

impl<P: Church> Show for Succ<P> {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        write!(f, "{}", self.as_int())
    }
}

// PlusOne: A -> R
trait PlusOne<A: Church, R: Church> {}
impl<A: Church> PlusOne<A, Succ<A>> for () {}

// MinusOne: A -> R
trait MinusOne<A: Church, R: Church> {}
impl MinusOne<Zero, Zero> for () {}
impl<P: Church> MinusOne<Succ<P>, P> for () {}

// Add: A, B -> R
trait Add<A: Church, B: Church, R: Church> {}
impl<A: Church> Add<A, Zero, A> for () {}
impl<A: Church, P: Church, R: Church, N> Add<A, Succ<P>, R> for ()
    where N: Add<Succ<A>, P, R> {}

fn add<A: Church, B: Church, R: Church, N>(_a: A, _b: B) -> R
    where N: Add<A, B, R>{ Default::default() }
    
type Two = Succ<Succ<Zero>>;
type Three = Succ<Two>;


fn main() {
    let a: Two = Default::default();
    let b: Three = Default::default();
    println!("{}", add(a, b));
}