Proving that λ x. Ω ≠ Ω in is one of the goals Abramsky sets for his lazy lambda calculus theory (page 2 of his paper, already cited by Uday Reddy), because they are both in weak head normal form. As of definition 2.7, he discusses explicitly that eta-reduction λ x. M x → M is not generally valid, but it is possible if M terminates in every environment. This does not mean that M must be a total function — only that evaluating M must terminate (by reducing to a lambda, for instance).
Your question seems to be motivated by practical concerns (performance). However, even though the Haskell Report might be less than completely clear, I doubt that equating λ x. ⊥ with ⊥ would produce a useful implementation of Haskell; whether it implements Haskell '98 or not is debatable, but given the remark, it's clear that the authors intended it to be the case.
Finally, how's seq to generate elements for an arbitrary input type? (I know QuickCheck defines the Arbitrary typeclass for that, but you're not allowed to add such constraints here). This violates parametricity.
Updated: I didn't manage to code this right (because I'm not so fluent in Haskel), and fixing this seems to require nested runST
regions.
I tried using a single reference cell (in the ST monad) to save such arbitrary elements, read them later, and make them universally available. Parametricity proves that break_parametricity
below cannot be defined (except by returning bottom, e.g. an error), while it could recover the elements your proposed seq would generate.
import Control.Monad.ST
import Data.STRef
import Data.Maybe
produce_maybe_a :: Maybe a
produce_maybe_a = runST $ do { cell <- newSTRef Nothing; (\x -> writeSTRef cell (Just x) >> return x) `seq` (readSTRef cell) }
break_parametricity :: a
break_parametricity = fromJust produce_maybe_a
I have to admit that I'm slightly fuzzy on formalizing the parametricity proof needed here, but this informal use of parametricity is standard in Haskell; but I learned from Derek Dreyer's writings that the needed theory is being quickly worked out in these last years.
EDITs:
- I am not even sure whether you need those extensions, which are studied for ML-like, imperative and untyped languages, or whether the classical theories of parametricity cover Haskell.
- Also, I mentioned Derek Dreyer simply because I only later came
across Uday Reddy's work — I learned about it only recently from "The essence of
Reynolds". (I only started really reading literature on parametricity in the last month or so).