[Agda] Slow type-checking of records

[Dominique Devriese]

Carter,

Yes, that was the long-term idea, I think, although we hadn't really
thought very deep about it and were focused on getting explicit
substitutions in the syntax to work in the first place (and
essentially failed...).  I had the impression that Ulf had a better
long-term vision of how these explicit substitutions in the internal
syntax could lead to a full solution for improving Agda's compile-time
evaluation, perhaps he can comment further.

I'm interested to hear that you're looking into doing it more
thoroughly in hopper. I hope to hear more about this in the future.

See you,
Dominique

2016-03-16 17:38 GMT+01:00 Carter Schonwald <carter.schonwald at gmail.com>:
> 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>
>> 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
>>
>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>