<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Apr 13, 2015 at 8:13 AM, Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 13.04.2015 07:32, N. Raghavendra wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br></blockquote></span><span class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Looks like Agda has to do a lot of work inferring these implicits! I am<br>
wondering if it's more efficient to avoid implicit arguments altogether,<br>
except for truly "background" stuff like universe levels. Without<br>
implicits, it looks like Agda has to do less work, and it may also be<br>
easy for other human readers to understand the code. What do you feel?<br>
</blockquote>
<br></span>
Boring, "obvious" type information tires the human reader out quickly. So it is necessary to omit it. Ideally, Agda would exactly infer what we consider obvious...<br></blockquote><div><br></div><div>Also, it's not at all the case that Agda has to do less work if you make everything</div><div>explicit. The reason for that is that Agda is not very trusting of the user, so if you</div><div>write something explicitly that Agda can figure out for itself it needs to check that</div><div>what you wrote is actually the right thing, i.e. it matches what Agda inferred it ought</div><div>to be.</div><div><br></div><div>Of course it's not always faster to leave things implicit, but there are certainly</div><div>cases where it will be.</div><div><br></div><div>/ Ulf</div></div></div></div>