[Agda] I want implicit coercions in Agda

[Sergei Meshveliani]

On Sat, 2018-11-17 at 00:23 +0000, Miëtek Bak wrote:
> Martin Odersky is proposing to get rid of implicits in Scala 3.  
> I would like to draw your attention to the following quote:
> 
> “… most applications of implicit conversions have turned out to be of dubious value. 
> The problem is that many newcomers to the language start with defining
> implicit conversions since they are easy to understand and seem 
> powerful and convenient. … But the problem remains that syntactically,
> conversions and values just look too similar for comfort.”
>
> https://github.com/lampepfl/dotty/pull/5458
> 
> Personally, I found implicit conversions greatly increase the difficulty of understanding 
> other people’s code, and I would be happier if they did not make 
> their way into Agda.
> 

Consider the two examples.

Example I. 
Defining multiplication in the direct product of two semigroups

    _∙_ : Op₂ (A × B)
    (x , y) ∙ (x' , y') =  (x ∙₁ x' , y ∙₂ y')     --(I.1)

                           -- (x ∙ x' , y ∙ y')    --(I.2)

Do the subscripts in ∙₁, ∙₂ make the program (I.1) easier to
read/understand than (I.2) ?  Is implicit conversion desirable here?
I doubt.

Example II. 
 homomorphismPreservesInversion
                (monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
   begin≈'
     f x'                     ≈'[ ≈'sym (∙ε' fx') ]
     fx' ∙' ε'                ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
     fx' ∙' (fx ∙' fx ⁻¹')    ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
     (fx' ∙' fx) ∙' fx ⁻¹'    ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
     f (x' ∙ x) ∙' fx ⁻¹'     ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
     f ε ∙' fx ⁻¹'            ≈'[ ∙'cong1 f-preserves-ε ]
     ε' ∙' fx ⁻¹'             ≈'[ ε'∙ (fx ⁻¹') ]
     (f x) ⁻¹'
   end≈'
   where
   x' = x ⁻¹;   fx = f x;   fx' = f x'

Here the carriers of G and G' are C and C',
≈ is on C,  ≈' is on C' (by renaming),  
_∙_ on C, _∙'_ on C',
ε is of G, ε' of G',  
_⁻¹ is of G,  _⁻¹' of G',
and so on.

It is desirable to make the code more readable by canceling some of the
above renaming. For example, to replace ε' with ε and _∙'_ with _∙_
-- at least in the right hand column.

Another point
-------------
In textbooks on mathematics they most often write things like

                    f(x+y) = f(x) + f(y) 

(the definition of  f : A -> B  being a homomorphism)
with `+' defined on two different domains.
Also they write
                    [m] * [n]  =def  [m * n]

as a definition for the product of residues, where  [k]  denotes the
residue class of an integer  k  modulo some  p. 

There are many other examples.

Generally, we need to respect mathematical style. 
It is based on experience of many centuries. 
Most of the mathematical community really understands which book is
easier to read. 
I tend to trust this approach more.

But there is a fashion for denotation in science, and it changes. 
But the implicit conversion style remains stable. I think this will
remain.

Similarly as a reader understands implicit conversion in a mathematical
book, a compiler and a reader of a program need to understand implicit
conversion in a program.

On the other hand, programs have more difficulties with implicit
conversion than mathematical texts. 
I observe this on my experience with Haskell and Agda.
For example, several years ago I was stuck with about 500 times slow
down in type checking in my program due to a single usage of "open Foo
{{...}}".

May be, the reason for this is that compilers are not enough wise, it 
needs a great effort to make them wiser.

I think that 
a) compilers need to understand implicit conversion as much as possible,
   and future compilers will do this, 
b) a programmer has to choose wisely where to apply implicit conversion,
c) for each compiler system being developed there is a priority in 
   developing features, for example, I cannot advise about the priority 
   of implicit conversion in the Agda type checker, let the Agda team
   decide.

Regards,

------
Sergei