[Haskell-cafe] What's the motivation for η rules?

[Luke Palmer]

Eta conversion corresponds to extensionality; i.e. there is nothing
more to a function than what it does to its argument.

Suppose f x = g x for all x.  Then using eta conversion:

f = (\x. f x) = (\x. g x) = g

Without eta this is not possible to prove.  It would be possible for
two functions to be distinct (well, not provably so) even if they do
the same thing to every argument -- say if they had different
performance characteristics.  Eta is a "controversial" rule of lambda
calculus -- sometimes it is omitted, for example, Coq does not use it.
 It tends to make things more difficult for the compiler -- I think
Conor McBride is the local expert on that subject.


On Tue, Dec 28, 2010 at 4:12 PM, David Sankel <camior at gmail.com> wrote:
> TIA,
> David
>
> --
> David Sankel
> Sankel Software
> www.sankelsoftware.com
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>