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

[Daniel Fischer]

On Tuesday 08 March 2011 00:38:53, Alexander Solla wrote:
> On Sat, Mar 5, 2011 at 5:06 AM, wren ng thornton <wren at freegeek.org> 
wrote:
> > 
> > If we have,
> > 
> >   data OneTuple a = One a
> > 
> > Then
> > 
> >    _|_ /= One _|_
> 
> That is vacuously true.  I will demonstrate the source of the
> contradiction
> 
> later.  But you also have "_|_ == One _|_", by evaluation:
> > Just undefined
> 
> Just *** Exception: Prelude.undefined
> 

But that shows that _|_ and Just _|_ aren't the same (in Haskell), doesn't 
it?

case x of
    Just _ -> "Just something"
    Nothing -> "Nothing"

produces "Just something" for (Just _|_), but not for _|_.

> > This can be detected by seq: the left-hand side doesn't terminate,
> > whereas the right-hand side does. And moreover, this can mess up
> > other things (e.g., monads) by introducing too much laziness. Space
> > leaks are quite a serious matter and they have nothing to do with
> > trying to compare uncomputable values. Do you want a seemingly
> > insignificant refactoring to cause your program to suddenly hang
> > forever? Or to take up gobs more space than it used to?
> 
> 'seq' is not a "function", since it breaks referential transparency

Does it, if one assumes that 'seq a b' is *not* the same as 'b' ?

> 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.

But reducing to WHNF is precisely what is needed to detect bottom.
If a value is a constructor application or a lambda, it's not bottom.

> In any case, the
> reduction is a side effect, with which can lead to inconsistent
> semantics if 'seq' is included in "the language".

But seq is "in the language", as specified by the report. You can argue 
that it shouldn't and campaign for its removal, but it's in now and 
speaking about Haskell, one can only sometimes ignore it.


> > 
> > 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 (_|_, _|_) = _|_ = (_|_, _|_).

But

case x of
  (_, _) -> "Okay"

distinguishes _|_ and (_|_, _|_). In Haskell98 and Haskell2010, they are 
not the same.

> 
> 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

Pattern matching

> 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.

That can be a source of much confusion. Usually, 'Haskell' is understood as 
the language defined in the report. There's some room for interpretation, 
but not too much. If you call soemthing too different 'Haskell', people 
won't understand you.