Adding seq ruins eta reduction. For normal order lambda calculus we have '\x.f x = f' (x not free in f). If we add seq this is no longer true.
isn't that a problem of seq (and evaluation in Haskell generally) not being strict enough (ie, forcing evaluation only to weak head normal form rather than to head normal form)? for instance: seq (\x->_|_ x) () = () =/= _|_ = seq _|_ () but (assuming a variant, seq-hnf, forcing to hnf instead): seq-hnf (\x-> _|_ x ) () = _|_ = seq-hnf _|_ () I don't have my "phone book" here, but didn't Barendregt have a discussion of what kind of normal form would be an appropriate choice for the meaning of lambda terms, with hnf being "good" and whnf or nf being "bad"? reduction to whnf is a pragmatic choice, with a long history, and its own calculus, which is not quite the ordinary lambda calculus. but it's been ages since I learned these things, so I might be misremembering. Claus
I'm a fan of eta, it makes reasoning easier. It also means the compiler can do more transformations.
I also like eta conversion, as well as its variations for non-function types. what they have in common is that the expanded form provides syntactic/structural evidence for properties that are only semantically present in the reduced form. for instance, if we add non-functions to the calculus, eta has to be constrained with type information for f - as the expanded form promises that we have a function, holding more information than the reduced form. variations of eta for non-function types, this allows us to make functions/ contexts less strict (the kind of "borrowing information from the future" so often needed in cyclic programming, or in dealing with other potentially infinite structures): lazy_id_pair x = (fst x,snd x) -- lazy_id_pair _|_ = (_|_,_|_) vs strict_id_pair (a,b) = (a,b) -- strict_id_pair _|_ = _|_ at the expense of not having laws like: x = (fst x,snd x) -- not true in general, even if we know that x::(a,b) x = x >>= return -- not true in general, even if x :: Monad m => m a x = \y-> x y -- not true in general, even if x :: a -> b we still have the inequalities, though - the expanded form being more defined than the reduced form. x :: t ]= (expand-at-t x) :: t -- eta conversion at type t so compilers could use eta-expansion, but not eta-reduction (not without an approximate analysis of an undecidable property). do you happen to have an example in mind where eta-reduction would be beneficial as a compiler transformation, but analysis (to demonstrate that the expanded functional expression terminates successfully) impractical?