[Agda] I want implicit coercions in Agda

[Sergei Meshveliani]

On Mon, 2018-11-19 at 04:44 +0000, Peter Hancock wrote:

> [..] 
>
> I presume coercions are injective functions that resolve type-clashes between 
> things like natural numbers and signed integers, or fractions, etc.


Just any function, not only injective. 
Any finite set of such declared in a particular program, similar as with
class instances.
But they can be composed in the process of searching of appropriate
coercion composition.  

For example, in 

       [2] : Z/<3>   -- domain of integers modulo 3
       a   : Z/<3>
       a = (5 + 3) + [2]  

Here the second + is on the domain Z/<3>.  So 5 + 3 -> 8  is expected to
coerce to  [8] : Z/<3>,  and it equals  [2] by taking the remainder by
3, and the whole expression coerces to

       [2] + [2]

> Sergie's gave some examples of using "+", "*" etc to mean different
> operations in different rings.  Is this an example of coercion?
> I'm inclined to call it overloading.  (Which also helps to dispense with 
> pedantic crap.) 

Also the first `+' is on Nat (or may be Integer), and the last `+' is on
Z/<3>. The method of searching for coercion includes searching for
appropriate operation (class) instances. It this example there are found
two instances of Semigroup -- for _+_.

A finite set of coercion declarations is set in the user program.
This is set similar as class instances.

Can it be called overloading? I do not know.

I know the word `coercion' from the materials of the Axiom library for
scientific computation (it started in about 1980).

I think that coercion has an essential part of instance resolution, 
and also specially, for the instances for the class

  record Coerce {α β} {A : Set α} {B : Set β} :  Set (α ⊔ β) where
         constructor coerce
         field
           $$ : A → B

The following example works. This example is contrived.
Suppose that the programmer puts that any  x  _can_ be coerced to 
(x , x),  and any Nat _can_ be coerced to Integer.
And there are also defined instances for some compositions of these
instances:

-------------------------------------------------------------
open import Level           using (_⊔_)
open import Function        using (_∘_; _$_; const)
open import Relation.Binary using (_Preserves_⟶_)
import Relation.Binary.EqReasoning as EqR
open import Data.Product using (_,_; proj₁; Σ)


record Coerce {α β} {A : Set α} {B : Set β} :  Set (α ⊔ β) where
       constructor coerce
       field
         $$ : A → B

open import Data.Nat     using (ℕ)
import Data.Nat.Show as NatShow
open import Data.Integer using (ℤ; +_) renaming (show to showℤ)
open import Data.Product using (_×_; _,_)
open import Data.List    using (List; []; _∷_)

instance
  coerce-ℕ→ℤ :  Coerce {A = ℕ} {B = ℤ}
  coerce-ℕ→ℤ =  coerce +_

  coerceToPair :  ∀ {α} {A : Set α} → Coerce {A = A} {B = A × A}
  coerceToPair =
               coerce (\x → (x , x))

  coerce-ℕ→ℤ×ℤ :  Coerce {A = ℕ} {B = ℤ × ℤ}
  coerce-ℕ→ℤ×ℤ =
               coerce ($$ {A = ℤ} ∘ $$ {B = ℤ})
               where
               open Coerce {{...}}

  open Coerce {{...}}

  f :  List ℤ
  f =  (+ 2) ∷ ($$ 3) ∷ []

  g :  List (ℤ × ℤ)
  g =  $$ 1 ∷  $$ 2 ∷  []

  h :  ℤ × ℤ
  h =  $$ 2   
------------------------------------------------------------------------

Also here                  h = $$ ($$ {B = ℤ} 2)      -- (II)

is resolved by the current Agda, and  

                           h = $$ ($$ 2)              -- (III)
is not.

A real coercion will have to make $$ implicit.
Because in mathematics
                       2 ∷ 3 ∷ []   : List ℤ
can be coerced to       
                       (+ 2) ∷ (+ 3) ∷ []
without showing $$.

May be this can be done as a library written in Agda, via Reflexion
feature, I do not know.

I expect that resolving a coercion for any expression E in a program is
something like finding of an appropriate sequence of class instances to
be composed.
It is needed a flexible way to define a set of coercions, wise options
for searching of a composition.

But I am not sure, I am not a specialist in dependent types resolution. 

I wrote Algebra in Haskell, and used explicit $$ of the Coerce class
(do not recall its name), with defining composition instances. It was
useful.
But Haskell (Glasgow extension of the language) 
can resolve a certain restricted case of _overlapping instances_,
with choosing the instance most special by substitution. 
Though, I think that the feature remains experimental, difficult to
implement, to support. 

But it is already useful for application, it looks like an interesting
field for implementors. And for theory too
(suppose that someone proves that a certain version of the feature is
fundamentally incorrect, etc.).

Regards,

------
Sergei