<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Oct 25, 2016 at 3:37 PM, Wolfram Kahl <span dir="ltr"><<a href="mailto:kahl@cas.mcmaster.ca" target="_blank">kahl@cas.mcmaster.ca</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 class="gmail-HOEnZb"><div class="gmail-h5">On Tue, Oct 25, 2016 at 02:19:54PM +0200, Ulf Norell wrote:<br>
> Before we discuss any particular solution to get call-by-need working, it's<br>
> useful to distinguish between two separate problems one might envision<br>
> call-by-need solving. The first, which I believe is the one you are<br>
> interested in, is to get efficient compile-time evaluation. The second is<br>
> to reduce the memory requirements of type checking by having more sharing<br>
> in terms. These are related but the second goal requires more care during<br>
> other phases of type checking than pure evaluation (such as unification).<br>
><br>
> The current implementation of `--sharing` is a hack using `IORef`s to see<br>
> how far it would get us towards solving problem number 2 (not very far).<br>
> The main problem with it, aside from being hacky, is that `IORef`s are too<br>
> persistent, so you run into problems when working interactively. For<br>
> instance, once you've looked at the normal form of a goal type you cannot<br>
> get back the original goal type, since it's been destructively updated to<br>
> its normal form. You could imagine ways to solve this problem, for instance<br>
> by making deep copies of terms before working on them, but it's easy to<br>
> miss cases and since the current implementation isn't really that nice to<br>
> begin with we haven't spent time on that.<br>
><br>
> The lambda-lifting issue I mentioned is a standard problem with<br>
> call-by-need. Consider the two Haskell functions pow2 and pow2':<br>
><br>
> pow2 0 = 1<br>
> pow2 n = r + r<br>
> where r = pow2 (n - 1)<br>
><br>
> r n = pow2' (n - 1)<br>
><br>
> pow2' 0 = 1<br>
> pow2' n = r n + r n<br>
><br>
> In pow2' we have lambda lifted the local binding r. If you run these you'll<br>
> find that pow2 is fast and pow2' is exponentially slow. The reason is that<br>
> call-by-need does not memoize function calls (like you seem to expect), it<br>
> just guarantees that named expressions are evaluated at most once.<br>
<br>
</div></div>In Haskell, the solution to that would be<br>
<br>
pow2' 0 = 1<br>
pow2' n = case r n of<br>
p -> p + p<br>
<br>
How can the effect of this be achieved in Agda (internal) syntax?<br></blockquote><div><br></div><div>pow2' n = case r n of λ { p → p + p }</div><div><br></div><div>(note the pattern matching lambda).</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<span class="gmail-"><br>
> If you want to experiment with call-by-need I would suggest implementing it<br>
> locally for the whnf-reduction in `Agda.TypeChecking.Reduce.<wbr>Fast`. There's<br>
> a single function reduceTm in which all reduction takes place (except for<br>
> some substitution), so that should save you from having to rewrite the<br>
> entire Agda code base.<br>
<br>
</span>Where does the lambda lifting happen?<br></blockquote><div><br></div><div>In Agda.TypeChecking.Monad.Signature.addConstant. Of course, it's not as simple as saying "let's not lambda lift then". There's no way to represent a function that is not lambda lifted in the Agda internals.</div><div><br></div><div>/ Ulf</div></div></div></div>