Why is seq bad?
Haskell has a magical function named seq , which takes an argument of any type and reduces it to Weak Head Normal Form (WHNF).
I've read a couple of sources [not that I can remember who they were now...] which claim that "polymorphic seq is bad". In what way are they "bad"?
Similarly, there is the rnf function, which reduces an argument to Normal Form (NF). But this is a class method; it does not work for arbitrary types. It seems "obvious" to me that one could alter the language spec to provide this as a built-in primitive, similar to seq . This, presumably, would be "even more bad" than just having seq . In what way is this so?
Finally, somebody suggested that giving seq , rnf , par and similars the same type as the id function, rather than the const function as it is now, would be an improvement. How so?
As far as I know a polymorphic seq function is bad because it weakens free theorems or, in other words, some equalities that are valid without seq are no longer valid with seq . For example, the equality
map g (f xs) = f (map g xs)
holds for all functions g :: tau -> tau' , all lists xs :: [tau] and all polymorphic functions f :: [a] -> [a] . Basically, this equality states that f can only reorder the elements of its argument list or drop or duplicate elements but cannot invent new elements.
To be honest, it can invent elements as it could "insert" a non-terminating computation/run-time error into the lists, as the type of an error is polymorphic. That is, this equality already breaks in a programming language like Haskell without seq . The following function definitions provide a counter example to the equation. Basically, on the left hand side g "hides" the error.
g _ = True
f _ = [undefined]
In order to fix the equation, g has to be strict, that is, it has to map an error to an error. In this case, the equality holds again.
If you add a polymorphic seq operator, the equation breaks again, for example, the following instantiation is a counter example.
g True = True
f (x:y:_) = [seq x y]
If we consider the list xs = [False, True] , we have
map g (f [False, True]) = map g [True] = [True]
but, on the other hand
f (map g [False, True]) = f [undefined, True] = [undefined]
That is, you can use seq to make the element of a certain position of the list depend on the definedness of another element in the list. The equality holds again if g is total. If you are intereseted in free theorems check out the free theorem generator, which allows you to specify whether you are considering a language with errors or even a language with seq . Although, this might seem to be of less practical relevance, seq breaks some transformations that are used to improve the performence of functional programs, for example, foldr / build fusion fails in the presence of seq . If you are intereseted in more details about free theorems in the presence of seq , take a look into Free Theorems in the Presence of seq.
As far as I know it had been known that a polymorphic seq breaks certain transformations, when it was added to the language. However, the althernatives have disadvantages as well. If you add a type class based seq , you might have to add lots of type class constraints to your program, if you add a seq somewhere deep down. Furthermore, it had not been a choice to omit seq as it had already been known that there are space leaks that can be fixed using seq .
Finally, I might miss something, but I don't see how a seq operator of type a -> a would work. The clue of seq is that it evaluates an expression to head normal form, if another expression is evaluated to head normal form. If seq has type a -> a there is no way of making the evaluation of one expression depend on the evaluation of another expression.
Another counterexample is given in this answer - monads fail to satisfy monad laws with seq and undefined . And since undefined cannot be avoided in a Turing-complete language, the one to blame is seq .
上一篇: Haskell中的评估和空间泄漏
下一篇: 为什么seq不好？