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

[Anton Setzer]

Nils Anders Danielsson wrote:
> 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.
>
I have a student doing a PhD project, and he had similar problems with
parametrised modules
(where the module was supposed to be parametrised by replacing parameter
variables by variables
with the same name, which was quite complicated to achieve in the first
place). We are now
temporarily working with non-parametrised modules and using postulates
instead, but that's not
a good solution.

Anton

-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------