Как понять вложенные лямбда-функции в Haskell

Question

Я пытаюсь понять значение следующих 2 лямбда-выражений в Haskell:

f = \x -> x (\y -> x y)
g = \x -> (\y -> y) x

Я попытался преобразовать их, и я получил это:

f x y = x x y
g x y = y x

Этоправильный?Я предположил, что аргументы обеих функций должны быть x и y, поскольку они оба находятся в лямбда-выражении в описании функции.Я в основном понял это так: f (x) = xf (y) и f (y) = y x.А для g g (x) = g (y) x и g (y) = y.Но так как я новичок в Haskell, я не очень уверен в этих типах конверсии.Если не правильно, что будет правильным преобразованием?

Answer 1

Ни один из них не является правильным. Ваше решение использует функции

f x y = x x y
g x y = y x

что на самом деле означает

f = \x -> (\y -> x x y)
g = \x -> (\y -> y x)

и те отличаются от оригинальных выражений

f = \x -> x (\y -> x y)
g = \x -> (\y -> y) x

Выше два уравнения можно переписать как

f x = x (\y -> x y)
g x = (\y -> y) x

Но отсюда нет способа превратить оставшиеся лямбды в дополнительные аргументы для f или g. В лучшем случае мы можем упростить их, используя бета / eta-конверсию, и получить

f x = x x            -- eta  (\y -> x y) = x
g x = x              -- beta (\y -> y) x = x

(Также см. Комментарий Уилла Несса ниже, который указывает, что с помощью дополнительного расширения eta в f мы могли бы достичь определения ОП. Тем не менее, это случайно.)

Наконец, обратите внимание, что Haskell не примет f x = x x, поскольку это не может быть напечатано, если мы не используем типы ранга 2 и явно не предоставляем аннотацию типа, такую ​​как f :: (forall a. a) -> b. Исходный код f = \x -> x (\y -> x y) страдает той же проблемой. Это также было бы хорошо для нетипизированных языков, например нетипизированное лямбда-исчисление в теории языков программирования.

Answer 2

Команда :type в приглашении GHCi - ваш друг.Давайте сначала возьмем ваш второй пример

λ> :type let g = \x -> (\y -> y) x in g
let g = \x -> (\y -> y) x in g :: p -> p

Итак, g хорошо напечатан и представляет собой запутанный способ написания функции идентификации :: p -> p.В частности, g принимает некоторое значение x и применяет функцию идентификации (\y -> y) к x, что приводит к x.GHCi при присвоении типа использует новое имя типа p, чтобы избежать путаницы.Нет, ваш g x y = ... не эквивалентен.(Проверьте это с помощью :type.)

Вы можете сократить :type до :t.Тогда давайте возьмем ваш первый пример.

λ> :t let f = \x -> x (\y -> x y) in f
* Occurs check: cannot construct the infinite type: t2 ~ t2 -> t3
* In the first argument of `x', namely `(\ y -> x y)'
  In the expression: x (\ y -> x y)
  In the expression: \ x -> x (\ y -> x y)
* Relevant bindings include
    x :: t2 -> t3 (bound at <interactive>:1:10)
    f :: (t2 -> t3) -> t3 (bound at <interactive>:1:5)

Errk.Ваш предложенный f такой же, как этот?

λ> :t let f x y = x x y in f
* Occurs check: cannot construct the infinite type:
    t3 ~ t3 -> t4 -> t5
* In the first argument of `x', namely `x'

По крайней мере, похоже на подобное сообщение об ошибке.Что это за t2, t3, t4, t5?Опять же, GHCi использует свежие имена для типов, чтобы избежать путаницы.

Глядя на let f = ..., GHCi видит, что x применяется к чему-то, поэтому он дает x :: t2 -> t3, где t2 - типаргумента t3 - это тип возвращаемого значения.Это также видит f = \x -> x (blah).Таким образом, тип возвращаемого значения f должен быть тем, что возвращает x, то есть t3, а аргумент f равен x.Так что f :: (t2 -> t3) -> t3.

Внутри (blah) к чему-то применяется x.Таким образом, что-то (то есть y) должно быть типом аргумента x, а возвращаемый тип должен быть типом возврата x.Т.е. (\y -> x y) :: t2 -> t3.Errk: тогда у нас должен быть такой же тип аргумента x, потому что к нему применяется x.И то, как мы пишем «так же, как», происходит с ~.

Тогда сообщение об ошибке говорит вам, что GHCi пытается разобраться в t2 ~ (t2 -> t3).(-> связывает сильнее, чем ~.) И если вы попытаетесь заменить эту эквивалентность для t2 в RHS, вы получите t2 ~ (((... -> t3) -> t3)-> t3) до бесконечности.

Предлагаемый вами эквивалент для f x y =не эквивалентен (сообщение / набор текста немного отличается).Но они оба бесконечные типы, поэтому не допускаются.