The value of "let x=(1:x); y=(1:y) in x==y" definitely _|_ )bottom) and nothing else.<br>A value of type Bool can be False, True, or _|_ and that expression does not yield a False or True.<br>It has nothing to do with time, it's just mathematics.
<br>What might be confusing you is that _|_ is often used as a name for non-termination, undefined, error etc.<br><br> -- Lennart<br><br><div class="gmail_quote">On Dec 27, 2007 7:20 PM, Achim Schneider <<a href="mailto:barsoap@web.de">
barsoap@web.de</a>> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><div class="Ih2E3d">Jonathan Cast <<a href="mailto:jonathanccast@fastmail.fm">
jonathanccast@fastmail.fm</a>> wrote:<br><br></div><div class="Ih2E3d">> On 27 Dec 2007, at 10:44 AM, Achim Schneider wrote:<br>><br>> > Wolfgang Jeltsch <<a href="mailto:g9ks157k@acme.softbase.org">g9ks157k@acme.softbase.org
</a>> wrote:<br>> ><br>> >> Am Donnerstag, 27. Dezember 2007 16:34 schrieb Cristian Baboi:<br>> >>> I'll have to trust you, because I cannot test it.<br>> >>><br>> >>> let x=(1:x); y=(1:y) in x==y .
<br>> >>><br>> >>> I also cannot test this:<br>> >>><br>> >>> let x=(1:x); y=1:1:y in x==y<br>> >><br>> >> In these examples, x and y denote the same value but the result of
<br>> >> x == y is _|_ (undefined) in both cases. So (==) is not really<br>> >> equality in Haskell but a kind of weak equality: If x doesn't equal<br>> >> y, x == y is False, but if x equals y, x == y might be True or
<br>> >> undefined.<br>> >><br>> > [1..] == [1..] certainly isn't undefined, it always evaluates to<br>> > True,<br>><br>> If something happens, it does eventually happen.<br>><br>
> More importantly, we can prove that [1..] == [1..] = _|_, since<br>><br>> [1..] == [1..]<br>> = LUB (n >= 1) [1..n] ++ _|_ == [1..n] ++ _|_<br>> = LUB (n >= 1) _|_<br>> = _|_<br>><br></div>
As far as I understand<br><a href="http://www.haskell.org/haskellwiki/Bottom" target="_blank">http://www.haskell.org/haskellwiki/Bottom</a><br>, only computations which cannot be successful are bottom, not those<br>that can be successful, but aren't. Kind of idealizing reality, that is.
<br><br>Confusion of computations vs. reductions and whether time exists or<br>not is included for free here. Actually, modulo mere words, I accept<br>both your and my argument as true, but prefer mine.<br><br>You _do_ accept that you won't ever see
Prelude.undefined in ghci<br>when evaluating<br><div class="Ih2E3d">let x=(1:x); y=(1:y) in x==y<br></div>, and there won't ever be a False in the chain of &&'s, don't you?<br><br>The question arises, which value is left from the possible values of
<br>Bool when you take away False and _|_?<br><br>And now don't you dare to say that _|_ /= undefined.<br><div><div></div><div class="Wj3C7c"><br>_______________________________________________<br>Haskell-Cafe mailing list
<br><a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br><a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br></div>
</div></blockquote></div><br>