CODEWITHSUNDEEP
recursionrustlambda-calculus
Doubtful
Doubtful

Reputation: 83

Why Rust fails when I try to implement recursion with "S I I" from SKI-calculus?

Note: I took definitions of S and I from here: https://en.wikipedia.org/wiki/SKI_combinator_calculus#Informal_description

So S xyz = xz(yz), or in Rust:

fn s <Z, Y, X> (
    x: fn(Z) -> fn(Y) -> X,
    y: fn(Z) -> Y,
    z: Z
) -> X
where Z: Copy
{
    x(z)(y(z))
}

Let's also define an auxiliary I x = x:

fn i <X> (x: X) -> X { x }

I know that S I I x is x(x)(the problem I'm actually trying to solve is finding a type of x such that x is applicable to itself.), but let's not be that generic rn and try to use S I I I instead.

Obviously, S I I I = I(I)(I(I)) = I(I) = I

let _ = s(i, i, i); // = i(i)(i(i)) = i(i) = i

That is legit in my eyes, but not in compiler's:

error[E0308]: mismatched types
  --> src/main.rs:45:18
   |
45 |     let _ = s(i, i, i);
   |             -    ^ cyclic type of infinite size
   |             |
   |             arguments to this function are incorrect
   |
note: function defined here
  --> src/main.rs:32:4
   |
32 | fn s <Z, Y, X> (
   |    ^
33 |     x: fn(Z) -> fn(Y) -> X,
34 |     y: fn(Z) -> Y,
   |     -------------

I've found an "explanation" that this error occurs because there's some incalculable type that rustc cannot cope with. Makes sense, but I don't see here any exemplar of said type. May you point to me where it happens(and how to work around it, if possible)?

Upvotes: 1

Views: 91

Answers (1)

jthulhu
jthulhu

Reputation: 8688

Let's try to write the type equations Rust has to solve, to understand what went wrong. Each i has type fn(X) -> X for a given X. Since they can be chosen independently for each i, I'll name them X₁, X₂ and X₃.

  1. The first i has type fn(X₁) -> X₁, and the expected type was fn(Z) -> fn(Y) -> X, so by unification we have Z = X₁ = fn(Y) -> X (1).
  2. The second i has type fn(X₂) -> X₂, and the expected type was fn(Z) -> Y, so by unification we have Z = X₂ = Y (2).
  3. The third type equation is X₃ = Z (3).

By combining (1) and (2), we have Y = fn(Y) -> X. This type equation is cyclic: you will never find a finite type (in Rust's type system, at least) that will satisfy that.

Just as an aside, OCaml can typecheck that, if you explicitely turn on recursive types with -rectypes:

# let s x y z = x z (y z) in s Fun.id Fun.id Fun.id;;
- : 'a -> 'a as 'a = <fun>
#

If you are exploring lambda calculi, and friends, OCaml might be a better alternative.

As for Rust, I don't think there are any type-friendly way to do this.

Upvotes: 1

Related Questions