SK combinators (infinite trait recursion)

I am trying to implement SK combinators in the type system, but an expression that should terminate quickly is throwing the trait resolver into an infinite loop. Have I gotten something wrong, or should I submit this as a bug report?

struct S;
struct K;
type I = ((S,K),K);

trait Derive {
    type Result;
}

// No Arguments
impl Derive for S { type Result = Self; }
impl Derive for K { type Result = Self; }

// One Argument
impl<X:Derive> Derive for (S,X) { type Result = (S, X::Result); }
impl<X:Derive> Derive for (K,X) { type Result = (K, X::Result); }

// Two Arguments
impl<X,Y> Derive for ((S,X),Y) where
    X: Derive,
    Y: Derive
{ type Result = ((S,X::Result),Y::Result); }

impl<X,Y> Derive for ((K,X), Y) where X:Derive
{ type Result = X::Result; }

// Three Arguments
impl<X,Y,Z> Derive for (((S, X), Y), Z) where
    ((X, Z), (Y, Z)): Derive,
{ type Result = <((X, Z), (Y, Z)) as Derive>::Result; }

impl<X,Y,Z> Derive for (((K,X), Y), Z) where
    (X,Z): Derive
{ type Result = <(X, Z) as Derive>:: Result; }

// 4+ Arguments
impl<V,W,X,Y,Z,A> Derive for ((((V,W), X), Y), Z) where
    (((V,W), X), Y): Derive<Result = A>,
    (A,Z): Derive
{ type Result = <(A, Z) as Derive>::Result; }


fn main() {
    dbg!(std::any::type_name::<<S as Derive>::Result>());
    dbg!(std::any::type_name::<<(S,S) as Derive>::Result>());
    dbg!(std::any::type_name::<<((K,S),K) as Derive>::Result>());
    dbg!(std::any::type_name::<<(((K,S),K),S) as Derive>::Result>());
    dbg!(std::any::type_name::<<(I,S) as Derive>::Result>());
    dbg!(std::any::type_name::<<((K,K),K) as Derive>::Result>());
    dbg!(std::any::type_name::<<(((S, S), K), S) as Derive>::Result>());
    dbg!(std::any::type_name::<<(((S, S), S), S) as Derive>::Result>());

//  Uncommenting this line leads to infinite recursion
//    dbg!(std::any::type_name::<<(((((K,K),K),S),K),S) as Derive>::Result>());
}

(Playground)

1 Like

I'm not sure if this is a bug, but if you go with something less general, this compiles as expected. But I assume that's not a solution, because by "4+ arguments" you mean you want the evaluation of any combinator with 4 or more arguments?

1 Like

That's correct. I'm trying to show that the trait solver is Turing complete, and this seemed like the easiest approach.


Edit: I think I've got this working now, with a different approach:

struct True;
struct False;

struct S;
struct K;
type I = ((S,K),K);

trait DeriveStep {
    type Continue;
    type Result;
}

trait Or { type Result; }

impl Or for (False, False) { type Result = False; }
impl Or for (True, False) { type Result = True; }
impl Or for (False, True) { type Result = True; }
impl Or for (True, True) { type Result = True; }

impl<A,B,C,X,Y> Or for (A,B,C) where
    (A,B): Or<Result=X>,
    (X,C): Or<Result=Y>
{
    type Result = Y;
}

impl<A,B,C,D,X,Y,Z> Or for (A,B,C,D) where
    (A,B): Or<Result=X>,
    (C,D): Or<Result=Y>,
    (X,Y): Or<Result=Z>
{
    type Result = Z;
}

// No arguments
impl DeriveStep for S {
    type Continue = False;
    type Result = S;
}

impl DeriveStep for K { 
    type Continue = False; 
    type Result = K; 
} 
 
// One argument 
impl<X> DeriveStep for (S,X) 
    where X: DeriveStep 
{ 
    type Continue = X::Continue; 
    type Result = (S, X::Result); 
} 
 
impl<X> DeriveStep for (K,X) 
    where X:DeriveStep 
{ 
    type Continue = X::Continue; 
    type Result = (K, X::Result); 
} 
 
// Two arguments 
impl<X,Y> DeriveStep for ((K,X), Y) 
    where X:DeriveStep 
{ 
    type Continue = True; 
    type Result = X::Result; 
} 
 
impl<X,Y,Cont> DeriveStep for ((S,X), Y) where 
    X:DeriveStep, 
    Y:DeriveStep, 
    (X::Continue, Y::Continue): Or<Result=Cont> 
{ 
    type Continue = Cont; 
    type Result = ((S, X::Result), Y::Result); 
} 

// Three arguments
impl<X,Y,Z> DeriveStep for (((S, X), Y), Z) where
    X:DeriveStep,
    Y:DeriveStep,
    Z:DeriveStep
{
    type Continue = True;
    type Result = ((X::Result, Z::Result), (Y::Result, Z::Result));
}

impl<X,Y,Z> DeriveStep for (((K,X), Y), Z) where
    X:DeriveStep,
    Z:DeriveStep,
{
    type Continue = True;
    type Result = (X::Result, Z::Result);
}

// 4+ Arguments
impl<V,W,X,Y,Z,A,ACont,ZCont,Cont> DeriveStep for ((((V,W), X), Y), Z) where
    (((V,W), X), Y): DeriveStep<Result = A, Continue=ACont>,
    Z: DeriveStep<Continue = ZCont>,
    (ACont, ZCont): Or<Result = Cont>,
{
    type Continue = Cont;
    type Result = (A, Z::Result);
}

trait DeriveCont<Expr> { type Result; }
impl<Expr> DeriveCont<Expr> for False { type Result = Expr; }
impl<Expr> DeriveCont<Expr> for True where
    Expr: DeriveStep,
    Expr::Continue: DeriveCont<Expr::Result>
{
    type Result = <Expr::Continue as DeriveCont<Expr::Result>>::Result;
}

trait Derive { type Result; }

impl<Expr> Derive for Expr where True: DeriveCont<Expr> {
    type Result = <True as DeriveCont<Expr>>::Result;
}


fn main() {
    dbg!(std::any::type_name::<<S as Derive>::Result>());
    dbg!(std::any::type_name::<<(S,S) as Derive>::Result>());
    dbg!(std::any::type_name::<<((K,S),K) as Derive>::Result>());
    dbg!(std::any::type_name::<<(((K,S),K),S) as Derive>::Result>());
    dbg!(std::any::type_name::<<(I,S) as Derive>::Result>());
    dbg!(std::any::type_name::<<((K,K),K) as Derive>::Result>());
    dbg!(std::any::type_name::<<(((S, S), K), S) as Derive>::Result>());
    dbg!(std::any::type_name::<<(((S, S), S), S) as Derive>::Result>());
    dbg!(std::any::type_name::<<(((((K,K),K),S),K),S) as Derive>::Result>());
}

(Playground)

1 Like

Thinking about it more, I think the following should also work, if only it compiled: Playground. However, from this particular formulation, I feel it's clear to me why this recurses infinitely.

In the pair (X, Y), the type X can be any type that can be evaluated. But at that point, it might as well match that exact same kind of pair, say, (T, U) itself, since that's exactly what Derive is being implemented for. For this reason, perhaps introducing another level of indirection could help? Or maybe another impl that provides a base case? I'm not sure.

1 Like

Oh, very nice. The impl<Expr> Derive for Expr where True: DeriveCont<Expr> part looks exactly like the missing level of indirection.

After a few more spot checks, this seems to be correct: (((S, I), I), ((S, I), I)) recurses infinitely as expected, and randomly-generated expressions match an online implementation.

2 Likes