seq does not preclude parametricity (Re: [Haskell-cafe] IO is not
voigt at tcs.inf.tu-dresden.de
Wed Jan 24 09:48:48 EST 2007
Lennart Augustsson wrote:
> 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.)
This idea has actually been investigated (as you might know):
That paper explains exactly how fix's impact on parametricity can be
tamed. I don't think it ever went into a practical system, though.
> 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).
Yup, see my self-correction earlier on the list.
> 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.
But not even completely so. Partial correctness is still given without
(also explaining that the nowadays maybe even more popular
destroy/unfoldr-dual of foldr/build does not even need seq to fail being
> The problem with the current seq can also be seen by the fact that
> it doesn't work properly with the IO type.
Yes, seq is from the dark side in many respects.
Dr. Janis Voigtlaender
mailto:voigt at tcs.inf.tu-dresden.de
More information about the Haskell-Cafe