Example of typed functional programming in Rust's type-level language

traitlang.rs

trait Nat {}
struct Zero;
impl Nat for Zero {}
struct Succ<N>(N);
impl<N:Nat> Nat for Succ<N> {}

type One = Succ <Zero >;

trait AddOne : Nat { type Result:Nat; }
impl<N:Nat> AddOne for N { type Result = Succ<N>; }
trait SubOne : Nat { type Result:Nat; }
impl<N:Nat> SubOne for Succ<N> { type Result = N; }

type Two = <One as AddOne >::Result;

trait Func2 <A,B> { type Result; }

struct Add;
impl<N:Nat> Func2 <Zero,N> for Add { type Result = N;}
impl<N1,N2> Func2<Succ<N1>,N2> for Add where
    N1:Nat, N2:Nat,
    Add : Func2<N1,N2>
{ type Result = Succ<<Add as Func2<N1,N2>>::Result>; }

type Three = <Add as Func2<One,Two>>::Result;

trait Typed { type Type; }

struct Natural;
impl Typed for Zero { type Type = Natural; }
impl<N:Typed<Type=Natural>> Typed for Succ<N> { type Type = Natural; }

trait Func1 <A:Typed > { type Result:Typed; }

struct Next;
impl<N:Typed<Type=Natural>> Func1<N> for Next { type Result = Succ<N>; }

type Four = <Next as Func1<Three>>::Result;

struct Apply;
impl <A,B,R> Func2 <A,B> for Apply where
    B: Typed, R: Typed,
    A: Func1 <B,Result=R>
{ type Result = R; }

type Five = <Apply as Func2<Next,Four>>::Result;

struct Arrow3<T0,T1,T2,T3>(T0,T1,T2,T3);
trait TypedFunc3 {type T0; type T1; type T2; type T3;}
impl<T0,T1,T2,T3,A> TypedFunc3 for A where
    A:Typed<Type=Arrow3<T0,T1,T2,T3>>
{ type T0=T0; type T1=T1; type T2=T2; type T3=T3; }
trait Func3<A,B,C> : TypedFunc3 where
    A:Typed<Type=Self::T0>,
    B:Typed<Type=Self::T1>,
    C:Typed<Type=Self::T2>,
{ type Result:Typed<Type=Self::T3>; }

struct Add3;
impl Typed for Add3 { type Type=Arrow3<Natural,Natural,Natural,Natural>; }
impl<A,B,C,R0,R1> Func3<A,B,C> for Add3 where
    A:Typed<Type=Natural>,
    B:Typed<Type=Natural>,
    C:Typed<Type=Natural>,
    R1:Typed<Type=Natural>,
    Add : Func2<A,B,Result=R0>,
    Add : Func2<R0,C,Result=R1>,
{ type Result = R1; }

type Six = <Add3 as Func3<One,Two,Three>>::Result;

#[allow(unused)]
struct AddOneTwo;
impl Typed for AddOneTwo
{ type Type=Arrow3<Natural,Natural,Natural,Natural>; }
impl Func3<One,Two,Zero> for AddOneTwo  { type Result=Three; }
impl Func3<One,Two,One> for AddOneTwo  { type Result=Four; }
impl Func3<One,Two,Two> for AddOneTwo  { type Result=Five; }


fn main() {
    let _one: One = Succ(Zero);
    let _two: Two = Succ(Succ(Zero));
    let _three: Three = Succ(Succ(Succ(Zero)));
    let _four: Four = Succ(Succ(Succ(Succ(Zero))));
    let _five: Five = Succ(Succ(Succ(Succ(Succ(Zero)))));
    let _six: Six = Succ(Succ(Succ(Succ(Succ(Succ(Zero))))));
}