Is eta-equivalence for functions compatiable with Haskell's seq operation? Lemma: Assuming eta-equivalence we have that (\x -&gt; ⊥) = ⊥ :: A -&gt; B.

Proof: ⊥ = (\x -&gt; ⊥ x) by eta-equivalence, and (\x -&gt; ⊥ x) = (\x -&gt; ⊥) by reduction under the lambda.

The Haskell 2010 report, section 6.2 specifies the seq function by two equations:


seq :: a -> b -> b
seq ⊥ b  =  ⊥
seq a b  =  b, if a ≠ ⊥


It then claims "As a consequence, ⊥ is not the same as \x -> ⊥, since seq can be used to distinguish them."

My question is, is that really a consequence of the definition of seq?

The implicit argument seems to be that seq would be uncomputable if seq (\x -&gt; ⊥) b = ⊥.  However I haven't been able to prove that such a seq would be uncomputable.  It seems to me such a seq is both monotone, and continuous, which puts it in the the realm of being computable.  

An algorithm that implement such as seq might work by attempting to search for for some x where f x ≠ ⊥ by enumerating the domain of f starting with ⊥. Though such an implementation, even if possible at all, gets pretty hairy once we want to make seq polymorphic.

Is there a proof that there is no computable seq that identifies (\x -&gt; ⊥) with ⊥ :: A -&gt; B?  Alternatively, is there some construction of seq that does identify (\x -&gt; ⊥) with ⊥ :: A -&gt; B?
First, let us be explicit about how seq distinguishes $\bot$ from $\lambda x . \bot$:

bottom :: a
bottom = bottom

eta :: a -&gt; b
eta x = bottom

-- This terminates
fortytwo = seq eta 42

-- This does not terminate
infinity = seq bottom 42


It is therefore an experimental fact that in Haskell $\bot$ and $\lambda x . \bot$ are operationally distinguishable. It is also a fact, and a quite obvious one, that seq is computable because Haskell computes it. So much about Haskell. You are asking about the very particular phrasing of the Haskell documentation. I read it as saying that seq is supposed to satisfy the two given equations, but those two equations are not sufficient for the definition of seq. Here is why: I can give you two models of (simply typed) $\lambda$-calculus in which seq is computable and satisfies the given equations, but in one of the models $\bot$ and $\lambda x . \bot$ agree, while in the other they do not.

In a simple domain-theoretic model where $\lambda$-expressions are interpreted in the domain of continuous functions $[D \to E]$ we have $\bot = \lambda x . \bot$, obviously. Take effective Scott domains or some such to make everything computable. It is easy to define seq in such a model.

We can also have a model of $\lambda$-calculus in which seq distinguishes $\bot$ and $\lambda x . \bot$, and then of course $\eta$-rule cannot hold. For instance, we can do this by interpreting functions in the domain $[D \to E]_\bot$, i.e., the function space domain with an extra bottom attached. Now $\bot$ is, well, the bottom of $[D \to E]_\bot$, while $\lambda x . \bot$ is the element just above it. They cannot be distinguished by application because they both evaluate to $\bot$, no matter what you apply them to (they are extensionally equal). But we do have seq as a map between domains and it alwyas distinguishes bottom from all other elements.