What is Eta abstraction in lambda calculus used for?

Question

Eta Abstraction in lambda calculus means following.

A function f can be written as \x -> f x

• Is Eta abstraction of any use while reducing lambda expressions?
• Is it only an alternate way of writing certain expressions?

Practical use cases would be appreciated.

Answer 1

The eta reduction/expansion is just a consequence of the law that says that given

f = g

it must be, that for any x

f x = g x

and vice versa.

Hence given:

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

we get, by beta reducing the right hand side

f x = f x

which must be true. Thus we can conclude

f   = \y -> f y

Answer 2

First, to clarify the terminology, paraphrasing a quote from the Eta conversion article in the Haskell wiki (also incorporating Will Ness' comment above):

Converting from \x -> f x to f would constitute an eta reduction, and moving in the opposite way would be an eta abstraction or expansion. The term eta conversion can refer to the process in either direction.

• Extensive use of η-reduction can lead to Pointfree programming.
• It is also typically used in certain compile-time optimisations.

Summary of the use cases found:

1. Point-free (style of) programming
2. Allow lazy evaluation in languages using strict/eager evaluation strategies
3. Compile-time optimizations
4. Extensionality

1. Point-free (style of) programming

From the Tacit programming Wikipedia article:

Tacit programming, also called point-free style, is a programming paradigm in which function definitions do not identify the arguments (or "points") on which they operate. Instead the definitions merely compose other functions

Borrowing a Haskell example from sth's answer (which also shows composition that I chose to ignore here):

inc x = x + 1

can be rewritten as

inc = (+) 1

This is because (following yatima2975's reasoning) inc x = x + 1 is just syntactic sugar for \x -> (+) 1 x so

\x -> f       x   => f
\x -> ((+) 1) x   => (+) 1

(Check Ingo's answer for the full proof.)

There is a good thread on Stackoverflow on its usage. (See also this repl.it snippet.)

2. Allow lazy evaluation in languages using strict/eager evaluation strategies

Makes it possible to use lazy evaluation in eager/strict languages.

Paraphrasing from the MLton documentation on Eta Expansion:

Eta expansion delays the evaluation of f until the surrounding function/lambda is applied, and will re-evaluate f each time the function/lambda is applied.

Interesting Stackoverflow thread: Can every functional language be lazy?

2.1 Thunks

I could be wrong, but I think the notion of thunking or thunks belongs here. From the wikipedia article on thunks:

In computer programming, a thunk is a subroutine used to inject an additional calculation into another subroutine. Thunks are primarily used to delay a calculation until its result is needed, or to insert operations at the beginning or end of the other subroutine.

The 4.2 Variations on a Scheme — Lazy Evaluation of the Structure and Interpretation of Computer Programs (pdf) has a very detailed introduction to thunks (and even though the latter has not one occurrence of the phrase "lambda calculus", it is worth reading).

(This paper also seemed interesting but didn't have the time to look into it yet: Thunks and the λ-Calculus.)

3. Compile-time optimizations

Completely ignorant on this topic, therefore just presenting sources:

• From Georg P. Loczewski's The Lambda Calculus:

  In 'lazy' languages like Lambda Calculus, A++, SML, Haskell, Miranda etc., eta conversion, abstraction and reduction alike, are mainly used within compilers. (See [Jon87] page 22.)

  where [Jon87] expands to

  Simon L. Peyton Jones
  The Implementation of Functional Programming Languages
  Prentice Hall International, Hertfordshire,HP2 7EZ, 1987.
  ISBN 0 13 453325 9.

• search results for "eta" reduction abstraction expansion conversion "compiler" optimization

4. Extensionality

^{This is another topic that I know little about, and this is more theoretical, so here it goes:}

From the Lambda calculus wikipedia article:

η-reduction expresses the idea of extensionality, which in this context is that two functions are the same if and only if they give the same result for all arguments.

Some other sources:

• nLab entry on Eta-conversion that goes deeper into its connection with extensionality, and its relationship with beta-conversion

• ton of info in the What's the point of η-conversion in lambda calculus? on the Theoretical Computer Science Stackexchange (but beware: the author of the accepted answer seems to have a beef with the commonly held belief about the relationsship between eta reduction and extensionality, so make sure to read the entire page. Most of it was over my head so I have no opinions.)

• The question above has been cross-posted to Math Exchange as well

• Speaking of "over my head" stuff: here's Conor McBride's take; the only thing I understood were that eta conversions can be controversial in certain context, but reading his reply was that of trying to figure out an alien language (couldn't resist)

^{Saved this page recursively in Internet Archive so if any of the links are not live anymore then that snapshot may have saved those too.}