Consider this combinator:
S (S K)
Apply it to the arguments X Y:
S (S K) X Y
It contracts to:
X Y
I converted S (S K) to the corresponding Lambda terms and got this result:
(\x y -> x y)
I used the Haskell WinGHCi tool to get the type signature of (\x y -> x y) and it returned:
(t1 -> t) -> t1 -> t
That makes sense to me.
Next, I used WinGHCi to get the type signature of s (s k) and it returned:
((t -> t1) -> t) -> (t -> t1) -> t
That doesn't make sense to me. Why are the type signatures different?
Note: I defined s, k, and i as:
s = (\f g x -> f x (g x))
k = (\a x -> a)
i = (\f -> f)
Thanks to all who responded to my question. I have studied your responses. To be sure that I understand what I've learned I have written my own answer to my question. If my answer is not correct, please let me know.
We start with the types of k and s:
k :: t1 -> t2 -> t1
k = (\a x -> a)
s :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5
s = (\f g x -> f x (g x))
Let's first work on determing the type signature of (s k).
Recall s's definition:
s = (\f g x -> f x (g x))
Substituting k for f results in (\f g x -> f x (g x)) contracting to:
(\g x -> k x (g x))
Important The type of g and x must be consistent with k's type signature.
Recall that k has this type signature:
k :: t1 -> t2 -> t1
So, for this function definition k x (g x) we can infer:
The type of x is the type of k's first argument, which is the type t1.
The type of k's second argument is t2, so the result of (g x) must be t2.
g has x as its argument which we've already determined has type t1. So the type signature of (g x) is (t1 -> t2).
The type of k's result is t1, so the result of (s k) is t1.
So, the type signature of (\g x -> k x (g x)) is this:
(t1 -> t2) -> t1 -> t1
Next, k is defined to always return its first argument. So this:
k x (g x)
contracts to this:
x
And this:
(\g x -> k x (g x))
contracts to this:
(\g x -> x)
Okay, now we have figured out (s k):
s k :: (t1 -> t2) -> t1 -> t1
s k = (\g x -> x)
Now let's determine the type signature of s (s k).
We proceed in the same manner.
Recall s's definition:
s = (\f g x -> f x (g x))
Substituting (s k) for f results in (\f g x -> f x (g x)) contracting to:
(\g x -> (s k) x (g x))
Important The type of g and x must be consistent with (s k)'s type signature.
Recall that (s k) has this type signature:
s k :: (t1 -> t2) -> t1 -> t1
So, for this function definition (s k) x (g x) we can infer:
The type of x is the type of (s k)'s first argument, which is the type (t1 -> t2).
The type of (s k)'s second argument is t1, so the result of (g x) must be t1.
g has x as its argument, which we've already determined has type (t1 -> t2).
So the type signature of (g x) is ((t1 -> t2) -> t1).
The type of (s k)'s result is t1, so the result of s (s k) is t1.
So, the type signature of (\g x -> (s k) x (g x)) is this:
((t1 -> t2) -> t1) -> (t1 -> t2) -> t1
Earlier we determined that s k has this definition:
(\g x -> x)
That is, it is a function that takes two arguments and returns the second.
Therefore, this:
(s k) x (g x)
Contracts to this:
(g x)
And this:
(\g x -> (s k) x (g x))
contracts to this:
(\g x -> g x)
Okay, now we have figured out s (s k).
s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1
s (s k) = (\g x -> g x)
Lastly, compare the type signature of s (s k) with the type signature of this function:
p = (\g x -> g x)
The type of p is:
p :: (t1 -> t) -> t1 -> t
p and s (s k) have the same definition (\g x -> g x) so why do they have different type signatures?
The reason that s (s k) has a different type signature than p is that there are no constraints on p. We saw that the s in (s k) is constrained to be consistent with the type signature of k, and the first s in s (s k) is constrained to be consistent with the type signature of (s k). So, the type signature of s (s k) is constrained due to its argument. Even though p and s (s k) have the same definition the constraints on g and x differ.