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, 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@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@gmail.com ballbery@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!

Also I want to point out to interesting and powerful language Shen: http://shenlanguage.org/learn-shen/index.html which supports lazy evaluation, dependent types and many other things: you can construct own rules in type-system level translator. I'm not familiar with Shen but I suppose it's possible to programming without "botton" in Shen. It supports Haskell too. By default partial functions are "tracked" and can be traced, but w/ Dep. types this can be avoided as I understand... So, such languages exists ;) === Best regards, Paul

Also, I'm sorry if the tone of the email is hostile, I don't mean it that way :) I just want to start a discussion about compiler and language design around lazy languages that permit bottom as an inhabitant.

On Tue 19 Dec, 2017, 08:20 (IIIT) Siddharth Bhat, < siddharth.bhat@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, 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@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@gmail.com ballbery@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!

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" 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@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, 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@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@gmail.com ballbery@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@gmail.com ballbery@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.