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

[Stefan Holdermans]

David,

Conor wrote:

> But the news is not all bad. It is possible to add some eta-rules
> without breaking the Geuvers property (for functions it's ok; for
> pairs and unit it's ok if you make their patterns irrefutable).

Note that, in Haskell, for functions it's only ok if you leave seq and the like out of the equation: otherwise undefined and (\x. undefined x) can be told apart using seq.  (That's a minor detail, though.)

Cheers,

  Stefan