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:[EMAIL PROTECTED]
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
