Haskell привязки `let` в лямбда-исчислении

Пример times/square можно выразить в терминах лямбда-функций с использованием области видимости:

(\times -> (\square -> square 5)(\x -> times x x))(\x y -> x * y)

Но области видимости недостаточно для рекурсивных или взаимно рекурсивных привязок let, таких как

let ones = 1 : ones in take 5 ones

let even n = n == 0 || odd (abs n - 1)
    odd n  = n /= 0 && even (abs n - 1)
in even 7

В лямбда-исчислении вы можете определить y-комбинатор для рекурсии как

(\f -> (\x -> f (x x))(\x -> f (x x)))

Это позволяет вам определять функции и значения с точки зрения самих себя. Эта формулировка не является допустимой для haskell из-за ограничений ввода, но есть способы обойти это.

Использование y-комбинатора позволяет нам выразить вышеуказанные привязки let с помощью лямбда-исчисления:

(\ones -> take 5 ones)((\f -> (\x -> f (x x))(\x -> f (x x)))(\ones -> 1 : ones))

(\evenodd -> evenodd (\x y -> x) 7)((\f -> (\x -> f (x x))(\x -> f (x x)))(\evenodd c -> c (\n -> n == 0 || evenodd (\x y -> y) (abs n - 1)) (\n -> n /= 0 && evenodd (\x y -> x) (abs n - 1)))) 

Обратите внимание, что несколько привязок let можно свести к одной, определяющей пару (в общем случае кортеж). Например. мы можем переписать

let times x y = x * y
    square x = times x x
in square 5

as

let times = \x y -> x * y
    square = \x -> times x x
in square 5

тогда

let (times, square) = (\x y -> x * y, \x -> times x x)
in square 5

тогда, если захочется,

let pair = (\x y -> x * y, \x -> fst pair x x)
in snd pair 5

После этого мы можем применить обычный перевод лямбда-исчисления. Если определение пары оказывается рекурсивным, как в случае выше, нам нужен комбинатор с фиксированной точкой.

(\pair -> snd pair 5) (fix (\pair -> (\x y -> x * y, \x -> fst pair x x)))

Обратите внимание, что этот перевод не играет с алгоритмами вывода типов, которые обрабатывают let особым образом, вводя полиморфизм. Однако это не важно, если мы заботимся только о динамических аспектах нашей программы.

Я отвечу на свой вопрос, чтобы, возможно, предоставить полезную точку зрения тем, кто посещает этот вопрос.

Мы хотим реализовать следующую программу с двумя привязками let:

let times a b = a * b
    square x = times x x
in square 5

Для начала давайте упростим это до сути того, что мы хотим:

square 5

Достаточно просто. Однако square в данном случае не определено! Что ж, мы можем связать его, используя механизм, который предоставляет нам наш язык — лямбду. Это дает нам (\ square -> square 5) (\x -> times x x). Теперь square определено, а его двоюродный брат times нет... Что ж, нам нужна еще одна лямбда! Наша окончательная программа должна выглядеть так:

(\times -> (\square -> square 5) (\x -> times x x)) (\a b -> a * b)

Обратите внимание, что (\times -> ...) полностью закрывает наш последний шаг, так что times будет в области видимости, поскольку она привязана. Это согласуется с ответом, данным @rampion, и сокращается следующим образом:

(\times -> (\square  -> square 5) (\x -> times x x)) (\a b -> a * b) =>
(\square -> square 5) (\x -> (\a b -> a * b) x x)                    =>
(\square -> square 5) (\x -> (\b -> x * b) x)                        => 
(\square -> square 5) (\x -> x * x)                                  => 
(\x -> x * x) 5                                                      =>
5 * 5                                                                => 
25

Если бы функция square не зависела от times, мы могли бы легко написать (\times square -> ..... Зависимость означает, что мы должны вложить эти две среды, одну из которых содержит times, а другую — внутри той, которая может использовать его определение.

Спасибо за всю твою помощь! Я поражен простотой и мощью лямбда-исчисления.