Рассмотрите этот комбинатор:
S (S K)
Примените его к аргументам XY :
S (S K) X Y
Он сокращается до:
X Y
Я преобразовал S (SK) в соответствующие термины Lambda и получил следующий результат:
(\x y -> x y)
Я использовал инструмент Haskell WinGHCi, чтобы получить сигнатуру типа (\xy -> xy) и он ответил:
(t1 -> t) -> t1 -> t
Это имеет смысл для меня.
Затем я использовал WinGHCi, чтобы получить сигнатуру типа s (s k), и он вернул:
((t -> t1) -> t) -> (t -> t1) -> t
Это не имеет для меня смысла. Почему сигнатуры типов разные?
Примечание: я определил s, k и i как:
s = (\f g x -> f x (g x))
k = (\a x -> a)
i = (\f -> f)