Lennart Augustsson wrote:
I don't think disallowing seq for functions makes them any more second class than not allow == for functions. I'm willing to sacrifice seq on functions to get parametricity back.
The underlying assumption that having seq makes us lose parametricity is a (widely spread) misconception, I think. Compare to the situation with fix (or, equivalently, general recursive definitions). The original notion of parametricity was developed for a calculus without fixpoints. If one allows fixpoints, then the original notion suddenly does not work anymore (see the last section of Wadler's original paper). So one might say: fixpoints break parametricity, so they are evil and should not be there. Of course, this is not what was done. Rather, the notion of parametricity was revised by changing the definition of the underlying logical relation to be more restrictive in the choice of relations to quantify over. Now, seq enters the picture. It turns out that even the revised notion of parametricity does not work for it. So one could come to the conclusion: seq breaks parametricity, so it is evil and should not be there. But this is a prejudice, because one can alternatively proceed just as for fixpoints, namely revise the notion of parametricity so that it works for both fixpoints and seq. There are more details on how to do this (and the consequences of doing so) than you probably want to see in the following papers: http://wwwtcs.inf.tu-dresden.de/~voigt/p76-voigtlaender.pdf http://wwwtcs.inf.tu-dresden.de/~voigt/seqFinal.pdf http://wwwtcs.inf.tu-dresden.de/~voigt/TUD-FI06-02.pdf Whether one likes the resulting notion of parametricity or not, one thing becomes clear: it is not any more justified to say that introducing seq "destroys" parametricity than to say that already introducing fix "destroyed" parametricity. In both cases, it was "just" necessary to adapt the concept of parametricity. Doing so then allows the same kind of reasoning and results as before, but for richer calculi.
There is a good reason seq cannot be defined for functions in the pure lambda calculus... It doesn't belong there. :)
How about the same argument for general recursion? As in: There is a good reason (typability) that fixpoint combinators cannot be defined in the pure lambda calculus... They don't belong there. Would anyone conclude from this that we should throw general recursive definitions out of Haskell? I doubt so. Note that nothing of the above implies that I think fully polymorphic seq is nice and cosy and should be in Haskell forever (even though it provided lot of nice research food for me so far ;-). My only point is that it is unfair to cite seq's supposed destruction of parametricity (as in "all or nothing") as an argument in weighing this decision. Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de