[Agda] Re: Implicit arguments

[Ulf Norell]

On Mon, Apr 13, 2015 at 8:13 AM, Andreas Abel <abela at chalmers.se> wrote:

> On 13.04.2015 07:32, N. Raghavendra wrote:
>
>>
>> Looks like Agda has to do a lot of work inferring these implicits!  I am
>> wondering if it's more efficient to avoid implicit arguments altogether,
>> except for truly "background" stuff like universe levels.  Without
>> implicits, it looks like Agda has to do less work, and it may also be
>> easy for other human readers to understand the code.  What do you feel?
>>
>
> 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...
>

Also, it's not at all the case that Agda has to do less work if you make
everything
explicit. The reason for that is that Agda is not very trusting of the
user, so if you
write something explicitly that Agda can figure out for itself it needs to
check that
what you wrote is actually the right thing, i.e. it matches what Agda
inferred it ought
to be.

Of course it's not always faster to leave things implicit, but there are
certainly
cases where it will be.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150413/8c2f4da5/attachment.html