Does Standard ML validate (CBV) eta equivalence?

Question

$\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.

1. Haskell includes seq, which can distinguish between (\x -> error "") and error ""
2. OCaml includes operations like "physical equality" (==), and which will distinguish fun x => x from fun y => (fun x => x) y because == 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?

Answer 1

@xuq01's guess is (extremely surprisingly!) wrong. The CBV eta rule described in the question is sound in Standard ML: the value v is contextually equivalent to fn x => v x.

There are two caveats to this.

1. First, in specific implementations this equivalence might not be sound: in SML/NJ, you could use Unsafe.cast to detect physical equality of function values. However, unsafe features are not part of the standard.

2. Second, eta with functions and sums interacts in a slightly subtle way, due to clausal definitions and incomplete pattern matching. In particular, the definitions:

   fun f (SOME x) (SOME y) = x + y
   

   and

   val g = fn (SOME x) => (fn (SOME y) => x + y)
   

   are not contextually equivalent. This is because the call f NONE will return a function, and g NONE will raise an error.

   - f NONE;
   val it = fn : int option -> int
   
   - g NONE;
   uncaught exception Match [nonexhaustive match failure]
   raised at: stdIn:2.32
   

   The reason this happens is operationally obvious, and of course a call-by-push-value/polarization setup makes this choice explicable. But if you really want to seriously understand clausal definitions, you are led to the idea that clausal definitions should be primary, and the usual term formers should be derived notions. See Abel, Pientka, Thibodeau and Setzer's Copatterns: programming infinite structures by observations for an example of a polarized calculus in this style. (See also Paul Levy's Jumbo Lambda-Calculus, for another calculus based on this observation.)

Answer 2

SML compilers do perform eta-reduction (at least SML/NJ does), but I expect most functional programming language compilers do, even those for which the eta-law does not always hold.

E.g. the pointer equality of OCaml doesn't have a strictly defined semantics, which means that the compiler is free to apply eta-reduction, even though it may change the program's behavior.