<div dir="ltr">Programs interface with the real world if they are to be useful, and the real world contains bottoms (including literal ones, ultimately: black holes). Mathematics is our cognitive tool, not the real world, and can reject bottoms at least up to a point.</div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Dec 19, 2017 at 11:51 AM, Siddharth Bhat <span dir="ltr"><<a href="mailto:siddu.druid@gmail.com" target="_blank">siddu.druid@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">So, I have two opinions to share on this:<br>
Regarding the plane example, it is wrong to attempt to graph it on a plane, precisely because the domain is not the plane. </p>
<p dir="ltr">I am confused by your assertion that it is impossible to avoid divergence in mathematics: we do not define division as a *partial* function. Rather we define it as a *total* function on a *restricted domain*. </p>
<p dir="ltr">So, what one would need is the ability to create these restricted domains, which certain languages have as far as I am aware.</p>
<p dir="ltr">At that point, now that we track our domains and codomains correctly, all should work out?</p>
<p dir="ltr">I would still like an answer to interesting transformations that are enabled by having purity and laziness and are not encumbered by the presence of bottoms.</p>
<p dir="ltr">Cheers,<br>
Siddharth</p>
<br><div class="gmail_quote"><div><div class="h5"><div dir="ltr">On Tue 19 Dec, 2017, 20:36 Jonathan Paugh, <<a href="mailto:jpaugh@gmx.com" target="_blank">jpaugh@gmx.com</a>> wrote:<br></div></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><div>In the strictest sense, the math will bottom in exactly the same scenarios that Haskell will, but a human is unlikely to make that mistake because the result is nonsensical. If the set x you've provided is the domain for a given function g, then it doesn't make sense to reason about g(106): since 106 isn't in the domain, g(106) cannot exist in the codomain. Yet, if you're trying to graph the function on a plane, you have to deal it somehow, because 106 will exist on the plane.<br>
<br>
Getting to the original topic, it is impossible to avoid divergence in general, even in mathematics, which is in no way retrained by a compiler (although it may be limited by the operating environment ;). Languages (or maths) which eschew divergence are not very powerful.<br>
Consider that arithmetic diverges, because division is partial. But we humans often learn to deal with bottoms iimplicitly, by eliminating them from consideration in the first place. That might be analogous to refactoring the program to remove all offending cases, and recompiling.<br><br><div class="gmail_quote"></div></div><div><div class="gmail_quote">On December 19, 2017 8:35:57 AM CST, Baa <<a href="mailto:aquagnu@gmail.com" target="_blank">aquagnu@gmail.com</a>> wrote:</div></div><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><pre class="m_1882308129980466352m_-7535722637507639358k9mail">Pure functions can return "undefined" for some arguments values. So,<br>such function is partially-defined. Its domain has "gaps". This can be<br>coded in math, to avoid "undefined" (bottom), like<br><br> x = {-100..100, 105, 107..200}<br><br>It's impossible in Haskell, but IMHO its possible in F*, due to DepTypes<br>and RefTypes ;)<br><br>IMHO this is the reason to have bottom: possibility to return<br>"undefined" w/ simple correct type in signature (hidden bottom). If you<br>have a way to code arguments domains, no need to have bottom for pure<br>functions to "signal" gaps - gaps happen in run-time :) This is the one<br>of reasons for bottom to exist, as far as I understand. May be there are<br>other reasons :)<br><br>===<br>Best regards, Paul<br><br></pre></blockquote></div></div><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><pre class="m_1882308129980466352m_-7535722637507639358k9mail"><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #729fcf;padding-left:1ex"> Siddharth,<br> <br> how would you deal with functions that terminate for some <br> arguments/inputs but do not terminate for the others ?<br> <br> Alexey.<br> <br> On Tue, 2017-12-19 at 07:20 +0000, (IIIT) Siddharth Bhat wrote:<br><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #ad7fa8;padding-left:1ex"><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #8ae234;padding-left:1ex"> Is that really true, though?<br> Usually when you have an infinite loop, you have progress of some<br> sort. Infinite loops with no side effects can be removed from the<br> program according to the C standard, for example. So, in general,<br> we should allow programmers to express termination / progress,<br> right? <br></blockquote> At <br><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #8ae234;padding-left:1ex"> that point, no computation ever "bottoms out"?<br> Shouldn't a hypothetical purely functional programming language<br> better control this (by eg. Forcing totality?) It seems like we<br> lose much of the benefits of purity by muddying the waters with<br> divergence.<br> From an optimising compiler perspective, Haskell is on some weird<br> lose-lose space, where you lose out on traditional compiler<br> techniques that work on strict code, but it also does not allow<br> the awesome stuff you could do with "pure" computation because<br> bottom lurks everywhere.<br> What neat optimisations can be done on Haskell that can't be done<br> in a traditional imperative language? I genuinely want to know.<br> What are your thoughts on this?<br> Cheers<br> Siddharth<br><br> On Tue 19 Dec, 2017, 08:09 Brandon Allbery, <<a href="mailto:allbery.b@gmail.com" target="_blank">allbery.b@gmail.com</a>><br> wrote: <br><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #fcaf3e;padding-left:1ex"><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #e9b96e;padding-left:1ex"> Define "natural".<br><br> You might want to look into the concept of Turing<br> completeness. <br></blockquote></blockquote> One <br><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #fcaf3e;padding-left:1ex"><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #e9b96e;padding-left:1ex"> could define a subset of Haskell in which bottoms cannot<br> occur... but it turns out there's a lot of useful things you<br> can't do in such a language. (In strict languages, these often<br> are expressed <br></blockquote></blockquote> as <br><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #fcaf3e;padding-left:1ex"><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #e9b96e;padding-left:1ex"> infinite loops of one kind or another. Note also that any<br> dependency on external input is an infinite loop from the<br> perspective of the language, since it can only be broken by the<br> external entity providing the input.)<br><br> On Tue, Dec 19, 2017 at 1:47 AM, (IIIT) Siddharth Bhat <br></blockquote></blockquote> <siddharth.b <br><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #fcaf3e;padding-left:1ex"><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #e9b96e;padding-left:1ex"> <a href="mailto:hat@research.iiit.ac.in" target="_blank">hat@research.iiit.ac.in</a>> wrote: <br><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #ccc;padding-left:1ex"><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #ccc;padding-left:1ex"> I've been thinking about the issue of purity and speculation<br> lately, and from what little I have read, it looks like the<br> presence of bottom hiding inside a lazy value is a huge<br> issue.<br><br> How "natural" is it for bottoms to exist? If one were to <br></blockquote></blockquote></blockquote> change <br><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #e9b96e;padding-left:1ex"><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #ccc;padding-left:1ex"><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #ccc;padding-left:1ex"> Haskell and declare that any haskell value can be speculated<br> upon, what ramifications does this have?<br><br> Is it totally broken? Is it "correct" but makes programming<br> unpleasant? What's the catch?<br><br> Thanks,<br> Siddharth <br></blockquote></blockquote></blockquote></blockquote></blockquote></blockquote> <br><hr><br></blockquote></pre></blockquote></div></div><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><pre class="m_1882308129980466352m_-7535722637507639358k9mail"><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #729fcf;padding-left:1ex"> Haskell-Cafe mailing list<br> To (un)subscribe, modify options or view archives go to:<br> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/haskell-<wbr>cafe</a><br> Only members subscribed via the mailman list are allowed to post.<br></blockquote></pre></blockquote></div></div><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><pre class="m_1882308129980466352m_-7535722637507639358k9mail"><hr><br>Haskell-Cafe mailing list<br>To (un)subscribe, modify options or view archives go to:<br><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/haskell-<wbr>cafe</a><br>Only members subscribed via the mailman list are allowed to post.</pre></blockquote></div></div><div><br>
-- <br>
Sent from my Android device with K-9 Mail. Please excuse my brevity.</div></div></div>______________________________<wbr>_________________<span class=""><br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/haskell-<wbr>cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</span></blockquote></div><div dir="ltr">-- <br></div><div class="HOEnZb"><div class="h5"><div class="m_1882308129980466352gmail_signature" data-smartmail="gmail_signature"><div dir="ltr">Sending this from my phone, please excuse any typos!</div></div>
</div></div><br>______________________________<wbr>_________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/haskell-<wbr>cafe</a><br>
Only members subscribed via the mailman list are allowed to post.<br></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div>brandon s allbery kf8nh sine nomine associates</div><div><a href="mailto:allbery.b@gmail.com" target="_blank">allbery.b@gmail.com</a> <a href="mailto:ballbery@sinenomine.net" target="_blank">ballbery@sinenomine.net</a></div><div>unix, openafs, kerberos, infrastructure, xmonad <a href="http://sinenomine.net" target="_blank">http://sinenomine.net</a></div></div></div>
</div>