Is eta-equivalence for functions compatiable with Haskell's seq operation?

Question

Lemma: Assuming eta-equivalence we have that (\x -> ⊥) = ⊥ :: A -> B.

Proof: ⊥ = (\x -> ⊥ x) by eta-equivalence, and (\x -> ⊥ x) = (\x -> ⊥) 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 -> ⊥) 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 -> ⊥) with ⊥ :: A -> B? Alternatively, is there some construction of seq that does identify (\x -> ⊥) with ⊥ :: A -> B?

Answer 1

First, let us be explicit about how seq distinguishes $\bot$ from $\lambda x . \bot$:

bottom :: a
bottom = bottom

eta :: a -> 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.

Answer 2

Note that the specification for seq which you quote is not its definition. To quote the Haskell report "The function seq is defined by the equations: [and then the equations you give]".

The suggested argument seems to be that seq would be uncomputable if seq (\x -> ⊥) b = ⊥.

Such behaviour would violate the specification of seq.

Importantly, since seq is polymorphic, seq cannot be defined in terms of deconstructors (projections/pattern matching, etc.) on either of the two parameters.

Is there a proof that there is no computable seq that identifies (\x -> ⊥) with ⊥ :: A -> B?

If seq' (\x -> ⊥) b, one might think we could apply the first parameter (which is a function) to some value and then get ⊥ out. But, seq can never identify the first parameter with a function value (even if it happens to be one for some use of seq) because of its parametric polymorphic type. Parametricity means we know nothing about the parameters. Furthermore, seq can never take an expression and decide "is this ⊥?" (cf. the Halting problem), seq can only try to evaluate it, and itself diverge to ⊥.

What seq does is to evaluate the first parameter (not fully, but to "weak head normal form" [1], i.e. to the top-most constructor), then return the second parameter. If the first parameter happens to be ⊥ (i.e., a non terminating computation) then evaluating it causes seq to non-terminate, and thus seq ⊥ a = ⊥.

[1] Free Theorems in the Presence of seq - Johann, Voigtlander http://www.iai.uni-bonn.de/~jv/p76-voigtlaender.pdf

Answer 3

I am not sure if the Haskell report defines the semantics rigorously enough to settle the question about what $\lambda x.\, \bot$ should mean. However, it is common experience in Haskell as well as all other lazy functional languages, that, if you ask them to evaluate a term that represents $\lambda x.\, \bot$, the evaluation terminates. The "As a consequence..." remark in the Haskell report is assuming that the reader knows this.

Samson Abramsky considered this issue a long time ago and wrote a paper called "The Lazy Lambda Calculus". So, if you want formal definitions, this is where you might look.

Answer 4

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).