[Agda] I want implicit coercions in Agda

[Sergei Meshveliani]

On Sat, 2018-11-17 at 16:54 +0000, Peter Hancock wrote:
> On 17/11/2018 15:53, Martin Escardo wrote:
> > If you want mathematicians to use proof assistants, you have to
> > implement the notations they use, not the notations that computer
> > scientists / engineers find convenient to write computer programs.
> > Martin
> 
> You might as well say that if you want mathematicians to use 
> type-setting software you have to implement the notations they use.
> The mathematicians I know seem to find their way pretty well around LaTeX, etc,
> for all its barbarity. 
> 
> Perhaps one can think of mathematical notation as a matter of DSLs.
> LaTeX is full of DSL-like apparatus for things like category theory diagrams, etc.
> I think the support in Agda for equational reasoning might be
> a nice example of a DSL.
> 
> Is there a general definition of coercion?  Is there a connection with identity types? 
> 



> Is changing coordinates from Cartesian to Polar something a coercion might do?


Coercion (if implemented) can do all transformations between all types.
It depends on which coercion instances are declared in a program.
We can set 

  record Coerce {α β} {A : Set α} {B : Set β} :  Set (α ⊔ β) where
         field
           coerce : A → B
  -- 
  -- a general notion of coercion 

and define 

  instance 
    Cartesian→Polar :  Coerce {Cartesian} {Polar} 
    Cartesian→Polar = 
                    record{ coerce = transform } 
                    where
                    transform : Cartesian → Polar
                    transform cart = 
                                   by the known formulae

Having types and classes in a program, and having a set of Coercion
instances in a program, and an expression E : T, 
the type checker needs to solve: what sequence of coercions to apply to
which part in E so that E to have a type T and the operations in E to
agree with the types.  

For example:

    f : Cartesian → Rational 
    f v = (norm v) + (radius v)

v  is a vector represented by a list of rational numbers, and 
(norm v) : Rational.
Suppose that  radius  is an operation of the class related to Polar.
But  v  is not of Polar. 
The type checker sees the coercion instance Cartesian→Polar. It has to
apply it and see whether the result agrees with types.
And the program is converted internally to

    f v =  (norm v) +q (radius v$$Polar),

where  _+q_  is _+_ instanced from implicit to  addition on Rational,
and
v$$Polar =  coerce {Cartesian} {Polar} v.



> Is there a general definition of coercion?  

The above discourse is something like a general definition of coercion.
I expect that coercion solutions are found by some kind of term
unification tactic. There may be many solutions found, and problems ...
Still, I expect, the tool is practicable.

Implicit instance resolution looks like a special case of implicit
coercion resolution.
I think that I need first to try implicit instances, as they are already
given in Agda. 
There my be overlapping instances, and their related problems.
But the programmer always can set enough of explicit things to obtain a
unique resolution.

The problem of powerful implicit instance resolution is difficult for
implementation. But Agda already has a certain resolution.
We need to see what real possibilities does it present, and what
problems it causes.

Regards,

------
Sergei