On Sat, Jan 24, 2009 at 10:32 AM,  <span dir="ltr">&lt;<a href="mailto:roconnor@theorem.ca">roconnor@theorem.ca</a>&gt;</span> wrote:<br><div class="gmail_quote"><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">On Fri, 23 Jan 2009, Luke Palmer wrote:<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
For example, it is possible to prove that foldr mappend mempty (x:xs) =<br>
foldr1 mappend (x:xs). &nbsp;Which means that anywhere in the source where we see<br>
the former, we can &quot;clean it up&quot; to the latter. &nbsp;However, if monad laws<br>
don&#39;t apply to partial values, then we first have to prove that none of the<br>
(x:xs) are _|_, perhaps even that no substrings are _|_. &nbsp;This is a much<br>
more involved transformation, so much so that you probably just wouldn&#39;t do<br>
it if you want to be correct.<br>
<br>
Bottoms are part of Haskell&#39;s semantics; theorems and laws have to apply to<br>
them to. &nbsp;You can pretend they don&#39;t exist, but then you have to be okay<br>
with never using an infinite data structure. &nbsp;I.e. if your programs would<br>
run just as well in Haskell as they would in a call-by-value language, then<br>
you don&#39;t have to worry about bottoms.<br>
</blockquote>
<br></div>
BTW, This last statement isn&#39;t true. &nbsp;The expression (let x = 1:x in x) won&#39;t work in CBV, but it is a well defined value without any bottoms.<br>
In fact, every subexpression in that value is a well defined value wihtout any bottoms.</blockquote><div><br>That&#39;s not what I said.&nbsp; My statement was a hypothetical: <i>if</i> it works call-by-value, then you don&#39;t have to worry about bottom.&nbsp; This program does not work in CBV, so my statement is true.<br>
<br>I&#39;m just being pedantic, of course.<br><br>The deeper reason that you have to worry about bottoms in this expression is that its denotation is a limit:&nbsp; { _|_, 1:_|_, 1:1:_|_, 1:1:1:_|_, ... }.&nbsp; Bottom has an essential role in describing infinity, not just programs which don&#39;t halt.<br>
<br>Luke<br><i></i></div></div>