$\eta$ equality of functions is fundamental in their Category-theoretic semantics but in practice even "functional" languages include "impure" features that violate it. Note that this is not an issue of CBN vs CBV, in CBN eta equality $M = \lambda x. M x$ should hold for any term $M : A \to B$ whereas in CBV this will be restricted to values $V = \lambda x. V x$. The CBV $\eta$ equality has a perfectly good category-theoretic explanation, see Levy's Call-by-push-value.
- Haskell includes
seq, which can distinguish between
(\x -> error "")and
- OCaml includes operations like "physical equality" (==), and which will distinguish
fun x => xfrom
fun y => (fun x => x) ybecause == corresponds to pointer equality.
So I wonder do any "real" languages satisfy eta for observational equivalence at all? All the better if it is known that a (correct) compiler implementation performs eta reductions just based on the type.
The only example I know of is Coq which includes it as a definitional equality as of a recent version. Maybe similar languages (Agda, Idris) do as well. These are not surprising because they include an equality type and it is very frustrating to prove equality of functions without $\eta$ or the stronger(?) extensionality principle.
My main question is about Standard ML specifically which I think does not have pointer equality for functions. Does it satisfy the CBV $\eta$ law? Furthermore do compilers for SML such as MLton use $\eta$ when optimizing programs?