On 08.06.2018 01:14, Steven Schveighoffer wrote:
> 
> No matter what is inside fn, it will return S.init, if it returns. The question to answer is, can we assume all functions don't enter infinite loops, and if we can assume this, then why couldn't the compiler simply replace a call to fn with S.init?
> 
> And the case FeepingCreature gives is pretty compelling, because it's a real example, not a toy example.
> 
> -Steve

FeepingCreature's example does not really qualify as a do-nothing loop, because the loop produces a value that you (presumably) later access.

In any case, I don't think the right answer is to make programs that enter infinite loops that do nothing undefined behavior (like in C++), but they should possibly be allowed to be removed, though it can be surprising, see: https://blog.regehr.org/archives/140
(However, the "Fermat" example is a bit contrived, because presumably one would also want to print the specific counterexample, breaking the "optimization".)

On 11.06.2018 16:39, Timon Gehr wrote:
> 
> FeepingCreature's example does not really qualify as a do-nothing loop, because the loop produces a value that you (presumably) later access.

Hm, ok. The problem is actually there, but it is not that the 'find' call will get removed, it is that the loop within find's implementation will be seen as doing nothing and producing nothing after inlining, breaking find's postcondition.

On 6/11/18 10:43 AM, Timon Gehr wrote:
> On 11.06.2018 16:39, Timon Gehr wrote:
>>
>> FeepingCreature's example does not really qualify as a do-nothing loop, because the loop produces a value that you (presumably) later access.
> 
> Hm, ok. The problem is actually there, but it is not that the 'find' call will get removed, it is that the loop within find's implementation will be seen as doing nothing and producing nothing after inlining, breaking find's postcondition.

Actually, one thing that can be determined statically is that it will never return. Essentially, this particular find function (with predicate inlining) will fold to:

while(true) {}

Since the final return outside the loop is obviously never reached, and the return inside the loop cannot be reached.

So I would assume this would properly be translated to an infinite loop.

I was not expecting that the compiler might eliminate infinite loops that it can prove are infinite loops, more like it should eliminate calls that trivially can be proven to do nothing based on the signature of the function.

-Steve

On 11.06.2018 20:15, Steven Schveighoffer wrote:
> On 6/11/18 10:43 AM, Timon Gehr wrote:
>> On 11.06.2018 16:39, Timon Gehr wrote:
>>>
>>> FeepingCreature's example does not really qualify as a do-nothing loop, because the loop produces a value that you (presumably) later access.
>>
>> Hm, ok. The problem is actually there, but it is not that the 'find' call will get removed, it is that the loop within find's implementation will be seen as doing nothing and producing nothing after inlining, breaking find's postcondition.
> 
> Actually, one thing that can be determined statically is that it will never return. Essentially, this particular find function (with predicate inlining) will fold to:
> 
> while(true) {}
> 
> Since the final return outside the loop is obviously never reached, and the return inside the loop cannot be reached.
> 
> So I would assume this would properly be translated to an infinite loop.
> 
> I was not expecting that the compiler might eliminate infinite loops that it can prove are infinite loops, more like it should eliminate calls that trivially can be proven to do nothing based on the signature of the function.
> 
> -Steve

Well, if the language definition is reasonable, then if calls to `void foo()pure @nothrow { while(true){} }` can be elided, so can the `while(true){}` loop itself.

On 6/11/18 2:23 PM, Timon Gehr wrote:
> On 11.06.2018 20:15, Steven Schveighoffer wrote:
>> On 6/11/18 10:43 AM, Timon Gehr wrote:
>>> On 11.06.2018 16:39, Timon Gehr wrote:
>>>>
>>>> FeepingCreature's example does not really qualify as a do-nothing loop, because the loop produces a value that you (presumably) later access.
>>>
>>> Hm, ok. The problem is actually there, but it is not that the 'find' call will get removed, it is that the loop within find's implementation will be seen as doing nothing and producing nothing after inlining, breaking find's postcondition.
>>
>> Actually, one thing that can be determined statically is that it will never return. Essentially, this particular find function (with predicate inlining) will fold to:
>>
>> while(true) {}
>>
>> Since the final return outside the loop is obviously never reached, and the return inside the loop cannot be reached.
>>
>> So I would assume this would properly be translated to an infinite loop.
>>
>> I was not expecting that the compiler might eliminate infinite loops that it can prove are infinite loops, more like it should eliminate calls that trivially can be proven to do nothing based on the signature of the function.
>>
> 
> Well, if the language definition is reasonable, then if calls to `void foo()pure @nothrow { while(true){} }` can be elided, so can the `while(true){}` loop itself.

Yes, it does seem that way.

Eliding (or moving) opaque calls in general if you can't see what the call is actually doing seems to be a minefield that probably cannot reasonably be navigated. The only reasonable elision seems to be for pure calls that have already been made so we know they actually return.

I'm curious if Haskell can properly navigate this with its lazy calls, or if it is subject to such oddities.

-Steve