[Haskell-cafe] Are bottoms ever natural?
Brandon Allbery
allbery.b at gmail.com
Tue Dec 19 17:26:29 UTC 2017
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.
On Tue, Dec 19, 2017 at 11:51 AM, Siddharth Bhat <siddu.druid at gmail.com>
wrote:
> So, I have two opinions to share on this:
> Regarding the plane example, it is wrong to attempt to graph it on a
> plane, precisely because the domain is not the plane.
>
> 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*.
>
> So, what one would need is the ability to create these restricted domains,
> which certain languages have as far as I am aware.
>
> At that point, now that we track our domains and codomains correctly, all
> should work out?
>
> 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.
>
> Cheers,
> Siddharth
>
> On Tue 19 Dec, 2017, 20:36 Jonathan Paugh, <jpaugh at gmx.com> wrote:
>
>> 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.
>>
>> 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.
>> 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.
>>
>> On December 19, 2017 8:35:57 AM CST, Baa <aquagnu at gmail.com> wrote:
>>
>>> Pure functions can return "undefined" for some arguments values. So,
>>> such function is partially-defined. Its domain has "gaps". This can be
>>> coded in math, to avoid "undefined" (bottom), like
>>>
>>> x = {-100..100, 105, 107..200}
>>>
>>> It's impossible in Haskell, but IMHO its possible in F*, due to DepTypes
>>> and RefTypes ;)
>>>
>>> IMHO this is the reason to have bottom: possibility to return
>>> "undefined" w/ simple correct type in signature (hidden bottom). If you
>>> have a way to code arguments domains, no need to have bottom for pure
>>> functions to "signal" gaps - gaps happen in run-time :) This is the one
>>> of reasons for bottom to exist, as far as I understand. May be there are
>>> other reasons :)
>>>
>>> ===
>>> Best regards, Paul
>>>
>>> Siddharth,
>>>>
>>>> how would you deal with functions that terminate for some
>>>> arguments/inputs but do not terminate for the others ?
>>>>
>>>> Alexey.
>>>>
>>>> On Tue, 2017-12-19 at 07:20 +0000, (IIIT) Siddharth Bhat wrote:
>>>>
>>>>> Is that really true, though?
>>>>>> Usually when you have an infinite loop, you have progress of some
>>>>>> sort. Infinite loops with no side effects can be removed from the
>>>>>> program according to the C standard, for example. So, in general,
>>>>>> we should allow programmers to express termination / progress,
>>>>>> right?
>>>>>>
>>>>> At
>>>>>
>>>>>> that point, no computation ever "bottoms out"?
>>>>>> Shouldn't a hypothetical purely functional programming language
>>>>>> better control this (by eg. Forcing totality?) It seems like we
>>>>>> lose much of the benefits of purity by muddying the waters with
>>>>>> divergence.
>>>>>> From an optimising compiler perspective, Haskell is on some weird
>>>>>> lose-lose space, where you lose out on traditional compiler
>>>>>> techniques that work on strict code, but it also does not allow
>>>>>> the awesome stuff you could do with "pure" computation because
>>>>>> bottom lurks everywhere.
>>>>>> What neat optimisations can be done on Haskell that can't be done
>>>>>> in a traditional imperative language? I genuinely want to know.
>>>>>> What are your thoughts on this?
>>>>>> Cheers
>>>>>> Siddharth
>>>>>>
>>>>>> On Tue 19 Dec, 2017, 08:09 Brandon Allbery, <allbery.b at gmail.com>
>>>>>> wrote:
>>>>>>
>>>>>>> Define "natural".
>>>>>>>>
>>>>>>>> You might want to look into the concept of Turing
>>>>>>>> completeness.
>>>>>>>>
>>>>>>> One
>>>>>>
>>>>>>> could define a subset of Haskell in which bottoms cannot
>>>>>>>> occur... but it turns out there's a lot of useful things you
>>>>>>>> can't do in such a language. (In strict languages, these often
>>>>>>>> are expressed
>>>>>>>>
>>>>>>> as
>>>>>>
>>>>>>> infinite loops of one kind or another. Note also that any
>>>>>>>> dependency on external input is an infinite loop from the
>>>>>>>> perspective of the language, since it can only be broken by the
>>>>>>>> external entity providing the input.)
>>>>>>>>
>>>>>>>> On Tue, Dec 19, 2017 at 1:47 AM, (IIIT) Siddharth Bhat
>>>>>>>>
>>>>>>> <siddharth.b
>>>>>>
>>>>>>> hat at research.iiit.ac.in> wrote:
>>>>>>>>
>>>>>>>>> I've been thinking about the issue of purity and speculation
>>>>>>>>>> lately, and from what little I have read, it looks like the
>>>>>>>>>> presence of bottom hiding inside a lazy value is a huge
>>>>>>>>>> issue.
>>>>>>>>>>
>>>>>>>>>> How "natural" is it for bottoms to exist? If one were to
>>>>>>>>>>
>>>>>>>>> change
>>>>>>>
>>>>>>>> Haskell and declare that any haskell value can be speculated
>>>>>>>>>> upon, what ramifications does this have?
>>>>>>>>>>
>>>>>>>>>> Is it totally broken? Is it "correct" but makes programming
>>>>>>>>>> unpleasant? What's the catch?
>>>>>>>>>>
>>>>>>>>>> Thanks,
>>>>>>>>>> Siddharth
>>>>>>>>>>
>>>>>>>>>
>>>> ------------------------------
>>>>
>>>> Haskell-Cafe mailing list
>>>> To (un)subscribe, modify options or view archives go to:
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>>> Only members subscribed via the mailman list are allowed to post.
>>>>
>>> ------------------------------
>>>
>>> Haskell-Cafe mailing list
>>> To (un)subscribe, modify options or view archives go to:
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>> Only members subscribed via the mailman list are allowed to post.
>>>
>>>
>> --
>> Sent from my Android device with K-9 Mail. Please excuse my brevity.
>> _______________________________________________
>> Haskell-Cafe mailing list
>> To (un)subscribe, modify options or view archives go to:
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>> Only members subscribed via the mailman list are allowed to post.
>
> --
> Sending this from my phone, please excuse any typos!
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
>
--
brandon s allbery kf8nh sine nomine associates
allbery.b at gmail.com ballbery at sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20171219/5a026814/attachment.html>
More information about the Haskell-Cafe
mailing list