<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Oct 25, 2016 at 4:43 PM, Wolfram Kahl <span dir="ltr">&lt;<a href="mailto:kahl@cas.mcmaster.ca" target="_blank">kahl@cas.mcmaster.ca</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Tue, Oct 25, 2016 at 04:25:32PM +0200, Ulf Norell wrote:<br>
&gt; On Tue, Oct 25, 2016 at 3:37 PM, Wolfram Kahl &lt;<a href="mailto:kahl@cas.mcmaster.ca">kahl@cas.mcmaster.ca</a>&gt; wrote:<br>
&gt;<br>
&gt; &gt; On Tue, Oct 25, 2016 at 02:19:54PM +0200, Ulf Norell wrote:<br>
&gt; &gt; &gt; Before we discuss any particular solution to get call-by-need working,<br>
&gt; &gt; it&#39;s<br>
&gt; &gt; &gt; useful to distinguish between two separate problems one might envision<br>
&gt; &gt; &gt; call-by-need solving. The first, which I believe is the one you are<br>
&gt; &gt; &gt; interested in, is to get efficient compile-time evaluation. The second is<br>
&gt; &gt; &gt; to reduce the memory requirements of type checking by having more sharing<br>
&gt; &gt; &gt; in terms. These are related but the second goal requires more care during<br>
&gt; &gt; &gt; other phases of type checking than pure evaluation (such as unification).<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; The current implementation of `--sharing` is a hack using `IORef`s to see<br>
</span>&gt; &gt; &gt; how far it would get us towards solving problem number 2 (not very far)..<br>
<div><div class="h5">&gt; &gt; &gt; The main problem with it, aside from being hacky, is that `IORef`s are<br>
&gt; &gt; too<br>
&gt; &gt; &gt; persistent, so you run into problems when working interactively. For<br>
&gt; &gt; &gt; instance, once you&#39;ve looked at the normal form of a goal type you cannot<br>
&gt; &gt; &gt; get back the original goal type, since it&#39;s been destructively updated to<br>
&gt; &gt; &gt; its normal form. You could imagine ways to solve this problem, for<br>
&gt; &gt; instance<br>
&gt; &gt; &gt; by making deep copies of terms before working on them, but it&#39;s easy to<br>
&gt; &gt; &gt; miss cases and since the current implementation isn&#39;t really that nice to<br>
&gt; &gt; &gt; begin with we haven&#39;t spent time on that.<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; The lambda-lifting issue I mentioned is a standard problem with<br>
&gt; &gt; &gt; call-by-need. Consider the two Haskell functions pow2 and pow2&#39;:<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; pow2 0 = 1<br>
&gt; &gt; &gt; pow2 n = r + r<br>
&gt; &gt; &gt;   where r = pow2 (n - 1)<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; r n = pow2&#39; (n - 1)<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; pow2&#39; 0 = 1<br>
&gt; &gt; &gt; pow2&#39; n = r n + r n<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; In pow2&#39; we have lambda lifted the local binding r. If you run these<br>
&gt; &gt; you&#39;ll<br>
&gt; &gt; &gt; find that pow2 is fast and pow2&#39; is exponentially slow. The reason is<br>
&gt; &gt; that<br>
&gt; &gt; &gt; call-by-need does not memoize function calls (like you seem to expect),<br>
&gt; &gt; it<br>
&gt; &gt; &gt; just guarantees that named expressions are evaluated at most once.<br>
&gt; &gt;<br>
&gt; &gt; In Haskell, the solution to that would be<br>
&gt; &gt;<br>
&gt; &gt; pow2&#39; 0 = 1<br>
&gt; &gt; pow2&#39; n = case r n of<br>
&gt; &gt;   p -&gt; p + p<br>
&gt; &gt;<br>
&gt; &gt; How can the effect of this be achieved in Agda (internal) syntax?<br>
&gt; &gt;<br>
&gt;<br>
&gt; pow2&#39; n = case r n of λ { p → p + p }<br>
&gt;<br>
&gt; (note the pattern matching lambda).<br>
<br>
</div></div>Well, in Haskell, ``case&#39;&#39; is primitive, and (specialised to this case)<br>
guarantees that p is evaluated only once.<br>
<br>
In Agda, ``case_of_&#39;&#39; is not primitive, so call by name has the opportunity<br>
to duplicate work. And aren&#39;t pattern matching lambdas translated into<br>
local functions, and then presumably lambda-lifted?<br></blockquote><div><br></div><div>Yes, you are right of course. That code only works if the pattern matching lambda is strict in its argument (which it isn&#39;t in the example). Adding a primForce on p should make it work though.</div><div><br></div><div>/ Ulf</div></div></div></div>