Сигнатура типа комбинатора не соответствует сигнатуре типа эквивалентной ему лямбда-функции

Рассмотрите этот комбинатор:

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)
5
задан Jacob 6 March 2012 в 21:28
поделиться