[Haskell-cafe] Expressing seq

[Janis Voigtlaender]

Chad Scherrer wrote:
>> >
>> > There must be a subtlety I'm missing, right?
>>
>> What if the types are not instances of Eq?
>>
>> Jason
>>
> 
> Thanks, I figured it was something simple. Now I just to convince
> myself there's no way around that. Is there a proof around somewhere?

Yes, there is a proof that

   seq :: a -> b -> b

with the semantics as described in the Haskell report cannot be defined
in "Haskell minus seq". It goes as follows:

If seq were so definable, then it would have to fulfill the free theorem
derived from its type in "Haskell minus seq" (read: System F plus fix).
But it doesn't. See Section 5 of

   http://wwwtcs.inf.tu-dresden.de/~voigt/seqFinal.pdf

Ciao, Janis.

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