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

oren revenge спросил: 12 мая 2018 в 04:18 в: haskell

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

: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))?

haskell functional-programming

2 ответа

Есть решение

chi ответил: 12 мая 2018 в 04:42

: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 есть только два лямбда.

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

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

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

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

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

Итак,

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

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

Круглые скобки здесь имеют значение, так как мы должны помнить, что t2 - это функция x. Без скобок мы получим функцию с тремя аргументами, как описано выше.

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

David Young Welperooni ответил: 12 мая 2018 в 08:01

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

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