[Haskell-cafe] Are bottoms ever natural?

Tue Dec 19 22:56:05 UTC 2017

Dependently typed languages usually have a totality checker and notion of
codata.  Idris seems most likely to have exploited that for optimizations,
but I haven't seen anything about interesting transformations. Its strict
of course but presumably if you're total you could play with that.

On Dec 19, 2017 8:53 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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20171219/b35d3042/attachment.html>