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

[Lennart Augustsson]

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