<div dir="ltr"><div class="gmail_extra">Before we discuss any particular solution to get call-by-need working, it's useful to distinguish between two separate problems one might envision call-by-need solving. The first, which I believe is the one you are interested in, is to get efficient compile-time evaluation. The second is to reduce the memory requirements of type checking by having more sharing in terms. These are related but the second goal requires more care during other phases of type checking than pure evaluation (such as unification).</div><div class="gmail_extra"><br></div><div class="gmail_extra">The current implementation of `--sharing` is a hack using `IORef`s to see how far it would get us towards solving problem number 2 (not very far). The main problem with it, aside from being hacky, is that `IORef`s are too persistent, so you run into problems when working interactively. For instance, once you've looked at the normal form of a goal type you cannot get back the original goal type, since it's been destructively updated to its normal form. You could imagine ways to solve this problem, for instance by making deep copies of terms before working on them, but it's easy to miss cases and since the current implementation isn't really that nice to begin with we haven't spent time on that.</div><div class="gmail_extra"><br></div><div class="gmail_extra">The lambda-lifting issue I mentioned is a standard problem with call-by-need. Consider the two Haskell functions pow2 and pow2':</div><div class="gmail_extra"><br></div><div class="gmail_extra"><div class="gmail_extra">pow2 0 = 1</div><div class="gmail_extra">pow2 n = r + r</div><div class="gmail_extra"> where r = pow2 (n - 1)</div><div class="gmail_extra"><br></div><div class="gmail_extra">r n = pow2' (n - 1)</div><div class="gmail_extra"><br></div><div class="gmail_extra">pow2' 0 = 1</div><div class="gmail_extra">pow2' n = r n + r n</div><div><br></div><div>In pow2' we have lambda lifted the local binding r. If you run these you'll find that pow2 is fast and pow2' is exponentially slow. The reason is that call-by-need does not memoize function calls (like you seem to expect), it just guarantees that named expressions are evaluated at most once.</div><div><br></div><div>If you want to experiment with call-by-need I would suggest implementing it locally for the whnf-reduction in `Agda.TypeChecking.Reduce.Fast`. There's a single function reduceTm in which all reduction takes place (except for some substitution), so that should save you from having to rewrite the entire Agda code base.</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Oct 24, 2016 at 4:42 AM, Martin Stone Davis <span dir="ltr"><<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div bgcolor="#FFFFFF">
<p>Despite my <a href="https://github.com/agda/agda/issues/426#issuecomment-254111273" target="_blank">best
efforts</a> to try to get around the performance problems that
are seemingly inherent in call-by-name, I have not found a
satisfactory solution, so I've come to agree that we need a
different evaluation strategy. Exactly what, I don't know, but I'm
starting to read through the Agda (Haskell) code, hoping to put
myself in a position to help.<br>
</p>
<p>I'd like some explanation how the current call-by-need
implementation, `--sharing`, works (or doesn't) and get your
thoughts on what a promising solution might look like. <br>
</p>
<p>On the subject of `--sharing`, Ulf Norell mentioned <a href="https://github.com/agda/agda/pull/1867#issuecomment-187596312" target="_blank">here</a>
that it's too problematic to continue improving. I'd like to know
what's fundamentally wrong with it. He mentions <a href="https://github.com/agda/agda/issues/426#issuecomment-129023261" target="_blank">here</a>
that substitution is not memoizing pointers, but I'm guessing that
that could be fixed and is *not* what's fundamentally wrong with
`--sharing`. In the same comment he mentions that a particular
where clause is problematic for `--sharing` "because of lambda
lifting". I'm unclear on how this is breaking call-by-need. Is the
function in the where clause getting lambda lifted? Does that
somehow lead to the top-level function not getting memoized?<br>
</p>
<p>What's the future of Agda's evaluation strategy?</p>
<p>(If this should have been posted in the issue tracker, please
continue the conversation there.)</p>
</div>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div></div>