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 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₃
.
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).i
has type fn(X₂) -> X₂
, and the expected type was fn(Z) -> Y
, so by unification we have Z = 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
:
# 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.