[Agda] type check performance

[Sergei Meshveliani]

Dear Agda developers,

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.
And the minimal memory is 10 Gb.
I recall the approach of using `abstract'.
In 2.5.3 in did not help. May it help in 2.5.4 ?

Are there ideas of how to optimize the type checker?

Regards,

------
Sergei

[Martin Escardo]

Post by Sergei Meshveliani
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.
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

[Nils Anders Danielsson]

Post by Martin Escardo
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].)

I could typecheck your code [1] using Agda 2.5.3 without enabling
sharing. The outcome of a single test was that 2.5.4 was ∼3% slower.

[Martin Escardo]

Post by Nils Anders Danielsson

Post by Martin Escardo
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].)

I could typecheck your code [1] using Agda 2.5.3 without enabling
sharing.

Right. I meant that with --sharing I get an error - sorry. Namely
"
/home/mhe/TypeTopology/source/UF-Equiv.lagda:325,57-61
I'm not sure if there should be a case for the constructor refl,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
x₁ ≟ x , _2385 f (f x) x x' refl p'
x₁ ≟ x' , p'
Possible reason why unification failed:
Cannot solve variable p' of type f x ≡ f x with solution
_2385 f (f x) x x refl p' because the variable occurs in the
solution, or in the type of one of the variables in the solution.
when checking that the pattern refl has type
x , _2385 f (f x) x x' refl p' ≡ x' , p'
"

Post by Nils Anders Danielsson
The outcome of a single test was that 2.5.4 was ∼3% slower.

Repeating the test a number of times, I get between a minimum of 7% and
a maximum of 12% slower.

Martin

[Sergei Meshveliani]

Post by Sergei Meshveliani
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.
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