<div dir="ltr"><div class="gmail_quote"><div dir="ltr">On Mon, Jun 4, 2018 at 8:38 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">it occurs that introducing call by need does not change any essentially<br>
the type check performance -- on the DoCon-A. It is about 10% speed up.<br>
</blockquote><div><br></div><div>I see it somewhat differently, I must admit:</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div><br></div></div></div>