Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Implement the untyped lambda calculus in the Rust type system.
// 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
{type CanReduce=E::CanReduce;}
impl<E1,E2> CanReduce for (E1,E2) where
// 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
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
{type ReduceTo=Lam<V,E::ReduceTo>;}
impl<E1,E2> ReduceTo for (E1,E2) where
{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
{type AppReduceTo1=(E1::ReduceTo,E2);}
impl<E1,E2> AppReduceTo1<False,True> for (E1,E2) where
{type AppReduceTo1=(E1,E2::ReduceTo);}
impl<V:Var,E1,E2> AppReduceTo1<False,False> for (Lam<V,E1>,E2) where
{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
{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
{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
{type LamSubst1=Lam<V2,E2::Subst>;}
impl<V:Var,E1,E2,E3> Subst<E1,V> for (E2,E3) where
{type Subst=(E2::Subst,E3::Subst);}
// iterate reduction while possible
trait ReduceAll {type ReduceAll;}
impl<E> ReduceAll for E where
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
{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!("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!("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());
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment