Why seq in Haskell has to have special rule for bottom?

Question

Haskell Report 2010 says that seq "weakens Haskell’s parametricity properties", as "⊥ is not the same as \x -> ⊥, since seq can be used to distinguish them" [1].

It seems that it happens exactly because of an explicit rule:

seq ⊥ b  =  ⊥

I was wondering why this special case was introduced? There must be a reason why

seq a b  =  b

would not be enough, and seq needs a more complicated definition with that special case:

seq ⊥ b  =  ⊥
seq a b  =  b, if a ≠ ⊥ 

[1] https://www.haskell.org/onlinereport/haskell2010/haskellch6.html#x13-1260006.2

---

[edit] It clarify the question, here is another angle on it. Why can not seq be defined like this:

seq :: a -> b -> b
seq a b  =  b

With a rule that seq is a special function that would evaluate its first argument "as much as possible". If evaluation results in HNF, then the argument is completely evaluated. If it would result in an exception or a bottom value, those are stored and would be thrown or returned whenever first argument would actually be used in evaluation of the second argument.

It is a bit lame, but I think that should make my questions a bit more clear. It is not about how seq works. It is about the intentions of the current design.

Maybe there are some obvious reasons, from the implementation standpoint. Or maybe it would have some consequences, like inability to provide some useful properties that are currently based on the seq been defined with that special case for bottom. Or maybe there are some other connections that I am not aware of. This is what I am quirious about :)

Answer 1

The whole point of seq x y is to evaluate x and then return y. Haskell is lazy, so a definition such as

seq x y = y

won't do, since x is left unevaluated. If we knew x :: Int we could write

seq x y = case x of
          0 -> y
          _ -> y

forcing x to be evaluated. We can play the same trick for lists, trees, etc. with a significant exception: functions. If x is a function, we can not case over it (trivial patterns aside, which do no force evaluation). Functions are only evaluated on call, so we might attempt

seq x y = case x 12 of -- let's pretend it's an Int->Int function
          0 -> y
          _ -> y

this will force the evaluation of x (good!), but will also evaluate x 12 (bad!).

It turns out that we know that writing seq in the lambda-calculus is actually impossible: theory formalizes the intuition around "we cannot force a function unless we apply, and if we apply we are also forcing the result".

So, in Haskell, seq was added as a primitive operation, not definable in terms of everything else. The implementation of seq is strict on its first argument, even if there's no need to evaluate it to return the second.

Since seq does something outside the lambda-calculus, it breaks a few things in the theory, such as parametricity, but this loss is not so large to ruin the whole language, which still enjoys many of the nice theoretical properties of the lambda calculus.

Historically, if my memory serves me right, early Haskell was about to include a class for seq:

 class Seq a where
    seq :: a -> b -> b

and this class was instantianted on every type but functions, so that parametricity was preserved as well. Later, it was decided that it was not practical to add all the Seq a constraints in the code, since a single use of seq would have required to add a large number of constraints around. So, seq was made into a primitive, at the cost of breaking the theory a bit.

Answer 2

An answer above contains a discussion that eventually allowed me to understand what was I missing. I think that the following is the gist of it.

Proposed definition would require solution to the halting problem, if we limit ourselves to one thread only. ⊥ means 3 different things: exceptions, errors and non-termination. First two could be dealt with, but the third on is impossible to solve in a general case.

It might be possible to provide an implementation that would use an additional thread to run evaluation of a. But it looks like a much more complicated solution, possibly, with its own pitfalls.