[Agda] Slow type-checking of records

[Andreas Abel]

Folklore suggests that you can improve performance by defining your 
record values via copattern matching and/or no-eta record types.

--Andreas

On 08.03.2016 00:50, Andreas Nuyts wrote:
> Dear All,
>
> I have an Agda file here (part of a library):
> https://github.com/anuyts/willow/blob/slowRecords/cat/Groupoids/CoreAdjunction.agda
>
> that contains two encodings of the same element of a record type of
> isomorphisms.
>
> In the encoding that is commented out, I define all four fields within
> the record block. This leads to very slow type-checking (150s, of which
> 110s for positivity - I've had longer times too), see
> https://github.com/anuyts/willow/blob/slowRecords/cat/Groupoids/CoreAdjunctionProfile.txt
>
> Oddly, disabling the positivity check doesn't solve the problem. Also,
> the file doesn't contain any type definitions, so it seems strange to
> begin with, that positivity-checking would be the problem.
> (The postulate 'hole' is there because (it seems) you cannot use the
> profiler from the command line when you have real holes.)
>
> In the encoding that is not commented out, I define the values for the
> fields fwd and bck (on which the types of fields src-id and tgt-id
> depend) seperately and then refer to them in the record block. This
> type-checks all right.
>
> 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?
>
> Best regards,
>
> Andreas Nuyts
>
> Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/