[Agda] Slow type-checking of records

[Carter Schonwald]

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?)

On Wednesday, March 16, 2016, Jesper Cockx <Jesper at sikanda.be> wrote:

> 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
> <javascript:_e(%7B%7D,'cvml','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
>> <javascript:_e(%7B%7D,'cvml','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/505ce5e1/attachment.html