seq does not preclude parametricity (Re: [Haskell-cafe] IO is not a monad)

[Janis Voigtlaender]

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 at tcs.inf.tu-dresden.de