[Agda] type check cost

[Andrea Vezzosi]

a) What's an example of something you'd like to put below abstract but cannot?

b) abstract definitions do not reduce outside other abstract blocks of
the same module.
    So e.g. suppose (foo : Nat -> Nat) is declared as abstract, then
if the typechecker wants to compare (f (2 * 5)) and (f 10) it will
just compare (2 * 5) and 10, instead of reducing the applications of
'f' first.



On Sun, Oct 4, 2015 at 4:38 PM,  <mechvel at scico.botik.ru> wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda