[Agda] type check performance

[Martin Escardo]

On 05/06/18 21:52, jesper.louis.andersen at gmail.com wrote:
> On Mon, Jun 4, 2018 at 8:38 PM Sergei Meshveliani <mechvel at botik.ru 
> <mailto: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.

In my case, Agda 2.5.3 is faster than 2.5.4.

Typechecking [1] takes respectively 43 and 48 seconds (12% more) in the 
same laptop.

(NB. I tried 2.5.3 with --no-sharing, and then I get a unification 
failure in [2].)

Martin

[1] 
https://github.com/martinescardo/TypeTopology/blob/master/source/everything.lagda

[2] 
https://github.com/martinescardo/TypeTopology/blob/master/source/UF-Equiv.lagda