Shared via Rust Playground

playground.rs

#![feature(optin_builtin_traits)]
use std::marker::PhantomData;

struct Nil;
struct Cons<H, T>(H, T);

struct Pair<A, B>(A, B);

trait Lookup_<S, Env> { type Type; }
type Lookup<S, Env> = <() as Lookup_<S, Env>>::Type;

trait NotKeyMatch {}
impl NotKeyMatch for .. {}
impl<K, V> !NotKeyMatch for (K, Pair<K, V>) {}

impl<K, X, XS>
Lookup_<K, Cons<X, XS>> for ()
where (): Lookup_<K, XS>, (K, X): NotKeyMatch
{ type Type = Lookup<K, XS>; }

impl<K, V, XS>
Lookup_<K, Cons<Pair<K, V>, XS>> for ()
{ type Type = V; }

trait Eval_<T, Env> { type Type; }
type Eval<T, Env> = <() as Eval_<T, Env>>::Type;

struct App<F, A>(PhantomData<(F, A)>);
struct Fn<X, E>(PhantomData<(X, E)>);
struct Ref<X>(PhantomData<X>);
struct Closure<X, E, Env>(PhantomData<(X, E, Env)>);
//struct Fix_<F>(PhantomData<F>);
struct Fixed<F>(PhantomData<F>);

trait NotAction {}
impl NotAction for .. {}
impl<X, E> !NotAction for Fn<X, E> {}
impl<F, A> !NotAction for App<F, A> {}
impl<X> !NotAction for Ref<X> {}
//impl<F> !NotAction for Fix_<F> {}

impl<X, Env>
Eval_<Ref<X>, Env> for ()
where (): Lookup_<X, Env>
{ type Type = Lookup<X, Env>; }

impl<X, E, Env>
Eval_<Fn<X, E>, Env> for ()
{ type Type = Closure<X, E, Env>; }
/*
impl<F, Env>
Eval_<Fix_<F>, Env> for ()
where (): Eval_<F, Env>
{ type Type = Fixed<Eval<F, Env>>; }
*/
trait Apply_<C, A> { type Type; }
type Apply<C, A> = <() as Apply_<C, A>>::Type;

impl<X, E, Env, A>
Apply_<Closure<X, E, Env>, A> for ()
where (): Eval_<E, Cons<Pair<X, A>, Env>>
{ type Type = Eval<E, Cons<Pair<X, A>, Env>>; }
/*
impl<F, A>
Apply_<Fixed<F>, A> for ()
where ():
Apply_<F, Fixed<F>> +
Apply_<Apply<F, Fixed<F>>, A>
{ type Type = Apply<Apply<F, Fixed<F>>, A>; }//Eval<, Nil>; }
*/
impl<F, A, Env>
Eval_<App<F, A>, Env> for ()
where ():
Eval_<F, Env> +
Eval_<A, Env> +
Apply_<Eval<F, Env>, Eval<A, Env>>
{ type Type = Apply<Eval<F, Env>, Eval<A, Env>>; }

impl<T, Env>
Eval_<T, Env> for ()
where T: NotAction
{ type Type = T; }

fn foo<F, A>() -> Apply<Apply<F, Fixed<F>>, A>
where ():
Apply_<F, Fixed<F>> +
Apply_<Apply<F, Fixed<F>>, A>
{ unimplemented!() }

/////////////////////////////////
//Helpers:
type Fn2<P1, P2, E> = Fn<P1, Fn<P2, E>>;
type Fn3<P1, P2, P3, E> = Fn<P1, Fn<P2, Fn<P3, E>>>;
type App2<F, A1, A2> = App<App<F, A1>, A2>;
type App3<F, A1, A2, A3> = App<App<App<F, A1>, A2>, A3>;
/////////////////////////////////

fn main() {
    // Type level identifiers - any type will do
    struct X; struct Y; struct A; struct B; struct F;
    
    type Id = Fn<X, Ref<X>>; // simple identity function
    type Bool = Eval<App<Id, bool>, Nil>; // should be `bool`
    let _: PhantomData<bool> = PhantomData::<Bool>; // check result
    //let y: Bool = true; // Unfortunately fails due to rust bug #28828
    
    // Church booleans
    type True = Fn2<X, Y, Ref<X>>;
    type False = Fn2<X, Y, Ref<Y>>;
    // Conditional
    type If = Id;
    // Example
    type U32 = Eval<App3<If, True, u32, bool>, Nil>;
    let _: PhantomData<u32> = PhantomData::<U32>; // check result
    
    type C = Eval<Fn2<F, X, Ref<X>>, Nil>;
    //let _: () = PhantomData::<C>;
    let _: () = foo::<C, bool>();
    /*
    type Inner = Fn<X, App<F, App<X, X>>>;
    type Fix = Fn<F, App<Inner, Inner>>;
    
    type Foo = App<Fix, Fn<Y, bool>>;
    
    type Bool2 = Eval<Foo, Nil>;
    
    let _: () = PhantomData::<Bool2>;*/
    // Church numerals
}