Путать с вложенными лямбда-типами в haskell

Question

Просто пытаюсь увидеть типы некоторых лямбда-выражений, подобных этому:

:t \x -> (\y -> x y)
\x -> (\y -> x y) :: (t1 -> t2) -> t1 -> t2

не должен ли тип здесь быть t1->(t2->t1->t2)?

Аналогично

:t \x -> (\y -> (\k -> y (x k)))
\x -> (\y -> (\k -> y (x k)))
  :: (t1 -> t2) -> (t2 -> t3) -> t1 -> t3

Разве тип не должен быть t1->(t2->(t3->t2))?

Answer 1

:t \x -> (\y -> x y)
\x -> (\y -> x y) :: (t1 -> t2) -> t1 -> t2

не должен ли тип здесь быть t1 -> (t2-> t1-> t2)?

Нет, t1->(t2->t1->t2) совпадает с t1->t2->t1->t2это тип функции с тремя аргументами (типа t1, t2 и t1), возвращающей t2.Однако есть только две лямбды, для двух аргументов x и y.

Вместо этого используется правильный тип

typeOfX -> (typeofY -> typeOfResult)
\x ->      (\y ->      x y)

(Кстати, ни одна из скобок вышенеобходимы.)

Что такое typeOfResult?Is является типом x y, поэтому это тип возвращаемого значения для x, который должен быть функцией.

Для проверки кода необходимо, чтобы typeOfX был типом функции, скажем a -> b.В таком случае мы можем видеть, что typeOfResult = b.Далее, в x y мы передаем y в x, и это может проверять тип, только если typeOfY = a.

Итак,

typeOfX  -> typeofY -> typeOfResult
=
(a -> b) -> a       -> b

Компилятор использовал имена t1 и t2, но это тот же тип.

Скобки здесь имеют значение, так как мы должны помнить, что x является функцией a -> b.Без скобок мы получили бы функцию с тремя аргументами, как объяснено выше.

Вы можете попытаться применить те же рассуждения ко второму примеру.Начните с typeOfX -> typeofY -> typeOfK -> TypeOfResult и постепенно узнайте, что это за типы на самом деле.

Answer 2

Тип x в \x -> \y -> x y равен t1 -> t2, и это первый аргумент.Как самая внешняя лямбда, она применяется сначала, а затем y

Вы могли бы написать ее как \x y -> x y, которая является просто приложением функции в естественном порядке.