<p>First, let us be explicit about how <code>seq</code> distinguishes $\bot$ from $\lambda x . \bot$:</p>

<pre><code>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
</code></pre>

<p>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 <code>seq</code> 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 <code>seq</code> is supposed to satisfy the two given equations, but those two equations are not sufficient for the definition of <code>seq</code>. Here is why: I can give you two models of (simply typed) $\lambda$-calculus in which <code>seq</code> 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.</p>

<p>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 <code>seq</code> in such a model.</p>

<p>We can also have a model of $\lambda$-calculus in which <code>seq</code> 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 <em>extensionally equal</em>). But we do have <code>seq</code> as a map between domains and it alwyas distinguishes bottom from all other elements.</p>

CC BY-SA 3.0
2013-10-01T22:50:35.803Z
It is an experimental fact that in GHC and/or Hugs ⊥ and λx.⊥.  Fortunately, Haskell isn't defined by an implementation.  My question is suggesting that Haskell is underspecified with regards to seq.
Russell O'Connor
CC BY-SA 3.0
2013-10-01T22:55:27.030Z
Can you give a reference to what you mean by "effective Scott domains"  Presumably that doesn't imply that the partial order is decidable.  Also, the STLC isn't polymorphic, but Haskell is.  Usually Haskell is interpreted in System F or one of its derivatives.  How does this affect your argument?
Russell O'Connor
CC BY-SA 3.0
2013-10-02T14:16:42.910Z
Section 1.1.4 of my Ph.D. dissertation http://andrej.com/thesis/thesis.pdf has a short definition of effective Scott domains, and this is actually the first Google hit that is freely available.
Andrej Bauer
CC BY-SA 3.0
2013-10-02T14:19:53.297Z
There are models of System F based on domain theory (the parametric PER model), but I do not know what happens to `seq` in them. I do not really believe that Haskell has well defined semantics, and certainly you can only interpret a fragment of it in System F.
Andrej Bauer
CC BY-SA 3.0
2013-10-02T14:21:47.020Z
So your question is: if we require that `seq` satisfy the stated equations *and* that it be parametrically polymorphic, is then `seq` uniquely determined? Is that the question?
Andrej Bauer
CC BY-SA 3.0
2013-10-02T14:33:07.783Z
Ok, I think I can modify my argument to show that `seq` is underspecified even if it is polymorphic. But what do I get if I write the proof for you?
Andrej Bauer
CC BY-SA 3.0
2013-10-02T17:08:02.600Z
If you write a proof for me you will get an implementation of Haskell 98 where the eta-rule holds allowing (foldr (\a b -> f a b) z xs) to be optimized to (foldr f z xs) causing an asymptotic performance increase from O(n^2) to O(n) (see http://ghc.haskell.org/trac/ghc/ticket/7436).  More compelling it will allow a NewTypeWrapper in (NewTypeWrapper . f) to be optimized away without forcing f to be eta-expanded and prevent some asymptotic performance penalties currently imposed by newTypes in GHC (in the use of foldr for example).
Russell O'Connor
CC BY-SA 3.0
2013-10-02T17:21:56.130Z
My question is, if we remove the (questionable) sentence "As a consequence, ⊥ is not the same as \x -> ⊥, since seq can be used to distinguish them." from the Haskell report, can we implement Haskell with a compiler that can safely eta-contract expressions and asymptotically increase performance of some Haskell programs.
Russell O'Connor
CC BY-SA 3.0
2013-10-02T23:46:28.323Z
I think so. From what I can see (inside my head) there is a polymorphic model in which $\eta$ holds and there is a polymorphic `seq` which satisfies the required equations. The point is that you can make a parametric model in which all bottoms in all types are actually the same element $\bot$ of the underlying universal domain.
Andrej Bauer
CC BY-SA 3.0
2013-10-03T00:13:17.370Z
Actually, you would have to make sure that your compiler *always* implements $\lambda x . \bot$ as $\bot$. That is, you might be tempted to not always contract and so in principle $\lambda x . \bot$ and $\bot$ would be "sometimes distinguishable", a very dangerous situation. To make sure this is not the case, you need to implement `seq` in a clever way which involves spawning infinitely many processes each applying your function to a basic element. If any of the processes terminates, then `seq` may proceed. It would be interesting to see if we can do this sequentially. Hmm.
Andrej Bauer
CC BY-SA 3.0
2013-10-01T06:47:41.530Z
2013-10-01T06:47:41.530Z
Andrej Bauer
<p>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.</p>

<p>Samson Abramsky considered this issue a long time ago and wrote a paper called "<a href="http://moscova.inria.fr/~levy/courses/X/M1/lambda/bib/90abramskylazy.pdf" rel="nofollow">The Lazy Lambda Calculus</a>".  So, if you want formal definitions, this is where you might look.</p>

CC BY-SA 3.0
2014-03-24T16:30:41.227Z
Apparently, these details are only defined by desugaring into the "Haskell kernel". Where is it defined is it?
The report says, [in Sec. 1.2](http://www.haskell.org/onlinereport/intro.html#sect1.2):
"Although the kernel is not formally specified, it is essentially a slightly sugared variant of the lambda calculus with a straightforward denotational semantics. The translation of each syntactic structure into the kernel is given as the syntax is introduced."
Blaisorblade
CC BY-SA 3.0
2014-03-24T16:52:18.430Z
The Haskell 2010 report says [the same](http://www.haskell.org/onlinereport/haskell2010/haskellch1.html#x6-110001.2), amazingly.
Blaisorblade
CC BY-SA 3.0
2014-03-24T17:55:43.573Z
Thanks for the reference to Abramsky! I skimmed it to see how it answers the question, and I came up with the following answer:
http://cstheory.stackexchange.com/a/21732/989
Blaisorblade
CC BY-SA 3.0
2014-02-24T01:12:09.587Z
2014-02-24T01:12:09.587Z
Uday Reddy
<p>Note that the specification for <code>seq</code> which you quote is <em>not</em> its definition.
 To quote the Haskell report "The function seq is <em>defined by the equations</em>: [and then the equations you give]".</p>

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

<p>Such behaviour would violate the specification of <code>seq</code>. </p>

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

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

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

<p>What <code>seq</code> 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 <code>⊥</code> (i.e., a non terminating computation) then evaluating it causes <code>seq</code> to non-terminate, and thus <code>seq ⊥ a = ⊥</code>.</p>

<p>[1] Free Theorems in the Presence of seq - Johann, Voigtlander <a href="http://www.iai.uni-bonn.de/~jv/p76-voigtlaender.pdf" rel="nofollow">http://www.iai.uni-bonn.de/~jv/p76-voigtlaender.pdf</a></p>

CC BY-SA 3.0
2013-09-27T22:03:40.750Z
The specification I give for seq is the definition of seq because that is exactly what the Haskell 2010 report says in Section 6.2.  Your operation definition of seq is not supported by the Haskell 2010 report: the words "head normal form" only occur once in the report in a totally different context.  It also is inconsistent with my understanding that GHC will often reduce the second argument to seq before the first argument, or the first argument won't be reduced at all because the strictness analyzer has proved it is non-bottom statically.
Russell O'Connor
CC BY-SA 3.0
2013-09-27T22:09:39.090Z
Parametricity doesn't directly say that we cannot apply any deconstructors, nor does it say we can never identify the first parameter with a function value.  All parametercity says for the polymorphic lambda calculus with fixpoints is that seq can absorb strict functions, or more generally certain strict relations hold for terms contain seq.  I admit it is plausible that parametricity might be used to prove (\x -> ⊥) &ne; ⊥, but I would like to see a rigorous proof.
Russell O'Connor
CC BY-SA 3.0
2013-09-28T12:31:47.817Z
In the case of a function `f : forall a . a -> T` (where `T` is some other type), then `f` cannot apply any deconstructors to its first argument since it does not know which deconstructors to apply. We cannot do a "case" on types. I have tried to improve the above answer (including citing information on `seq` evaluating to head normal form).
dorchard
CC BY-SA 3.0
2013-09-28T12:32:56.777Z
I can try to do the rigorous proof later if I find time (using relations in the style of Reynolds might be a good approach).
dorchard
CC BY-SA 3.0
2014-03-24T16:27:51.940Z
@RussellO'Connor: the description of seq is not "inconsistent" with those behaviors, it's just an operational specification (and behaviors are optimizations which do not change the final result).
Blaisorblade
CC BY-SA 3.0
2013-09-27T17:35:12.690Z
2013-09-29T01:39:54.717Z
2013-09-29T01:39:54.717Z
dorchard
<p>Proving that λ x. Ω ‌≠ Ω in is one of the goals Abramsky sets for his lazy lambda calculus theory (page 2 of <a href="http://moscova.inria.fr/~levy/courses/X/M1/lambda/bib/90abramskylazy.pdf" rel="nofollow">his paper</a>, 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).</p>

<p>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.</p>

<p>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.</p>

<p><strong>Updated</strong>: I didn't manage to code this right (because I'm not so fluent in Haskel), and fixing this seems to require nested <code>runST</code> 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 <code>break_parametricity</code> below cannot be defined (except by returning bottom, e.g. an error), while it could recover the elements your proposed seq would generate.</p>

<pre><code>import Control.Monad.ST
import Data.STRef
import Data.Maybe

produce_maybe_a :: Maybe a
produce_maybe_a = runST $ do { cell &lt;- newSTRef Nothing; (\x -&gt; writeSTRef cell (Just x) &gt;&gt; return x) `seq` (readSTRef cell) }

break_parametricity :: a
break_parametricity = fromJust produce_maybe_a
</code></pre>

<p>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.</p>

<p>EDITs:</p>

<ul>
<li>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.</li>
<li>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).</li>
</ul>

CC BY-SA 3.0
2014-04-06T05:36:50.393Z
Evaluating ``(\x -> writeSTRef cell (Just x) >> return x)`` on random inputs does not execute a write to the cell. Only the ST commands that make it into the sequenced passed into ``runST`` are ever executed. Similarly, running ``main = (putStrLn "Hello") `seq` (return ())`` does not print anything onto the display.
Russell O'Connor
CC BY-SA 3.0
2014-04-07T10:18:50.417Z
@RussellO'Connor, of course you're right — testing is hard since seq does not have the behavior we discuss.
But I still think generating elements breaks parametricity per se. I'll try fixing the answer to exemplify that.
Blaisorblade
CC BY-SA 3.0
2014-04-07T19:37:45.083Z
Hm, the obvious fix to the answer requires nesting runST regions and using the cell from the outer region in the inner one, but that's not allowed.
Blaisorblade
CC BY-SA 3.0
2014-03-24T17:29:29.523Z
2014-04-07T10:26:50.833Z
2014-04-07T10:26:50.833Z
Blaisorblade
<p>Lemma: Assuming eta-equivalence we have that <code>(\x -&gt; ⊥) = ⊥ :: A -&gt; B</code>.</p>

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

<p>The Haskell 2010 report, section 6.2 specifies the <code>seq</code> function by two equations:</p>

<pre>
seq :: a -> b -> b
seq ⊥ b  =  ⊥
seq a b  =  b, if a ≠ ⊥
</pre>

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

<p>My question is, is that really a consequence of the definition of <code>seq</code>?</p>

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

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

<p>Is there a proof that there is no computable <code>seq</code> that identifies <code>(\x -&gt; ⊥)</code> with <code>⊥ :: A -&gt; B</code>?  Alternatively, is there some construction of <code>seq</code> that does identify <code>(\x -&gt; ⊥)</code> with <code>⊥ :: A -&gt; B</code>?</p>

<domain-theory><haskell><extensionality>
Is eta-equivalence for functions compatiable with Haskell's seq operation?
Russell O'Connor
# Is eta-equivalence for functions compatiable with Haskell's seq operation?

(Asked by: username_0 on 2013-09-27)

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?

**Tags:** domain-theory, haskell, extensionality


---

## 4 answers

### Answer by username_1 on 2013-10-01. Score: 6

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.

> **Comments:**
> **username_0**: It is an experimental fact that in GHC and/or Hugs ⊥ and λx.⊥.  Fortunately, Haskell isn't defined by an implementation.  My question is suggesting that Haskell is underspecified with regards to seq.  
> **username_0**: Can you give a reference to what you mean by "effective Scott domains"  Presumably that doesn't imply that the partial order is decidable.  Also, the STLC isn't polymorphic, but Haskell is.  Usually Haskell is interpreted in System F or one of its derivatives.  How does this affect your argument?  
> **username_1**: Section 1.1.4 of my Ph.D. dissertation http://andrej.com/thesis/thesis.pdf has a short definition of effective Scott domains, and this is actually the first Google hit that is freely available.  
> **username_1**: There are models of System F based on domain theory (the parametric PER model), but I do not know what happens to `seq` in them. I do not really believe that Haskell has well defined semantics, and certainly you can only interpret a fragment of it in System F.  
> **username_1**: So your question is: if we require that `seq` satisfy the stated equations *and* that it be parametrically polymorphic, is then `seq` uniquely determined? Is that the question?  
> **username_1**: Ok, I think I can modify my argument to show that `seq` is underspecified even if it is polymorphic. But what do I get if I write the proof for you?  
> **username_0**: If you write a proof for me you will get an implementation of Haskell 98 where the eta-rule holds allowing (foldr (\a b -> f a b) z xs) to be optimized to (foldr f z xs) causing an asymptotic performance increase from O(n^2) to O(n) (see http://ghc.haskell.org/trac/ghc/ticket/7436).  More compelling it will allow a NewTypeWrapper in (NewTypeWrapper . f) to be optimized away without forcing f to be eta-expanded and prevent some asymptotic performance penalties currently imposed by newTypes in GHC (in the use of foldr for example).  
> **username_0**: My question is, if we remove the (questionable) sentence "As a consequence, ⊥ is not the same as \x -> ⊥, since seq can be used to distinguish them." from the Haskell report, can we implement Haskell with a compiler that can safely eta-contract expressions and asymptotically increase performance of some Haskell programs.  
> **username_1**: I think so. From what I can see (inside my head) there is a polymorphic model in which $\eta$ holds and there is a polymorphic `seq` which satisfies the required equations. The point is that you can make a parametric model in which all bottoms in all types are actually the same element $\bot$ of the underlying universal domain.  
> **username_1**: Actually, you would have to make sure that your compiler *always* implements $\lambda x . \bot$ as $\bot$. That is, you might be tempted to not always contract and so in principle $\lambda x . \bot$ and $\bot$ would be "sometimes distinguishable", a very dangerous situation. To make sure this is not the case, you need to implement `seq` in a clever way which involves spawning infinitely many processes each applying your function to a basic element. If any of the processes terminates, then `seq` may proceed. It would be interesting to see if we can do this sequentially. Hmm.  

---

### Answer by username_2 on 2014-02-24. Score: 2

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](http://moscova.inria.fr/~levy/courses/X/M1/lambda/bib/90abramskylazy.pdf)". So, if you want formal definitions, this is where you might look.

> **Comments:**
> **username_3**: Apparently, these details are only defined by desugaring into the "Haskell kernel". Where is it defined is it? The report says, [in Sec. 1.2](http://www.haskell.org/onlinereport/intro.html#sect1.2): "Although the kernel is not formally specified, it is essentially a slightly sugared variant of the lambda calculus with a straightforward denotational semantics. The translation of each syntactic structure into the kernel is given as the syntax is introduced."  
> **username_3**: The Haskell 2010 report says [the same](http://www.haskell.org/onlinereport/haskell2010/haskellch1.html#x6-110001.2), amazingly.  
> **username_3**: Thanks for the reference to Abramsky! I skimmed it to see how it answers the question, and I came up with the following answer: http://cstheory.stackexchange.com/a/21732/989  

---

### Answer by username_4 on 2013-09-27. Score: 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>

> **Comments:**
> **username_0**: The specification I give for seq is the definition of seq because that is exactly what the Haskell 2010 report says in Section 6.2.  Your operation definition of seq is not supported by the Haskell 2010 report: the words "head normal form" only occur once in the report in a totally different context.  It also is inconsistent with my understanding that GHC will often reduce the second argument to seq before the first argument, or the first argument won't be reduced at all because the strictness analyzer has proved it is non-bottom statically.  
> **username_0**: Parametricity doesn't directly say that we cannot apply any deconstructors, nor does it say we can never identify the first parameter with a function value.  All parametercity says for the polymorphic lambda calculus with fixpoints is that seq can absorb strict functions, or more generally certain strict relations hold for terms contain seq.  I admit it is plausible that parametricity might be used to prove (\x -> ⊥) &ne; ⊥, but I would like to see a rigorous proof.  
> **username_4**: In the case of a function `f : forall a . a -> T` (where `T` is some other type), then `f` cannot apply any deconstructors to its first argument since it does not know which deconstructors to apply. We cannot do a "case" on types. I have tried to improve the above answer (including citing information on `seq` evaluating to head normal form).  
> **username_4**: I can try to do the rigorous proof later if I find time (using relations in the style of Reynolds might be a good approach).  
> **username_3**: @RussellO'Connor: the description of seq is not "inconsistent" with those behaviors, it's just an operational specification (and behaviors are optimizations which do not change the final result).  

---

### Answer by username_3 on 2014-03-24. Score: 2

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 username_2), 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 username_2'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).

> **Comments:**
> **username_0**: Evaluating ``(\x -> writeSTRef cell (Just x) >> return x)`` on random inputs does not execute a write to the cell. Only the ST commands that make it into the sequenced passed into ``runST`` are ever executed. Similarly, running ``main = (putStrLn "Hello") `seq` (return ())`` does not print anything onto the display.  
> **username_3**: @RussellO'Connor, of course you're right — testing is hard since seq does not have the behavior we discuss. But I still think generating elements breaks parametricity per se. I'll try fixing the answer to exemplify that.  
> **username_3**: Hm, the obvious fix to the answer requires nesting runST regions and using the cell from the outer region in the inner one, but that's not allowed.  

---

