Well, I think fix destroys parametricity too, and it would be better to get rid of fix. But I'm not proposing to do that for Haskell, because I don't have a viable proposal to do so. (But I think the proposal would be along the same lines as the seq one; provide fix in a type class so we can keep tabs on it.) BTW, fix can be defined in the pure lambda calculus, just not in simply typed pure lambda calculus (when not qualified by "typed" the term "lambda calculus" usually refers to the untyped version). OK, so I was a bit harsh when I said seq destroys parametricity, it doesn't destroy it completely, just enough to ruin the properties used by, e.g., foldr/build. The problem with the current seq can also be seen by the fact that it doesn't work properly with the IO type. -- Lennart On Jan 24, 2007, at 04:11 , Janis Voigtlaender wrote:
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