Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
Example of typed functional programming in Rust's type-level language
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
{ type T0=T0; type T1=T1; type T2=T2; type T3=T3; }
trait Func3<A,B,C> : TypedFunc3 where
{ 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
Add : Func2<A,B,Result=R0>,
Add : Func2<R0,C,Result=R1>,
{ type Result = R1; }
type Six = <Add3 as Func3<One,Two,Three>>::Result;
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))))));
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.