[Agda] overloading operations

[Sergei Meshveliani]

On Sun, 2018-11-11 at 12:42 +0100, Guillaume Allais wrote:
> Hi Sergei,
> 
> Note that you don't the stdlib to change to be able to use Guillaume's
> approach: you can add a layer on top of the stdlib giving a definition
> of Semigroup exposing the Carrier and add a generic instance converting
> from the stdlib's style to that new style. Self-contained example:
> 
> ===================================================================
> open import Level
> open import Algebra
> open import Algebra.Structures
> open import Algebra.FunctionProperties.Core
> open import Relation.Binary
> 
> record OverloadedSemigroup {c} (Carrier : Set c) ℓ : Set (c ⊔ suc ℓ) where
>   infixl 7 _∙_
>   infix  4 _≈_
>   field
>     _≈_         : Rel Carrier ℓ
>     _∙_         : Op₂ Carrier
>     isSemigroup : IsSemigroup _≈_ _∙_
> 
> instance
>   OS : ∀ {c ℓ} {{S : Semigroup c ℓ}} →
>        OverloadedSemigroup (Semigroup.Carrier S) ℓ
>   OS {{S}} = record { Semigroup S }
> 
> import Data.Nat.Properties as NProp
> import Data.Integer.Properties as ZProp
> 
> instance
> 
>   *-ℕ : Semigroup _ _
>   *-ℕ = NProp.*-semigroup
> 
>   *-ℤ : Semigroup _ _
>   *-ℤ = record { isSemigroup = ZProp.*-isSemigroup }
> 
> open import Data.Integer
> open import Relation.Binary.PropositionalEquality
> 
> open OverloadedSemigroup {{...}}
> 
> abs-homomorphism : (m n : ℤ) → ∣ m ∙ n ∣ ≡ ∣ m ∣ ∙ ∣ n ∣
> abs-homomorphism m n = {!!}
> ===================================================================


I thank both Guillaume-s for explanation.

Suppose that one develops a library for operating with fractions and
polynomials in general case. These functions will deal with various
different instances of the structures of  Setoid, Semigroup, Monoid,
Group, ..., Semiring, CommutativeRing -- with different instances of
their declared operations and relations (_≈_, _∙_, _+_; _*_ and such).
Suppose that one needs to use in this library the same name for
different used instances for each of this operations.

I doubt of that this can be be totally supported. 
Also some program fragments are read easier if there are used different
names.

Still let us put that we need to use such an overloading wide enough.
With your suggested approach, one needs to declare the `Overloaded'
version for each of the structures  
Setoid, Semigroup, ..., Semiring, CommutativeRing. 
Then, the library and user programs will be polluted with the prefix
`Overloaded'. I doubt of whether it worth to do this even if it is
abbreviated to a single letter `O'. A mathematician knows the word 
Group, and one will be forced to find out what is OGroup.
I consider re-declaring structures like this:

  record Setoid {c} ℓ (Carrier : Set c) :  Set (suc (c ⊔ ℓ))  where
    infix 4 _≈_
    field
      _≈_           : Rel Carrier ℓ
      isEquivalence : IsEquivalence _≈_

-- after the suggestion by Guillaume Brunerie.
And if the user needs a Standard structure, one renames it to 
Setoid-std, Semigroup-std, and so on.

Overloading for the above Setoid operations works like this:

  open Setoid {{...}}

  module _ {α α= β β=} (C : Set α) (C' : Set β)
                       {{S : Setoid α= C}} {{S' : Setoid β= C'}}
    where
    IsCongruent :  (C → C') → Set _
    IsCongruent f =
                  {x y : C} → x ≈ y → (f x) ≈ (f y)
                                --          --

(1) Can this approach be extended to further generic structures?

Also I do not understand the meaning of the `instance' language
construct.
I know its meaning in Haskell: an instance of a class.
I expect, that theoretically, this corresponds to a pair: a theory and
its model.
Now, Standard library for Agda declares, for example, Setoid
(which somewhat corresponds to some class) and also gives an
implementation for the Setoid instance for Nat (natural numbers) 
-- without setting the word `instance'.
Also it gives an implementation to build the Setoid `pointwise' instance
for List A, from a Setoid instance over the type A -- without setting
the word `instance'.

(2) In the above intended `overloading' library where it will need to 
    appear the `instance' key word?

I thank people in advance for possible explanation.

------
Sergei