[Agda] Slow type-checking of records

[Jesper Cockx]

>
> What can we do about this? I don't want to force users to use
> workarounds like copattern matching. Could we for instance add support
> for beta-redexes to the internal syntax?


Maybe the explicit substitutions that some people were working on last Agda
meeting could help?

Jesper

On Wed, Mar 16, 2016 at 5:06 PM, Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 2016-03-12 00:33, Nils Anders Danielsson wrote:
>
>> I found another problem. I've created a ticket on the bug tracker:
>> https://github.com/agda/agda/issues/1901.
>>
>
> This problem has been fixed, and I can now type-check Andreas' old code
> on my machine. However, Agda is still slow.
>
> I tried replacing all lambdas in coreAdjunction with pattern-matching
> lambdas, and then Agda became roughly ten times faster and used roughly
> nine times less memory. This suggests to me that (part of) the problem
> is that Agda always reduces lambda applications (as opposed to
> applications of pattern-matching lambdas and defined functions), as
> pointed out by Andrea.
>
> What can we do about this? I don't want to force users to use
> workarounds like copattern matching. Could we for instance add support
> for beta-redexes to the internal syntax?
>
>
> --
> /NAD
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160316/f08adda6/attachment.html