[Agda] Implicit arguments

[Martin Escardo]

On 12/04/15 20:50, N. Raghavendra wrote:
> When defining a function or a dependent type, I'm often unsure about
> which parameters can be declared as implicit.  

This is not a real answer.

But my rule is this: when doing mathematics, when people use a
subscript (or a superscript, or whatever decoration), and then they
immediately say that they will ommit it when it can be inferred from
the context, we are talking about implicit arguments.

This is not a real answer because I am not telling you how
mathematicians (including computer scientists) decide what should be
left implicit so that their prose is both readable and rigorous.

In fact, a number of mathematicians who favour ultimate rigour do
include all the decorations in their papers, which more often than not
makes them unreadable in my opinion (and annoys me too).

So, no answer for you. But I found that, in practice, Agda both infers
less than people do, and also more. Occasionally, for readability,
I've made an inferable argument explicit. And very often I am also
unhappy that Agda can't infer what is obvious.  But ces't la vie.

So, notice that there are *three* entities involved

 (1) The writer of the Agda code.
 (2) The human reader of the Agda code.
 (3) The automaton reader of the Agda code, the computer.

The choice implicit/explicit is a trade-off between these three
entities.

Pleople who ignore (2) fight more often with (3).

This is perhaps the real rule to avoid fights with (3).

M.


> How do I know whether the
> system can infer a particular argument from the types of other
> arguments?  Until now, I have been just guessing, and it hasn't been
> satisfactory.  Can people describe some method of finding out which
> parameters to assume as implicit?
> 
> Thanks and cheers,
> Raghu.
> 
> --
> N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
> Harish-Chandra Research Institute, http://www.hri.res.in/
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe