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

[Janis Voigtlaender]

Janis Voigtlaender wrote:
> Lennart Augustsson wrote:
>> 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.

Maybe by "pure lambda calculus" you meant the untyped one. Then my
comparative argument does not work anymore, because fixpoints are
definable in the untyped setting, whereas seq isn't. Still, it remains
questionable whether this provides an argument for removing seq but
retaining fixpoints in Haskell. Why is the untyped setting the point of
reference?

In any case, the argument via losing parametricity does not hold. It is
not necessary to sacrifice seq to get parametricity back. Not any more
than it was necessary to sacrifice seq to get parametricity back.

Ciao,
Janis.

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