Я только что нашел следующее выражение лямбда-исчисления:
(((λ f . (λ x . (f x))) (λ a . a)) (λ b . b))
Итак, это функция, которая принимает аргумент f и возвращает другую функцию, которая принимает аргумент x и возвращает результат применения x к f. Результатом приведенного выше выражения будет (λ b . b).
Это напоминает мне частичное применение и каррирование, однако применение функции "наизнанку" (f x) вызвало у меня интерес.
Есть ли в этом выражении более глубокий теоретический смысл?
Это выражение на самом деле очень крутое, хотя это довольно простая операция. В конце концов, функция — это просто приложение функции, верно?
Вот где все становится интересным. В лямбда-исчислении применение — это синтаксическое правило, которое просто гласит: «Если f — это выражение, а x — это выражение, то f x — это выражение». Приложение не является какой-либо функцией. Это прискорбно: поскольку лямбда-исчисление полностью основано на функциях, было бы отстойно полагаться на что-то, что не является функцией!
Ваш пример - своего рода средство от этого. Хотя мы не можем избавиться от приложения, мы можем, по крайней мере, определить аналог приложения. Этот аналог — лямбда-функция (λ f . (λ x . (f x))) (или, говоря идиоматически, λfx.f x). Это является функцией, поэтому мы можем рассуждать о ней и использовать ее точно так же, как и любую другую функцию. Мы можем передать его в качестве аргумента другим функциям или использовать как результат функции. Внезапно применение функции стало намного удобнее.
Это все, что у меня есть, что касается лямбда-исчисления, но эта функция и другие, подобные ей, также весьма полезны в реальной жизни. В языке функционального программирования F# у этой функции даже есть имя «оператор обратного конвейера», и мы пишем, что он имеет инфиксный оператор <|. Таким образом, в качестве альтернативы написанию f (x), где x — какое-то выражение, мы можем написать f <| x. Это хорошо, поскольку часто может освободить нас от написания множества надоедливых скобок. Ключевым моментом, который я пытаюсь здесь подчеркнуть, является то, что, хотя на первый взгляд ваш пример кажется академическим или, возможно, просто не очень полезным, он на самом деле нашел свое применение в нескольких основных языках программирования.
$ и <| делают одно и то же, и я почти уверен, что они определяются точно так же (хотя и не уверен на 100%). Кажется, я помню, что $ и <| имеют разный приоритет операций, но я недостаточно знаком с Haskell, чтобы сказать наверняка.
- person Ken Wayne VanderLinde; 02.02.2012
