This expression is really pretty cool, although it's a pretty simple operation. After all, a function is just an application function, right?
Where things get interesting. In terms of lambda, an application is a syntax rule that simply says: "If f
is an expression and x
is an expression, then fx
is an expression." The application is not a function. This is sad: since lambda calculus is all about functions, it would suck to rely heavily on what is not a function!
Your example is a means of doing this. Although we cannot get rid of the application, we can at least define an analogue of the application. This analogue is a lambda function (λ f . (λ x . (fx)))
(or more idiomatically, λfx.fx
). This is a function, so we can reason about it and use it just like any other function. We can pass it as arguments to other functions or use it as the result of a function. Suddenly, the application-application has become much more convenient.
That's all I have before calculating lambda, but this function and others like it are also very useful in real life. In the functional programming language F #, this function even has a name, the “feedback operator”, and we write that it has the infix operator <|
. Thus, as an alternative to writing f (x)
, where x
is some expression, we can write f <| x
f <| x
. This is good because it can often free us from writing a lot of annoying parentheses. The key point I'm trying to do here is that, although at first glance your example seems academic or perhaps just not very useful, it really found its way into several major programming languages.
source share