If you add a let binding: let x = slowFunction 1000 in f x \y -> let x = slowFunction 1000 in f x y I believe GHC may optimise both functions to only compute the `slowFunction 1000` once due to the full laziness/let floating optimisation. So then the eta-equivalence holds again. Maybe the full laziness optimisation should be disabled by default to make performance more predictable and to make it even more obvious that eta-equivalence doesn’t hold. See https://gitlab.haskell.org/ghc/ghc/-/issues/8457 Cheers, Jaro

On 28 Jun 2022, at 11:57, Richard Eisenberg wrote:

My best understanding is that eta-equivalence holds only in total languages, and even there without regard to performance. So you can hunt for eta-equivalence trouble anywhere that non-totality or performance comes into play.

For example, compare (A) `f (slowFunction 1000)` and (B) `\x -> f (slowFunction 1000) x`. If we map (A) over a list, then `slowFunction 1000` is computed once. If we map (B) over a list, then `slowFunction 1000` is computed for each element of the list.

Note that this example is very bare-bones: no extensions, no parametricity-busting `seq`, no compiler flags. All it relies on is a non-strict functional language.

I do think compiling this examples is a nice service -- thanks! Richard

...

On Jun 20, 2022, at 4:38 AM, Hécate wrote:

Hi Café!

I was wondering if anyone knew of a centralised list of occurrences where GHC Haskell stops upholding η-equivalence. I am interested in both type changes and operational semantics. So far I've collected the following things:

* Rank-2 types

* Monomorphism restriction

* The presence of seq

* Non-pedantic bottoms

One source is the GHC Manual¹, and Neil Mitchell pointed me to the list of bugs and limitations of HLint².

If you have other examples, or explanations of the mechanisms at play here, I would be very interested, and intend to upstream those in the GHC manual.

Cheers, Hécate

[¹] https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/bugs.html#ex...

[²] https://github.com/ndmitchell/hlint#bugs-and-limitations

-- Hécate ✨ 🐦: @TechnoEmpress IRC: Hecate WWW: https://glitchbra.in RUN: BSD

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

No, you're right. My comment about "lazy" was more relevant to a second example that I removed (because it sneakily relied on `seq` and is thus redundant with other mention of `seq`). Thanks for correcting. Richard

On Jun 29, 2022, at 3:02 AM, Tom Ellis wrote:

It seems to me the same difference would hold in a strict language too. Am I missing something? (A difference between strict and lazy here would be that in a lazy language `slowFunction 1000` would not be computed at all if the list is empty.)

Tom

On Tue, Jun 28, 2022 at 06:57:14PM +0000, Richard Eisenberg wrote:

...

My best understanding is that eta-equivalence holds only in total languages, and even there without regard to performance. So you can hunt for eta-equivalence trouble anywhere that non-totality or performance comes into play.

For example, compare (A) `f (slowFunction 1000)` and (B) `\x -> f (slowFunction 1000) x`. If we map (A) over a list, then `slowFunction 1000` is computed once. If we map (B) over a list, then `slowFunction 1000` is computed for each element of the list.

Note that this example is very bare-bones: no extensions, no parametricity-busting `seq`, no compiler flags. All it relies on is a non-strict functional language.

---

Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.