That'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's looking tractable. <span></span><br><br>On Thursday, March 17, 2016, Dominique Devriese <<a href="mailto:dominique.devriese@gmail.com">dominique.devriese@gmail.com</a>> 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'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's compile-time<br>
evaluation, perhaps he can comment further.<br>
<br>
I'm interested to hear that you'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 <<a href="javascript:;" onclick="_e(event, 'cvml', 'carter.schonwald@gmail.com')">carter.schonwald@gmail.com</a>>:<br>
> Are explicit substitutions related to having an explicit model heap? (At<br>
> least if explicit sharing / sharing recovery is a goal, it seems to be the<br>
> same in practice?)<br>
><br>
><br>
> On Wednesday, March 16, 2016, Jesper Cockx <<a href="javascript:;" onclick="_e(event, 'cvml', 'Jesper@sikanda.be')">Jesper@sikanda.be</a>> wrote:<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?<br>
>><br>
>><br>
>> Maybe the explicit substitutions that some people were working on last<br>
>> Agda meeting could help?<br>
>><br>
>> Jesper<br>
>><br>
>> On Wed, Mar 16, 2016 at 5:06 PM, Nils Anders Danielsson <<a href="javascript:;" onclick="_e(event, 'cvml', 'nad@cse.gu.se')">nad@cse.gu.se</a>><br>
>> wrote:<br>
>>><br>
>>> On 2016-03-12 00:33, Nils Anders Danielsson wrote:<br>
>>>><br>
>>>> I found another problem. I've created a ticket on the bug tracker:<br>
>>>> <a href="https://github.com/agda/agda/issues/1901" target="_blank">https://github.com/agda/agda/issues/1901</a>.<br>
>>><br>
>>><br>
>>> 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?<br>
>>><br>
>>><br>
>>> --<br>
>>> /NAD<br>
>>> _______________________________________________<br>
>>> Agda mailing list<br>
>>> <a href="javascript:;" onclick="_e(event, 'cvml', 'Agda@lists.chalmers.se')">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>
>><br>
>><br>
><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="javascript:;" onclick="_e(event, 'cvml', 'Agda@lists.chalmers.se')">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>
><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="javascript:;" onclick="_e(event, 'cvml', 'Agda@lists.chalmers.se')">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>