Are explicit substitutions related to having an explicit model heap? (At least if explicit sharing / sharing recovery is a goal, it seems to be the same in practice?<span></span>) <br><br>On Wednesday, March 16, 2016, Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">What can we do about this? I don't want to force users to use<br>
workarounds like copattern matching. Could we for instance add support<br>
for beta-redexes to the internal syntax?</blockquote><div><br></div><div>Maybe the explicit substitutions that some people were working on last Agda meeting could help?<br><br></div><div>Jesper <br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Mar 16, 2016 at 5:06 PM, Nils Anders Danielsson <span dir="ltr"><<a href="javascript:_e(%7B%7D,'cvml','nad@cse.gu.se');" target="_blank">nad@cse.gu.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span>On 2016-03-12 00:33, Nils Anders Danielsson wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I found another problem. I've created a ticket on the bug tracker:<br>
<a href="https://github.com/agda/agda/issues/1901" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/1901</a>.<br>
</blockquote>
<br></span>
This problem has been fixed, and I can now type-check Andreas' old code<br>
on my machine. However, Agda is still slow.<br>
<br>
I tried replacing all lambdas in coreAdjunction with pattern-matching<br>
lambdas, and then Agda became roughly ten times faster and used roughly<br>
nine times less memory. This suggests to me that (part of) the problem<br>
is that Agda always reduces lambda applications (as opposed to<br>
applications of pattern-matching lambdas and defined functions), as<br>
pointed out by Andrea.<br>
<br>
What can we do about this? I don't want to force users to use<br>
workarounds like copattern matching. Could we for instance add support<br>
for beta-redexes to the internal syntax?<div><div><br>
<br>
-- <br>
/NAD<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="javascript:_e(%7B%7D,'cvml','Agda@lists.chalmers.se');" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>
</blockquote>