On 3/7/11 6:38 PM, Alexander Solla wrote:
'seq' is not a "function", since it breaks referential transparency and possibly extensionality in function composition. By construction, "seq a b = b", and yet "seq undefined b /= b". Admittedly, the Haskell report and the GHC implementation, diverge on this issue. Haskell98 specifically defines seq in terms of a comparison with bottom, whereas GHC "merely" reduces the first argument to WHNF. In any case, the reduction is a side effect, with which can lead to inconsistent semantics if 'seq' is included in "the language".
It is nice to know that we can work in a consistent language if we avoid certain constructs, such as 'seq', 'unsafePerformIO', and probably others. In addition to making the "core language" conceptually simpler, it means that we can be sure we aren't inadvertently destroying the correctness guarantees introduced by the Howard-Curry correspondence theorem.
You are free to reason in whichever language you so desire. But that does not mean the semantics of the language you desire are the same as the semantics of Haskell. Fact of the matter is that Haskell has 'seq' and bottom, even if you choose to call them non-functions or non-values.
It is not the case that for every pair, ab, we have that:
ab == (fst ab, snd ab)
Why? Well consider ab = undefined:
_|_ /= (_|_,_|_)
(undefined, undefined) (*** Exception: Prelude.undefined
That is as close to Haskell-equality as you can get for a proto-value that does not have an Eq instance. As a consequence of referential transparency, evaluation induces an equivalence relation. This implies that (_|_, _|_) = _|_ = (_|_, _|_).
I value referential transparency, and so reject constructs which violate it.
Please demonstrate a proof that _|_ /= (_|_, _|_), so that I can exclude the unsound constructs you will undoubtedly have to use from my interpretation of "the language". I am more interested in finding the consistent fragment of what you call Haskell than defending what I call Haskell.
The trivial proof is: seq _|_ () == _|_ /= seq (_|_,_|_) () == () But you refuse to believe that 'seq' exists, so here's another proof: case _|_ of (_,_) -> () == _|_ /= case (_|_,_|_) of (_,_) -> () == () Do you refuse to believe that case analysis exists too? -- Live well, ~wren