<div dir="ltr">Got it! Thanks!!</div><br><div class="gmail_quote"><div dir="ltr">On Sun, Mar 27, 2016 at 7:44 PM Dan Doel <<a href="mailto:dan.doel@gmail.com">dan.doel@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On Sun, Mar 27, 2016 at 4:42 PM, George Colpitts<br>
<<a href="mailto:george.colpitts@gmail.com" target="_blank">george.colpitts@gmail.com</a>> wrote:<br>
> I still don't understand why<br>
><br>
> as' i s<br>
>      | i >= n    = s<br>
>      | otherwise = as' (i + 2) (s + (-1) / i + 1 / (i + 1))<br>
><br>
><br>
> is not lazy in its second arg as it only has to evaluate it if i >= n. This<br>
> seems exactly analogous to or, ||, which only needs to evaluate its second<br>
> arg if its first arg is False. || is definitely lazy in its second argument.<br>
> Can you explain why as' is strict in its second arg, s? Is it due to the<br>
> following from,<br>
> <a href="https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/Demand" rel="noreferrer" target="_blank">https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/Demand</a> ?<br>
<br>
The simplest way to see why as' is strict in s is to use the actual<br>
definition of strictness, and not think about operational semantics.<br>
The definition is that a function f is strict if `f undefined =<br>
undefined`. So, what is `as' i undefined`?<br>
<br>
If `i >= n` then `as' i undefined = undefined`<br>
if not `i >= n` then `as' i undefined = as' (i+2) undefined`<br>
<br>
The second case holds because Double arithmetic is strict, so the<br>
complex expression will be undefined because s is.<br>
<br>
>From these cases we can reason that the result will always be<br>
undefined. Either the value of i will grow such that the first case<br>
succeeds, or if that will never happen (if n is NaN for instance), the<br>
loop will continue forever, in which case the result is equivalent to<br>
undefined semantically.<br>
<br>
Because of this denotational analysis, we are at liberty to make the<br>
operation of as' such that it always evaluates s immediately, because<br>
it won't change the answer. And that is the optimization that saves<br>
time/space.<br>
<br>
By contrast, my alternate function:<br>
<br>
    as' i s<br>
      | i >= n = (i, s)<br>
      | otherwise = as' (i+2) (...)<br>
<br>
is easily not strict in s, because:<br>
<br>
    as' i undefined = (i, undefined)<br>
<br>
when `i >= n` is True, and (i, undefined) is not undefined. So it is<br>
invalid to perform the same optimization, because it would change the<br>
answer on some inputs. We happen to know that all the places the<br>
function is used, those two answers would be equivalent (because we<br>
just project out the second item), but that's somewhat difficult,<br>
non-local reasoning.<br>
<br>
Note that GHC does do some optimization. The loop in until is (in this<br>
case) a loop on a pair, and it figures out that the loop is strict in<br>
the pair, and eliminates the construction of the pair (by passing two<br>
separate arguments, and returning an unboxed pair from the loop).<br>
Optimizing the pieces of the pair would have to be a sort of<br>
speculative operation (without doing a global analysis), where 2^k<br>
different versions of the loop are generated (where k is the number of<br>
non-strict pieces), and the call sites are optimized to call the best<br>
of those versions for them. But 2^k isn't a good looking number for<br>
this sort of thing.<br>
<br>
-- Dan<br>
</blockquote></div>