[Haskell-cafe] What's the motivation for η rules?
monnier at iro.umontreal.ca
Wed Dec 29 04:44:55 CET 2010
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.
λ 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.
More information about the Haskell-Cafe