[Agda] I want implicit coercions in Agda

[Guillaume Brunerie]

It seems like there are non-trivial interactions between implicit
coercions and instance arguments.
For instance if you have an implicit coercion inj : N -> Q, and n m :
N, then what is n + m : Q supposed to mean?
Is it inj (n +_N m) or is it (inj n) +_Q (inj m) ?
Of course in that case they are both (propositionally) equal, that’s
why a mathematician is happy with it, but which one should Agda
choose?

Best,
Guillaume
Den mån 19 nov. 2018 kl 19:44 skrev Sergei Meshveliani <mechvel at botik.ru>:
>
> On Sun, 2018-11-18 at 21:35 +0100, Ulf Norell wrote:
>
> > [..]
> >  To move this discussion forward I suggest that you give some of the
> > following:
> >
> >
> > - concrete examples of implicit coercions that you'd like to see
> > - a rough sketch of how they are to be solved
> > - references to the proof assistants that (in your opinion) have
> > gotten implicit coercions right
> > - some notes on why instance arguments are not a good replacement for
> > implicit coercions
>
>
> 1. Examples are given in the book about a library for computer algebra
>    "Axiom. 30 years horizon",
>    Chapter 2.7:  coercion, conversion ... There are given examples.
>    It is on the Web.
>
> 2. Nicolas J. Doye.
> Automated coercion for axiom.  ACM journal, 1999.
> It is on the Web.
>
> This paper looks like a foundation for an algorithm to find coercion.
> I never tried to understand it.
>
> 3. May be, algebraic libraries in Coq develop coercion.
>
>
>
> > some notes on why instance arguments are not a good replacement for
> > implicit coercions
>
>
> Suppose that Rational is represented as  n /' d,  n, d : Integer
> (let us forget here of d /= 0).
> Consider
>             a :  Rational
>             a =  2 + (1 /' 2)            -- (E)
>
> To which types each part of (E) needs to be mapped, and how,
> so that to obtain a valid expression of type Rational
> to be type-checked?
>
> By implicit instances, _+_ can be resolved to _+r_ -- addition on
> rational numbers.
> But Agda will report an error, because
>
>    2  is not in Rational,  1 and 2 are not in Integer.
>
> Some method needs to guess how to coerce (E) to the subsumed expression
>
>             ((+ 2) /' 1)  +  ((+ 1) /' (+ 2))
>
> And the rest is by instance resolution for _+_.
> Here 2 first transforms to  (+ 2),  and then to  (+ 2) /' (+ 1).
>
> Mathematicians and engineers write (E) with subsuming this coercion.
>
> The basic coercions are declared and defined in the user program.
> For Agda, they can be set, say, as instances of the Coerce class,
> why not?
>
> In this example, basic coercions are
>    n : Nat      ->  (+ n)       : Integer,
>    x : Integer  ->  x /' (+ 1)  : Rational.
>
> The solver needs to find a chain of basic coercions that satisfy the
> goal type and also is type-checked.
>
> Can implicit instances for _+_ be set so that the current Agda to
> type-check (E) ?
> I think, they cannot. So that implicit instance arguments do not cover
> coercion.
> Am I missing something?
>
> Regards,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda