Implement the untyped lambda calculus in the Rust type system.

untyped_lambda.rs

#![allow(unused)]
//#![feature(optin_builtin_traits)]

// Booleans
struct True;
struct False;
trait BoolOr<B> {type BoolOr;}
impl<B> BoolOr<B> for True {type BoolOr=True;}
impl BoolOr<True> for False {type BoolOr=True;}
impl BoolOr<False> for False {type BoolOr=False;}

// terms
// use trait `Var` for variables (defined below)
// use tuple (_,_) for applications
struct Lam<V:Var,E>(V,E);

// printing terms
trait MakeString {fn str()->String;}
impl<V:Var,E:MakeString> MakeString for Lam<V,E> {
  fn str()->String {format!("(λ{}.{})",V::str(),E::str())}
}
impl<E1:MakeString,E2:MakeString> MakeString for (E1,E2) {
  fn str()->String {format!("({})({})",E1::str(),E2::str())}
}

// Traits are used as type-level functions
// If a trait can be applied, the associated
// type holds the result of the function
// Branching is accomplished with supplemental traits

// check possible reduction
trait CanReduce {type CanReduce;}
impl<V:Var> CanReduce for V {type CanReduce=False;}
impl<V:Var,E> CanReduce for Lam<V,E> where
  E:CanReduce,
{type CanReduce=E::CanReduce;}
impl<E1,E2> CanReduce for (E1,E2) where
  E1:CanReduce,
  E2:CanReduce,
  E1::CanReduce:BoolOr<E2::CanReduce>,
  // Note: I'd love to do S@Self:Trait here so that
  // S is a shortcut to <Self as Trait>
  Self:AppCanReduce1<<E1::CanReduce as BoolOr<E2::CanReduce>>::BoolOr>,
{
  type CanReduce=<Self as AppCanReduce1<
    <E1::CanReduce as BoolOr<E2::CanReduce>>::BoolOr
  >>::AppCanReduce1;
}
trait AppCanReduce1<NoNeed> {type AppCanReduce1;}
impl<E1,E2> AppCanReduce1<True> for (E1,E2) {type AppCanReduce1=True;}
impl<V:Var,E> AppCanReduce1<False> for (V,E) {type AppCanReduce1=False;}
impl<V:Var,E1,E2> AppCanReduce1<False> for (Lam<V,E1>,E2) {type AppCanReduce1=True;}
impl<E1,E2,E3> AppCanReduce1<False> for ((E1,E2),E3) {type AppCanReduce1=False;}

// perform reduction
trait ReduceTo {type ReduceTo;}
impl<V:Var,E> ReduceTo for Lam<V,E> where
  E:ReduceTo,
{type ReduceTo=Lam<V,E::ReduceTo>;}
impl<E1,E2> ReduceTo for (E1,E2) where
  E1:CanReduce,
  E2:CanReduce,
  Self:AppReduceTo1<E1::CanReduce,E2::CanReduce>,
{type ReduceTo=<Self as AppReduceTo1<E1::CanReduce,E2::CanReduce>>::AppReduceTo1;}
trait AppReduceTo1<First,Second> {type AppReduceTo1;}
impl<B,E1,E2> AppReduceTo1<True,B> for (E1,E2) where
  E1:ReduceTo,
{type AppReduceTo1=(E1::ReduceTo,E2);}
impl<E1,E2> AppReduceTo1<False,True> for (E1,E2) where
  E2:ReduceTo,
{type AppReduceTo1=(E1,E2::ReduceTo);}
impl<V:Var,E1,E2> AppReduceTo1<False,False> for (Lam<V,E1>,E2) where
  E1:Subst<E2,V>,
{type AppReduceTo1=E1::Subst;}

// perform substitution
trait Subst<E,V:Var> {type Subst;}
impl<E,V1:Var,V2:Var> Subst<E,V1> for V2 where
  V1:SameVar<V2>,
  Self:VarSubst1<V1::SameVar,E>,
{type Subst=<Self as VarSubst1<V1::SameVar,E>>::VarSubst1;}
trait VarSubst1<B,E> {type VarSubst1;}
impl<V:Var,E> VarSubst1<True,E> for V {type VarSubst1=E;}
impl<V:Var,E> VarSubst1<False,E> for V {type VarSubst1=V;}
impl<E1,E2,V1:Var,V2:Var> Subst<E1,V1> for Lam<V2,E2> where
  V1:SameVar<V2>,
  Self:LamSubst1<V1::SameVar,E1,V1>,
{type Subst=<Self as LamSubst1<V1::SameVar,E1,V1>>::LamSubst1;}
trait LamSubst1<B,E,V:Var> {type LamSubst1;}
impl<V1:Var,V2:Var,E1,E2> LamSubst1<True,E1,V1> for Lam<V2,E2> {type LamSubst1=Lam<V2,E2>;}
impl<V1:Var,V2:Var,E1,E2> LamSubst1<False,E1,V1> for Lam<V2,E2> where
  E2:Subst<E1,V1>,
{type LamSubst1=Lam<V2,E2::Subst>;}
impl<V:Var,E1,E2,E3> Subst<E1,V> for (E2,E3) where
  E2:Subst<E1,V>,
  E3:Subst<E1,V>,
{type Subst=(E2::Subst,E3::Subst);}

// iterate reduction while possible
trait ReduceAll {type ReduceAll;}
impl<E> ReduceAll for E where
  E:ReduceTo,
  E::ReduceTo:CanReduce,
  E::ReduceTo:ReduceAll1<<E::ReduceTo as CanReduce>::CanReduce>,
{type ReduceAll=<E::ReduceTo as ReduceAll1<<E::ReduceTo as CanReduce>::CanReduce>>::ReduceAll1;}
trait ReduceAll1<B> {type ReduceAll1;}
impl<E> ReduceAll1<False> for E {type ReduceAll1=E;}
impl<E> ReduceAll1<True> for E where
  E:ReduceAll,
{type ReduceAll1=E::ReduceAll;} 

// define usable variable names
trait Var : MakeString {}
trait SameVar<V:Var> : Var {type SameVar;}

// Rust doesn't have type inequalities in order to maintain
// extensibility. We have to manually encode which variables
// are distinct from others.
//
// There are two ways to do that presented here. Either
// enumerate all combinations, which works well for a
// small, unextensible set, or use feature(optin_builtin_traits),
// which scales better but only works on nightly rust. I've
// commented out the nightly-only code below for better distribution.

// TODO: Learn macros
struct X;
impl Var for X {}
impl MakeString for X {fn str()->String{format!("x")}}
// trait NotX {}
// impl NotX for .. {}
// impl !NotX for X {}
// impl SameVar<X> for X {type SameVar=True;}
// impl<V:Var+NotX> SameVar<X> for V {type SameVar=False;}
struct Y;
impl Var for Y {}
impl MakeString for Y {fn str()->String{format!("y")}}
// trait NotY {}
// impl NotY for .. {}
// impl !NotY for Y {}
// impl SameVar<Y> for Y {type SameVar=True;}
// impl<V:Var+NotY> SameVar<Y> for V {type SameVar=False;}
struct F;
impl Var for F {}
impl MakeString for F {fn str()->String{format!("f")}}
// trait NotF {}
// impl NotF for .. {}
// impl !NotF for F {}
// impl SameVar<F> for F {type SameVar=True;}
// impl<V:Var+NotF> SameVar<F> for V {type SameVar=False;}
struct G;
impl Var for G {}
impl MakeString for G {fn str()->String{format!("g")}}
// trait NotG {}
// impl NotG for .. {}
// impl !NotG for G {}
// impl SameVar<G> for G {type SameVar=True;}
// impl<V:Var+NotG> SameVar<G> for V {type SameVar=False;}
struct N;
impl Var for N {}
impl MakeString for N {fn str()->String{format!("n")}}
// trait NotN {}
// impl NotN for .. {}
// impl !NotN for N {}
// impl SameVar<N> for N {type SameVar=True;}
// impl<V:Var+NotN> SameVar<N> for V {type SameVar=False;}
struct M;
impl Var for M {}
impl MakeString for M {fn str()->String{format!("m")}}
// trait NotM {}
// impl NotM for .. {}
// impl !NotM for M {}
// impl SameVar<M> for M {type SameVar=True;}
// impl<V:Var+NotM> SameVar<M> for V {type SameVar=False;}


// Without nightly features, we must enumerate (see comment above)
impl SameVar<X> for X {type SameVar=True;}
impl SameVar<X> for Y {type SameVar=False;}
impl SameVar<X> for F {type SameVar=False;}
impl SameVar<X> for G {type SameVar=False;}
impl SameVar<X> for N {type SameVar=False;}
impl SameVar<X> for M {type SameVar=False;}

impl SameVar<Y> for X {type SameVar=False;}
impl SameVar<Y> for Y {type SameVar=True;}
impl SameVar<Y> for F {type SameVar=False;}
impl SameVar<Y> for G {type SameVar=False;}
impl SameVar<Y> for N {type SameVar=False;}
impl SameVar<Y> for M {type SameVar=False;}

impl SameVar<F> for X {type SameVar=False;}
impl SameVar<F> for Y {type SameVar=False;}
impl SameVar<F> for F {type SameVar=True;}
impl SameVar<F> for G {type SameVar=False;}
impl SameVar<F> for N {type SameVar=False;}
impl SameVar<F> for M {type SameVar=False;}

impl SameVar<G> for X {type SameVar=False;}
impl SameVar<G> for Y {type SameVar=False;}
impl SameVar<G> for F {type SameVar=False;}
impl SameVar<G> for G {type SameVar=True;}
impl SameVar<G> for N {type SameVar=False;}
impl SameVar<G> for M {type SameVar=False;}

impl SameVar<N> for X {type SameVar=False;}
impl SameVar<N> for Y {type SameVar=False;}
impl SameVar<N> for F {type SameVar=False;}
impl SameVar<N> for G {type SameVar=False;}
impl SameVar<N> for N {type SameVar=True;}
impl SameVar<N> for M {type SameVar=False;}

impl SameVar<M> for X {type SameVar=False;}
impl SameVar<M> for Y {type SameVar=False;}
impl SameVar<M> for F {type SameVar=False;}
impl SameVar<M> for G {type SameVar=False;}
impl SameVar<M> for N {type SameVar=False;}
impl SameVar<M> for M {type SameVar=True;}

fn main() {
  // Lambda calculus syntax used here
  // Expressions
  // - anything below
  // Variables (limited, but expandable, set)
  // - X, Y, F, G, N, M
  // Lambdas (functions)
  // - Lam<var,expr>
  // Applications (reduce by substitution when the first is a lambda)
  // - (expr,expr)

  // church encoding
  type C0 = Lam<F,Lam<X,X>>;
  type C1 = Lam<F,Lam<X,(F,X)>>;
  type C2 = Lam<F,Lam<X,(F,(F,X))>>;
  type C3 = Lam<F,Lam<X,(F,(F,(F,X)))>>;
  type C4 = Lam<F,Lam<X,(F,(F,(F,(F,X))))>>;
  type CPlus = Lam<M,Lam<N,Lam<F,Lam<X,((M,F),((N,F),X))>>>>;
  type CMult = Lam<M,Lam<N,Lam<F,(M,(N,F))>>>;

  // starter lambda expression
  type L0 = ((CPlus,C2),C3);

  // // (λx.y x)((λy.y) n) - simple example
  // type L0 = (Lam<X,(Y,X)>,(Lam<Y,Y>,N));

  // // (λx.x x)(λx.x x) - reduces to itself, will not terminate
  // type L0 =
  // (Lam<X,(X,X)>,Lam<X,(X,X)>);

  type Full = <L0 as ReduceAll>::ReduceAll;
  println!("");
  println!("input: {:?}", L0::str());
  println!("reduce all: {:?}", Full::str());

  // these are evaluated only as needed
  type L1 = <L0 as ReduceTo>::ReduceTo;
  type L2 = <L1 as ReduceTo>::ReduceTo;
  type L3 = <L2 as ReduceTo>::ReduceTo;
  type L4 = <L3 as ReduceTo>::ReduceTo;
  type L5 = <L4 as ReduceTo>::ReduceTo;
  type L6 = <L5 as ReduceTo>::ReduceTo;
  type L7 = <L6 as ReduceTo>::ReduceTo;
  type L8 = <L7 as ReduceTo>::ReduceTo;
  type L9 = <L8 as ReduceTo>::ReduceTo;

  // print out reductions, too many will produce a compile error
  println!("");
  println!("input: {:?}", L0::str());
  println!("step 1:{:?}", L1::str());
  println!("step 2:{:?}", L2::str());
  println!("step 3:{:?}", L3::str());
  println!("step 4:{:?}", L4::str());
  println!("step 5:{:?}", L5::str());
  println!("step 6:{:?}", L6::str());
  // println!("step 7:{:?}", L7::str());
  // println!("step 8:{:?}", L8::str());
  // println!("step 9:{:?}", L9::str());

}