church.rs

#[feature(macro_rules)];

use std::fmt;
use std::ops;

///////////////////////////////////////
////////// Basic Definitions //////////
///////////////////////////////////////

// Zero numeral, and a Successor operator
enum Zero {}
enum Succ<A> {}

// Some common named numerals
type One = Succ<Zero>;
type Two = Succ<One>;
type Three = Succ<Two>;

//////////////////////////////////////////////
////////// Types -> uint conversion //////////
//////////////////////////////////////////////

// A trait to get a normal uint out of the type.
// The Option<Self> hack is a way to specify what Church implementation
// to use, by providing a value involving Self but not actually containing
// any values of type Self. Call like so:
//     let x: Option<A> = None;
//     Church::to_value(x)
trait Church {
    fn to_value(_: Option<Self>) -> uint;
}

// A macro that encapsulates the above into just: church_value!(A)
macro_rules! church_value(
    ($t:ty) => (
        {
            let x: Option<$t> = None;
            Church::to_value(x)
        }
    )
)

// implementations of Church for Zero and Succ<A>
impl Church for Zero {
    fn to_value(_: Option<Zero>) -> uint { 0 }
}
impl<A: Church> Church for Succ<A> {
    fn to_value(_: Option<Succ<A>>) -> uint { 1 + church_value!(A) }
}

//////////////////////////////
////////// Addition //////////
//////////////////////////////

// a trait abused to add numerals
// in a set of type arguments, <RHS, Result, A: ChurchAdd<RHS, Result> will
// force Result to be A + RHS
trait ChurchAdd<RHS, Result> {}

// an implementation for Zero + RHS = RHS
impl<RHS> ChurchAdd<RHS, RHS> for Zero {}

// an implementation for Succ<A> + RHS = A + Succ<RHS>
impl<RHS, Result, A: ChurchAdd<Succ<RHS>, Result>> ChurchAdd<RHS, Result> for Succ<A> {}

/////////////////////////////////////////////
////////// Example Usage: SI Units //////////
/////////////////////////////////////////////

// A type annotated with SI units, with powers encoded as types
struct SI<N, Meters, Seconds>(N);

// helper methods to get the type powers of a value
impl<N, Meters: Church, Seconds: Church> SI<N, Meters, Seconds> {
    fn get_meters(&self) -> uint { church_value!(Meters) }
    fn get_seconds(&self) -> uint { church_value!(Seconds) }
}

// if N has a fmt::Default implementation, then so does SI<N, ...>
impl<N: fmt::Default, Meters: Church, Seconds: Church> fmt::Default for SI<N, Meters, Seconds> {
    fn fmt(v: &SI<N, Meters, Seconds>, f: &mut fmt::Formatter) {
        match *v {
            SI(ref n) => write!(f.buf, "{} m^{} s^{}", *n, v.get_meters(), v.get_seconds())
        }
    }
}

// if N + RHS is valid, then so is SI<N, ...> + SI<RHS, ...>, but only if
// the units on both sides have the same value
impl<RHS, Result, N: ops::Add<RHS, Result>, Meters, Seconds> ops::Add<SI<RHS, Meters, Seconds>, SI<Result, Meters, Seconds>> for SI<N, Meters, Seconds> {
    fn add(&self, rhs: &SI<RHS, Meters, Seconds>) -> SI<Result, Meters, Seconds> {
        match (self, rhs) {
            (&SI(ref n), &SI(ref r)) => SI(*n + *r)
        }
    }
}

// if N * RHS is valid, then so is SI<N, ...> * SI<RHS, ...>, and the resulting
// units are the sum of the component units, component-wise
impl<RHS, Result, N: ops::Mul<RHS, Result>, RMeters, ResMeters, Meters: ChurchAdd<RMeters, ResMeters>, RSeconds, ResSeconds, Seconds: ChurchAdd<RSeconds, ResSeconds>> ops::Mul<SI<RHS, RMeters, RSeconds>, SI<Result, ResMeters, ResSeconds>> for SI<N, Meters, Seconds> {
    fn mul(&self, rhs: &SI<RHS, RMeters, RSeconds>) -> SI<Result, ResMeters, ResSeconds> {
        match (self, rhs) {
            (&SI(ref n), &SI(ref r)) => SI(*n * *r)
        }
    }
}

// an example
fn main() {
    let a: SI<int, One, One> = SI(4);
    let b: SI<int, One, One> = SI(5);
    let c: SI<int, Two, One> = SI(-1);
    println!("a = {}", a);
    println!("b = {}", b);
    println!("c = {}", c);
    
    println!("a + b = {}", a + b);
    // the following is a type error, as it adds m^1 s^1 to m^2 s^1
    //println!("a + c = {}", a + c);
    
    println!("a * c = {}", a * c);
}