[Agda] Slow type-checking of records

[Andreas Nuyts]

Hi,

You can find the output of the options you give, here: 
https://github.com/anuyts/willow/blob/slowRecords/cat/Groupoids/positivityGraphs.txt
The big (but not huge? Memory usage goes up to about 8GiB of RAM and 
8GiB of swap) term you see is just the single object defined in the 
file. I don't really know how to interpret the rest.

Using copatterns does the job.

I suspected something like what Andrea says, but again, I don't think 
any terms should become GiB-huge. But maybe time & memory usage of 
creating these graphs depends in a very unfavorable way on the size of 
the term?

Thanks for the help!

Andreas

On 08-03-16 10:56, Nils Anders Danielsson wrote:
> On 2016-03-07 16:50, Andreas Nuyts wrote:
>> Oddly, disabling the positivity check doesn't solve the problem.
>
> Agda keeps track of how different arguments are used. This analysis is
> run even if the positivity checker is turned off. The analysis can be
> quite expensive.
>
> I tried using the -v machinery to see what happens in your case, but I
> have trouble type-checking the slow version of your file on my machine.
> If you add
>
>   {-# OPTIONS -vtc.pos.tick:100 -vtc.pos.graph:100 -vtc.pos.check:100
>               -vtc.pos.record:100 -vtc.pos.args:100 -vtc.pos:25 #-}
>
> to the top of the file, then you can perhaps get some information about
> what is going on.
>
>> I have the impression that this behaviour has to do with the fact that
>> the objects fwd and bck are themselves records (of the natural
>> transformation type _nt→_). Is this normal behaviour or should I file
>> a bug?
>
> Andrea Vezzosi once wrote that "I guess the lambda gets always
> beta-reduced in the type of the remaining fields, while a defined
> function will not be unfolded as much":
>
>   [Agda] agda slow
>   Andrea Vezzosi
>   Wed Jun 3 22:04:04 CEST 2015
>   https://lists.chalmers.se/pipermail/agda/2015/007867.html
>
> If this is the case, then the problem could be that the analysis
> mentioned above gets huge terms to process.
>

Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm