[Agda] type check performance

[Sergei Meshveliani]

On Tue, 2018-06-05 at 22:52 +0200, Jesper Louis Andersen wrote:
> On Mon, Jun 4, 2018 at 8:38 PM Sergei Meshveliani <mechvel at botik.ru>
> wrote:
> 
>         it occurs that introducing call by need does not change any
>         essentially
>         the type check performance -- on the DoCon-A. It is about 10%
>         speed up.
> 
> 
> I see it somewhat differently, I must admit:
> 
> 
> If you can get 10% speedup in any compiler in produced code or a
> reduction in compilation time, this is normally seen as a very high
> level of improvement. Even 1-2% here and there are welcome. So 10% is
> by all senses and purposes a massive gain. Given Agda, you could argue
> the type checker has an equal amount of importance.
> 
> 
> The background for this is that usually a type checker or compiler has
> a lot of things which it is so-to-speak forced to look at and cannot
> skip. So barring a breakthrough of some kind of rather epic
> proportions, it is probably hard to speed up the system. And that the
> low-hanging fruit is often picked early on, and it becomes
> considerably harder to pull off the big increases.
> 

My note was only on the type check stage.
In my application the type checker deals with terms in which large
subterms repeat many times.
And it occurs that this application cannot be type-checked on a computer
that has 8 Gb memory. This application 
(see DoCon-A-2.02 on Web, only some standard functions changed their
paths to fit the experimental Standard library) is such a small piece of
algebra, that, I expect its type check to fit into somewhat 2 Gb. 

I am not sure. Probably, I (or may be also Agda developers) need to
study the effect in detail on an example. 

Regards,

------
Sergei