<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">&lt;<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>&gt;</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&#39;s more efficient to avoid implicit arguments altogether,<br>
except for truly &quot;background&quot; 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, &quot;obvious&quot; 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&#39;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&#39;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>