[Haskell-cafe] Where does η-equivalence stop?

J. Reinders jaro.reinders at gmail.com
Tue Jun 28 19:16:33 UTC 2022


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 <lists at richarde.dev> 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 <hecate at glitchbra.in> 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#expressions-and-patterns
>> 
>> [²] 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.



More information about the Haskell-Cafe mailing list