[Agda] Re: Implicit arguments

[N. Raghavendra]

At 2015-04-17T20:12:37+01:00, Martin Escardo wrote:

> 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.

Many thanks for the response!

> 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.

Well, in mathematics, one often uses subscripts, etc., even if they
aren't needed, and available from the context.  E.g., the common
notation M\otimes_A N for the tensor product of two A-modules, where A
is a commutative ring, and Hom_A (M,N) for the A-module of homomorphisms
between the same A-modules.  If S is a multiplicative subset of A, then
for the canonical homomorphism of rings S⁻¹A → A, Bourbaki keeps even S
and A in the notation i_A^S.  Many mathematics books use id_X : X → X or
1_X : X → X, and not just id : X → X for the identity function of a set
X.  The HoTT book uses ind_N (C, c₀, cₛ, n) for induction on natural
numbers, although the family C is superfluous in the notation.

> 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).

I find it good when people take pains to be precise, even if it means
using redundant notation that may seem superfluous.  Perhaps some
redundancy of notation isn't bad.  Certainly, I find Bourbaki extremely
readable.  Likewise, the HoTT book.

Perhaps redundancy of notation is reassuring and useful in informal
mathematics, where the reader has to keep a check on the correctness or
the well-typedness of things.  In Agda, it isn't necessary for the
reader to ensure that things are well-typed, etc., so redundant notation
becomes truly superfluous.  That's why I find implicit arguments a bit
unsettling.

Anyway, I often miss writing id X in Agda for the identity map, and
sometimes, when I am anxious, I even write id {A = X}!  Similarly, when
I write foo refl = refl, I keep thinking it's better to record which
refl {a = x} stands for each of the two refl's.

> 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).

It sure is pragmatic to tailor my thinking to use the machine fully.
When I use implicits next, probably I shouldn't worry too much about my
own memory failing me when I see the code later, and worry even less
about the unlikely readers of my code!

Thanks again for your reply!

Cheers,
Raghu.

--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/