5
$\begingroup$

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

$\endgroup$
  • $\begingroup$ My guess is no because of some wacky detail in the language, but I can't find an example... $\endgroup$ – xrq Jun 23 '18 at 18:16
6
$\begingroup$

@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.)

$\endgroup$
  • 1
    $\begingroup$ Why do you find that extremely surprising, given SML's puristic design? $\endgroup$ – Andreas Rossberg Jun 24 '18 at 16:34
  • 2
    $\begingroup$ Given a randomly chosen cbv programming language, that equation holding is not the way to bet! Of course, SML was engineered well, but that's precisely what is surprising. :) $\endgroup$ – Neel Krishnaswami Jun 24 '18 at 20:05
  • $\begingroup$ Do you know of any proof of this or is this just based on extensive knowledge of the language standard? $\endgroup$ – Max New Jun 25 '18 at 13:31
  • $\begingroup$ @MaxNew The latter. Standard ML has an operational semantics and mechanized type-safety proof (of the Harper-Stone semantics), but as far as I know, no one has proven the soundness of a nontrivial equational theory for SML proper. $\endgroup$ – Neel Krishnaswami Jun 25 '18 at 14:11
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.