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

[Stefan Monnier]

One way to look at it is that β rules are the application of an
eliminator (e.g. function application) to its corresponding constructor
(the lambda expression), whereas η rules correspond to the application
of a constructor to its corresponding eliminator.

E.g.

   λ y . (x y)                =>  x
   if x then True else False  =>  x
   (π₁ x, π₂ x)               =>  x

IOW there's no need for a motivation: those rules just appear naturally.


        Stefan