<p>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.</p>

<p>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.</p>

CC BY-SA 4.0
2018-06-24T13:26:38.677Z
2018-06-24T13:26:38.677Z
Stefan
<p>@xuq01's guess is (extremely surprisingly!) wrong. The CBV eta rule described in the question is sound in Standard ML: the value <code>v</code> is contextually equivalent to <code>fn x =&gt; v x</code>. </p>

<p>There are two caveats to this.</p>

<ol>
<li><p>First, in specific <em>implementations</em> this equivalence might not be sound: in SML/NJ, you could use <code>Unsafe.cast</code> to detect physical equality of function values. However, unsafe features are not part of the standard. </p></li>
<li><p>Second, eta with functions and sums interacts in a slightly subtle way, due to clausal definitions and incomplete pattern matching. In particular, the definitions:</p>

<pre><code>fun f (SOME x) (SOME y) = x + y
</code></pre>

<p>and</p>

<pre><code>val g = fn (SOME x) =&gt; (fn (SOME y) =&gt; x + y)
</code></pre>

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

<pre><code>- f NONE;
val it = fn : int option -&gt; int

- g NONE;
uncaught exception Match [nonexhaustive match failure]
raised at: stdIn:2.32
</code></pre>

<p>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 <a href="https://dl.acm.org/citation.cfm?id=2429075" rel="noreferrer"><em>Copatterns: programming infinite structures by observations</em></a> for an example of a polarized calculus in this style. (See also Paul Levy's <a href="http://www.cs.bham.ac.uk/~pbl/papers/jumboicalp.pdf" rel="noreferrer"><em>Jumbo Lambda-Calculus</em></a>, for another calculus based on this observation.)   </p></li>
</ol>

CC BY-SA 4.0
2018-06-24T16:34:22.347Z
Why do you find that extremely surprising, given SML's puristic design?
Andreas Rossberg
CC BY-SA 4.0
2018-06-24T20:05:51.557Z
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. :)
Neel Krishnaswami
CC BY-SA 4.0
2018-06-25T13:31:26.260Z
Do you know of any proof of this or is this just based on extensive knowledge of the language standard?
Max New
CC BY-SA 4.0
2018-06-25T14:11:01.973Z
@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.
Neel Krishnaswami
CC BY-SA 4.0
2018-06-24T13:47:43.780Z
2018-06-24T13:47:43.780Z
Neel Krishnaswami
<p>$\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.</p>

<ol>
<li>Haskell includes <code>seq</code>, which can distinguish between <code>(\x -&gt; error "")</code> and <code>error ""</code></li>
<li>OCaml includes operations like "physical equality" (==), and which will distinguish <code>fun x =&gt; x</code> from <code>fun y =&gt; (fun x =&gt; x) y</code> because == corresponds to pointer equality.</li>
</ol>

<p>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.</p>

<p>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.</p>

<p>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?</p>

CC BY-SA 4.0
2018-06-23T18:16:24.253Z
My guess is no because of some wacky detail in the language, but I can't find an example...
xrq
<pl.programming-languages><type-theory><compilers>
Does Standard ML validate (CBV) eta equivalence?
Max New
# Does Standard ML validate (CBV) eta equivalence?

(Asked by: username_0 on 2018-06-23)

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

**Tags:** pl.programming-languages, type-theory, compilers

> **Comments:**
> **username_1**: My guess is no because of some wacky detail in the language, but I can't find an example...  

---

## 2 answers

### Answer by username_3 on 2018-06-24. Score: 7 | Accepted answer

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

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

> **Comments:**
> **username_4**: Why do you find that extremely surprising, given SML's puristic design?  
> **username_3**: 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. :)  
> **username_0**: Do you know of any proof of this or is this just based on extensive knowledge of the language standard?  
> **username_3**: @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.  

---

### Answer by username_2 on 2018-06-24. Score: 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.


---

