Eta Conversion, Extensionality, and When Two Functions Are the Same

Beta reduction decides when a function application can be simplified. It says nothing about when two functions that are not applied to anything are the same. In the pure calculus the gap is filled by a second rule, and the rule is deceptively small: λx. M x is the same function as M, provided x does not occur free in M. The right-hand side is a value of function type; the left-hand side is a function that immediately passes its argument along. No observable difference exists between them, so identifying them is the natural extension of the theory.

The rule is called eta conversion, and its consequences run further than its statement. It encodes the principle of extensionality, it changes which normal forms are canonical, it is unsound in the evaluation order that most languages use, and it reappears in compilers under the name “eta-expansion” doing a job that has nothing to do with equality.

The rule and its two directions

Eta appears in two forms. Eta-reduction contracts:

λx. M x  →η  M        (x not free in M)

Eta-expansion goes the other way, from M to λx. M x, and is used to make a term’s arity explicit. The conversion relation =η is the symmetric-transitive closure, and =βη combines both rules. Two terms are beta-eta equivalent when they are connected by a chain of beta and eta steps in either direction.

The side condition is essential, as with alpha. In λx. x x, the rightmost x is bound by the lambda, so the term is not of the form λx. M x with x free in M; contracting it would produce x, a free variable, which is a different term entirely. The condition x ∉ FV(M) is what makes the contraction a renaming-safe operation rather than a capture.

Three equations follow immediately, and they are the ones that show up in proofs:

• λx. f x =η f for any f, the defining case.
• λx. λy. f x y =η f, by two contractions, which is why curried functions can be written at any arity.
• λx. h ((λy. g y) x) =η λx. h (g x), a case where the contraction applies to a subterm rather than to the whole term, since the outer body is not of the form M x.

The third equation is a useful reminder that eta is not a global simplification. It rewrites wherever its side condition holds, including inside arguments and bodies, and it can increase as well as decrease the size of a term if applied in the expansion direction.

Extensionality, stated properly

The mathematical content of eta is function extensionality: two functions are equal if they agree on every argument. In set theory that is an axiom about functions as sets of pairs. In the lambda calculus it is a derived rule, and the derivation is short. Suppose M x =βη N x for a variable x not free in M or N. Then

M  =η  λx. M x  =βη  λx. N x  =η  N

so M =βη N. The eta steps are expansions at the two ends, the beta-eta step in the middle is the hypothesis, and the conclusion is extensional equality. Conversely, if M =βη N, then applying both sides to an argument preserves the equality because beta-eta is a congruence.

This is the property that makes the calculus a theory of functions rather than a theory of algorithms. Two different algorithms computing the same function are not beta-eta equivalent in general, because their terms reduce through different sequences, but two functions that differ only in how they accept arguments are. Eta captures the part of function identity that is independent of implementation, and it stops exactly where the implementation becomes observable.

The typed reading is sharper. In the simply typed lambda calculus the correspondence with category theory is exact: terms are morphisms of the category built from the typing rules, beta is the computation rule that governs the currying-evaluation adjunction, and eta is its unit law. That is why eta is not optional in the categorical reading; dropping it produces a category where the currying and evaluation morphisms do not compose to the identity, and the correspondence breaks.

Why call-by-value rejects eta-reduction

Under call-by-name, eta-reduction is a valid optimisation: it removes a beta step and a closure, and it never changes whether a term terminates. Under call-by-value it does not, and the counterexample is one line.

Take M = Ω, the divergent term (λx. x x)(λx. x x), and consider λx. Ω x. Under call-by-value, λx. Ω x is a value: it is a lambda, and lambdas are values regardless of what their bodies do. Evaluating it terminates immediately, producing a closure. Eta-reducing it gives Ω, which under call-by-value diverges. So the reduction changes a terminating program into a non-terminating one, and the two terms are not observationally equivalent.

The diagnosis is that call-by-value distinguishes values from computations, and the eta axiom assumes the two are the same. λx. M x delays the evaluation of M until the function is applied; M evaluates it now. In a lazy setting those are the same moment, because M is not evaluated until needed either. In a strict setting they are different moments, and the difference is observable.

The same argument explains why eta-expansion is safe under call-by-value while eta-reduction is not. Expanding M to λx. M x delays M behind a binder, which can only make a program terminate more often, never less. So a compiler may eta-expand freely; it may eta-reduce only when it knows the term is already a value, or when the language is lazy.

There is a subtler form of the same issue when M is not a value. If M is itself an application, λx. M x is still a value — the lambda is formed without evaluating the body — whereas M must be evaluated to a value before it can be used at all. Under call-by-value with effects, that difference is observable in the order in which effects happen. Implementations that track whether an expression is already a value can apply eta-reduction in exactly the case where it is sound.

Eta and normal forms

Adding eta changes what counts as a normal form. Under beta alone, λx. f x is a normal form, since it contains no redex. Under beta-eta, it is not: the eta-reduction applies, and the normal form is f. So beta-eta normal forms are a strict subset of beta normal forms, and every beta-eta normal form is a beta normal form.

The difference matters for decision procedures. Beta-eta equivalence is decidable for the simply typed calculus, because every well-typed term has a beta-eta normal form and the normal form is unique up to alpha. The algorithm is: normalise both terms under both rules, then compare structurally. That is the standard equality test in type checkers for dependently typed languages, where definitional equality includes eta for functions and, in some systems, for records and unit.

For the untyped calculus, beta equivalence is undecidable, and adding eta does not change that. The undecidability comes from the halting problem, not from the equality rule, because eta identifies only terms that observation cannot tell apart. What eta does change is the set of normal forms, and therefore the procedure for finding one. Eta-reduction on a beta normal form always terminates, because each step removes a lambda and the term shrinks, so a beta-eta normal form exists whenever a beta normal form does. The normalisation procedure is therefore two passes: beta-normalise, then eta-reduce to a fixed point.

The combination of beta and eta is confluent, but the proof needs care: the two rules feed each other, since a beta step can create an eta redex, as when (λy. λx. y x) z reduces to λx. z x, so the parallel-reduction argument for beta alone does not transfer directly. Implementations sidestep this by normalising under beta first and applying eta as a separate pass on the result, which is correct because eta-reduction preserves beta normality and the two passes reach the same normal form as any interleaved order.

Hereditary eta and the expansion that does not terminate

Eta-expansion applied naively does not terminate. M expands to λx. M x, which contains M, which expands again, ad infinitum. So expansion is only meaningful when it is guarded: expand a function-typed term by a lambda, and stop at the base type, since a term of base type has no argument to accept.

The guarded version is called hereditary eta-expansion, and it is what a type-directed compiler pass actually does. For a term M of function type A → B, produce λx. M' where M' is the hereditary expansion of M x at B; for a term of base type, leave it alone. The recursion is on the type, not on the term, so it terminates as long as the type is finite, which it is in any non-recursive type system. With recursive types the expansion can loop, and implementations bound it.

This is the form that appears in compilers under names like “eta-expansion” or “arity raising”. Its purpose there is not to establish equality but to make calling conventions uniform: a function that takes two arguments curried and a function that takes them as a pair must be adapted to a common representation before a call site can be compiled. The transformation is the same term-level rewrite, used for a different reason, and the type-directed guard is the same.

The boundary between equality and observation

The honest summary is that eta is a choice about what counts as observable. If a program can only observe a function by applying it, then λx. M x and M are indistinguishable, and eta is the right equality. If a program can observe when a computation happens — by timing, by effect ordering, by catching divergence — then they are distinguishable, and eta is wrong.

Most languages fall on the second side, which is why eta-reduction is not a valid general optimisation in a strict language even though it is valid in a lazy one. The distinction is not about the lambda calculus; it is about the observation the language’s semantics is built to respect. The pure calculus has no effects and no timing, so it can afford the extensional equality. A language with both has to give it up, and the price is that two functions that agree on every input may fail to be equal as programs.

That boundary is also where the eta rule meets the rest of the theory. Confluence of beta-eta holds, but the Church-Rosser argument has to be extended, because an eta step can sit inside a term that a beta step is about to rewrite, and the parallel-reduction proof does not apply unchanged. The typed version of the same question — whether definitional equality should include eta for every type former — is settled differently for sums and for functions, and the difference is one of the reasons the encodings of data as functions are canonical for some types and not others. The machinery that decides these equalities at scale is the normaliser inside a type checker, which is where the cost of eta becomes a runtime cost rather than a proof obligation.