[Agda] type check performance

[Jesper Louis Andersen]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180605/406e5c83/attachment.html>