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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
