[Agda] Agda takes a long time to type check.

[Nils Anders Danielsson]

On 2009-01-26 11:10, Vilius Naudziunas wrote:

> Could you tell me what kind of constructions in Agda could be causing 
> such behaviour? Maybe I could avoid them by generating code differently.

Could you show us a small piece of code which triggers the performance
problem?

I have sometimes had problems when instantiating parameterised modules
with large records. Agda performs equality checking by normalising the
records and checking them for syntactic equality; no use is made of the
fact that all these records were originally the same one, leading to
lots of duplicated (n-plicated) work.

One can perhaps work around this problem by instantiating modules as
late as possible. However, Agda should really handle this better. Ulf
started optimising the equality checker a while ago, but I do not know
if he plans to finish this project anytime soon.

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.