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

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