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

Stefan Monnier 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.

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




More information about the Haskell-Cafe mailing list