[Haskell-cafe] Re: Wikipedia on first-class object

[Lennart Augustsson]

The value of "let x=(1:x); y=(1:y) in x==y" definitely _|_ )bottom) and
nothing else.
A value of type Bool can be False, True, or _|_ and that expression does not
yield a False or True.
It has nothing to do with time, it's just mathematics.
What might be confusing you is that _|_ is often used as a name for
non-termination, undefined, error etc.

  -- Lennart

On Dec 27, 2007 7:20 PM, Achim Schneider <barsoap at web.de> wrote:

> Jonathan Cast <jonathanccast at fastmail.fm> wrote:
>
> > On 27 Dec 2007, at 10:44 AM, Achim Schneider wrote:
> >
> > > Wolfgang Jeltsch <g9ks157k at acme.softbase.org> wrote:
> > >
> > >> Am Donnerstag, 27. Dezember 2007 16:34 schrieb Cristian Baboi:
> > >>> I'll have to trust you, because I cannot test it.
> > >>>
> > >>> let x=(1:x); y=(1:y) in x==y .
> > >>>
> > >>> I also cannot test this:
> > >>>
> > >>> let x=(1:x); y=1:1:y in x==y
> > >>
> > >> In these examples, x and y denote the same value but the result of
> > >> x == y is _|_ (undefined) in both cases.  So (==) is not really
> > >> equality in Haskell but a kind of weak equality: If x doesn't equal
> > >> y, x == y is False, but if x equals y, x == y might be True or
> > >> undefined.
> > >>
> > > [1..] == [1..] certainly isn't undefined, it always evaluates to
> > > True,
> >
> > If something happens, it does eventually happen.
> >
> > More importantly, we can prove that [1..] == [1..] = _|_, since
> >
> >    [1..] == [1..]
> > = LUB (n >= 1) [1..n] ++ _|_ == [1..n] ++ _|_
> > = LUB (n >= 1) _|_
> > = _|_
> >
> As far as I understand
> http://www.haskell.org/haskellwiki/Bottom
> , only computations which cannot be successful are bottom, not those
> that can be successful, but aren't. Kind of idealizing reality, that is.
>
> Confusion of computations vs. reductions and whether time exists or
> not is included for free here. Actually, modulo mere words, I accept
> both your and my argument as true, but prefer mine.
>
> You _do_ accept that you won't ever see Prelude.undefined in ghci
> when evaluating
> let x=(1:x); y=(1:y) in x==y
> , and there won't ever be a False in the chain of &&'s, don't you?
>
> The question arises, which value is left from the possible values of
> Bool when you take away False and _|_?
>
> And now don't you dare to say that _|_ /= undefined.
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20071228/f8c10790/attachment.htm