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

[Janis Voigtlaender]

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):

http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=651452

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
restrictions. See

http://haskell.org/haskellwiki/Correctness_of_short_cut_fusion

(also explaining that the nowadays maybe even more popular
destroy/unfoldr-dual of foldr/build does not even need seq to fail being
correct)

> 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.

Ciao, Janis.

-- 
Dr. Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt at tcs.inf.tu-dresden.de