Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Implement the untyped lambda calculus in the Rust type system.
#![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());
}
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.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.