Eta conversion corresponds to extensionality; i.e. there is nothing more to a function than what it does to its argument.
Suppose f x = g x for all x. Then using eta conversion: f = (\x. f x) = (\x. g x) = g Without eta this is not possible to prove. It would be possible for two functions to be distinct (well, not provably so) even if they do the same thing to every argument -- say if they had different performance characteristics. Eta is a "controversial" rule of lambda calculus -- sometimes it is omitted, for example, Coq does not use it. It tends to make things more difficult for the compiler -- I think Conor McBride is the local expert on that subject. On Tue, Dec 28, 2010 at 4:12 PM, David Sankel <cam...@gmail.com> wrote: > TIA, > David > > -- > David Sankel > Sankel Software > www.sankelsoftware.com > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe