That&#39;s very helpful to hear! <div>Engineering that piece has turned out to be a by of work! And it has some gnarly sub rabbit holes related to binder rep and lowering ast reps and raising then back up.  But it&#39;s looking tractable.  <span></span><br><br>On Thursday, March 17, 2016, Dominique Devriese &lt;<a href="mailto:dominique.devriese@gmail.com">dominique.devriese@gmail.com</a>&gt; wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Carter,<br>
<br>
Yes, that was the long-term idea, I think, although we hadn&#39;t really<br>
thought very deep about it and were focused on getting explicit<br>
substitutions in the syntax to work in the first place (and<br>
essentially failed...).  I had the impression that Ulf had a better<br>
long-term vision of how these explicit substitutions in the internal<br>
syntax could lead to a full solution for improving Agda&#39;s compile-time<br>
evaluation, perhaps he can comment further.<br>
<br>
I&#39;m interested to hear that you&#39;re looking into doing it more<br>
thoroughly in hopper. I hope to hear more about this in the future.<br>
<br>
See you,<br>
Dominique<br>
<br>
2016-03-16 17:38 GMT+01:00 Carter Schonwald &lt;<a href="javascript:;" onclick="_e(event, &#39;cvml&#39;, &#39;carter.schonwald@gmail.com&#39;)">carter.schonwald@gmail.com</a>&gt;:<br>
&gt; Are explicit substitutions related to having an explicit model heap? (At<br>
&gt; least if explicit sharing / sharing recovery is a goal, it seems to be the<br>
&gt; same in practice?)<br>
&gt;<br>
&gt;<br>
&gt; On Wednesday, March 16, 2016, Jesper Cockx &lt;<a href="javascript:;" onclick="_e(event, &#39;cvml&#39;, &#39;Jesper@sikanda.be&#39;)">Jesper@sikanda.be</a>&gt; wrote:<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; What can we do about this? I don&#39;t want to force users to use<br>
&gt;&gt;&gt; workarounds like copattern matching. Could we for instance add support<br>
&gt;&gt;&gt; for beta-redexes to the internal syntax?<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt; Maybe the explicit substitutions that some people were working on last<br>
&gt;&gt; Agda meeting could help?<br>
&gt;&gt;<br>
&gt;&gt; Jesper<br>
&gt;&gt;<br>
&gt;&gt; On Wed, Mar 16, 2016 at 5:06 PM, Nils Anders Danielsson &lt;<a href="javascript:;" onclick="_e(event, &#39;cvml&#39;, &#39;nad@cse.gu.se&#39;)">nad@cse.gu.se</a>&gt;<br>
&gt;&gt; wrote:<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; On 2016-03-12 00:33, Nils Anders Danielsson wrote:<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; I found another problem. I&#39;ve created a ticket on the bug tracker:<br>
&gt;&gt;&gt;&gt; <a href="https://github.com/agda/agda/issues/1901" target="_blank">https://github.com/agda/agda/issues/1901</a>.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; This problem has been fixed, and I can now type-check Andreas&#39; old code<br>
&gt;&gt;&gt; on my machine. However, Agda is still slow.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; I tried replacing all lambdas in coreAdjunction with pattern-matching<br>
&gt;&gt;&gt; lambdas, and then Agda became roughly ten times faster and used roughly<br>
&gt;&gt;&gt; nine times less memory. This suggests to me that (part of) the problem<br>
&gt;&gt;&gt; is that Agda always reduces lambda applications (as opposed to<br>
&gt;&gt;&gt; applications of pattern-matching lambdas and defined functions), as<br>
&gt;&gt;&gt; pointed out by Andrea.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; What can we do about this? I don&#39;t want to force users to use<br>
&gt;&gt;&gt; workarounds like copattern matching. Could we for instance add support<br>
&gt;&gt;&gt; for beta-redexes to the internal syntax?<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; --<br>
&gt;&gt;&gt; /NAD<br>
&gt;&gt;&gt; _______________________________________________<br>
&gt;&gt;&gt; Agda mailing list<br>
&gt;&gt;&gt; <a href="javascript:;" onclick="_e(event, &#39;cvml&#39;, &#39;Agda@lists.chalmers.se&#39;)">Agda@lists.chalmers.se</a><br>
&gt;&gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;<br>
&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="javascript:;" onclick="_e(event, &#39;cvml&#39;, &#39;Agda@lists.chalmers.se&#39;)">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="javascript:;" onclick="_e(event, &#39;cvml&#39;, &#39;Agda@lists.chalmers.se&#39;)">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>