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)?
Let's try to write the type equations Rust has to solve, to understand what went wrong. Each
ihas typefn(X) -> Xfor a givenX. Since they can be chosen independently for eachi, I'll name themX₁,X₂andX₃.ihas typefn(X₁) -> X₁, and the expected type wasfn(Z) -> fn(Y) -> X, so by unification we haveZ = X₁ = fn(Y) -> X(1).ihas typefn(X₂) -> X₂, and the expected type wasfn(Z) -> Y, so by unification we haveZ = X₂ = Y(2).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: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.