[Agda] Slow type-checking of records

[Carter Schonwald]

That's very helpful to hear!
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.

On Thursday, March 17, 2016, Dominique Devriese <
dominique.devriese at gmail.com> wrote:

> 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
> <javascript:;>>:
> > 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
> <javascript:;>> 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:;>>
> >> 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:;>
> >>> https://lists.chalmers.se/mailman/listinfo/agda
> >>
> >>
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se <javascript:;>
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se <javascript:;>
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160317/498830b4/attachment.html