[Haskell-cafe] Are bottoms ever natural?

[Theodore Lief Gannon]

Extremely relevant blog (even references Bloop/Floop) about how
distinguishing data from codata addresses this issue:
http://blog.sigfpe.com/2007/07/data-and-codata.html

On Dec 18, 2017 11:44 PM, "Brandon Allbery" <allbery.b at gmail.com> wrote:

> I'm tempted to refer you to the "Floop and Bloop and Gloop" chapter in
> _Gödel, Escher, Bach: an Eternal Golden Braid_.
>
> How exactly do you prove to the compiler that you have made sufficient
> progress? It's not enough to assume that doing any particular operation
> constitutes progress. And even in cases where you can provide such a proof,
> it usually requires dependent types to express because "progress" depends
> on some value. Consider that any given action may appear to have no side
> effects even in C unless the entire program is considered as a single unit.
> And also consider that Haskell expressions usually do not have "side
> effects" in this sense at all, unless you are in IO... and now you have to
> formalize what an IO "side effect" is in order to prove that you have
> actually accomplished something.
>
> On Tue, Dec 19, 2017 at 2:20 AM, (IIIT) Siddharth Bhat <
> siddharth.bhat at research.iiit.ac.in> 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.bhat 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
>>>> --
>>>> 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
>>> _______________________________________________
>>> 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!
>>
>
>
>
> --
> brandon s allbery kf8nh                               sine nomine
> associates
> allbery.b at gmail.com
> ballbery at sinenomine.net
> unix, openafs, kerberos, infrastructure, xmonad
> http://sinenomine.net
>
> _______________________________________________
> 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/90fde52e/attachment.html>