[Agda] type check cost

[mechvel at scico.botik.ru]

There is another point: using `abstract'.

1) About 2/3 of the type check cost in my library is spent to _proofs_.
2) Almost all proofs can be abstracted.

But
a) Agda allows `abstract' almost nowhere in my library (there is a 
restriction on the scope
    level),
b) I do not know how much effect can give applying abstraction.

------
Sergei


mechvel at scico.botik.ru писал 04.10.2015 16:57:
> Dear Agda developers,
> 
> Currently I use  Agda 2.4.2.4  to develop my algebraic library called 
> DoCon-A.
> And it cannot type-check on a machine of  16 Gb RAM.
> 
> First, I had an impression that Agda 2.4.2.4 spends 3 times less space
> (on DoCon-A)
> than the previous version.
> Now, it looks like this factor is about  1.3.
> Small additions have been done to a couple of modules in the project,
> and the type check space
> grows to 16 Gb.
> 
> The type checker has  n^2,  or may be an exponent, somewhere in it.
> You have observed a simple example on this subject, and generally, you
> have a more clear idea
> about the source of this effect.
> 
> Currently I am not stuck with the DoCon-A library, because I have an
> access to a 24 Gb machine.
> But as the type checker has at least n^2 inside, this `currently' will
> hardly last more than 6 months
> of the project development.
> 
> Also you understand that even 2 Gb is unnaturally large space for
> type-checking it.
> This library is currently only a toy application, it has not any
> advanced methods, so far,
> it has only some definitions taken from textbooks on algebra.
> 
> It is evident that some radical improvements are desirable for the
> type check method.
> 
> Regards,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda