[Agda] type check cost

[Andrea Vezzosi]

You raise, as in the past, a valid concern.

I would like to point out that the memory consumption is not primarily
a factor of the amount of code, but it depends greatly on the kind of
code you write.

We can typecheck the whole standard library in 1.5Gb while I have an
example where changing a single line in a small developement can push
me from 3Gb to over 16Gb.

The functor composition example from Wolfram is similar, you can load
the modules defining the functors just fine, but if you try to
typecheck the composition it's a lost cause.

In that example we know that the culprit is a pair of values of the
category type which the typechecker expands to compare, but presumably
they get too big, or just reducing them is inefficient.

At the last AIM, Ulf suggested that disabling eta equality for record
types and defining their values with copatterns can help block
reduction, and so keep typechecking from having to do too much work.
(Disabling eta is only possible in the master branch atm).


Also at the last AIM, there was an effort to introduce a way to
express sharing in the internal syntax, so that we might get closer to
call-by-need, rather than call-by-name.

I figure we probably also need a way to have heuristics for when
reducing an application is a good way to check for equality, so that
we get to sometimes exploit for efficiency the layers of abstraction
used in the code.




On Sun, Oct 4, 2015 at 3:57 PM,  <mechvel at scico.botik.ru> wrote:
> 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