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

[Janis Voigtlaender]

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

Replace "seq" by "fix" in the last sentence ;-)

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