[Haskell-cafe] Learn You a Haskell for Great Good - a few doubts

[wren ng thornton]

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