[Agda] overloading operations

[Sergei Meshveliani]

On Fri, 2018-11-16 at 09:31 +0100, Guillaume Allais wrote:
> You didn't use `instance` but you declared that the parameters S and S'
> where instance arguments so they were used by the instance resolution.
> This however only works for parameters. Ultimately you probably want
> some concrete instances to be resolved. And that's where your `instance`
> blocks matter.


I am trying to understand the thing by considering examples. 
In the below example, I do not import Semigroup of Standard, instead
declare OSemigroup (after the sample given by Guillaume Brunerie).
(in a real program, I am going to redefine Semigroup as using Carrier as
argument, and Standard semigroup to be possible to imported with
renaming). 

Then, define the instances of OSemigroup for (ℕ, _*_) and for A × B for
the pointwise operation. 
Then,  open OSemigroup {{...}},  and 
  use _∙_ to multiply both natural numbers and pairs of natural numbers,
  use _≈_ both in  2 ∙ 3 ≈ 6  and in  pair ≈ (4 , 6).

If I move  oSemigroup-×  out of the `instance' scope,  then everything
is type-checked, except the last operations with `pair'.

This whole instance usage looks similar to Haskell's. 

Is this a regular instance usage for Agda ?

Thanks,

------
Sergei


-----------------------------------------------------------------
open import Level
open import Algebra.FunctionProperties using (Op₂)
open import Algebra.Structures using (IsSemigroup)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

record OSemigroup {c} (Carrier : Set c) ℓ :  Set (c ⊔ suc ℓ) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    _≈_         : Rel Carrier ℓ
    _∙_         : Op₂ Carrier
    isSemigroup : IsSemigroup _≈_ _∙_


open import Data.Nat using (ℕ; _*_)
import Data.Nat.Properties as NProp
open import Data.Product using (_×_; _,_)
import Data.Product.Relation.Pointwise.NonDependent as PointwisePair

instance
  *oSemigroup-ℕ :  OSemigroup ℕ _
  *oSemigroup-ℕ =  record{ _≈_         = _≡_
                        ; _∙_         = _*_
                        ; isSemigroup = NProp.*-isSemigroup
                        }
  oSemigroup-× : {c ℓ c' ℓ' : Level} {A : Set c} {B : Set c'} →
                OSemigroup A ℓ → OSemigroup B ℓ' → OSemigroup (A × B) _

  oSemigroup-× {c} {ℓ} {c'} {ℓ'} {A} {B} H H' =

    record{ _≈_         =  _≈_
          ; _∙_         =  _∙_
          ; isSemigroup =  A×B-isSemigroup
          }
    where
    open OSemigroup H  using () renaming (_≈_ to _≈₁_; _∙_ to _∙₁_)
    open OSemigroup H' using () renaming (_≈_ to _≈₂_; _∙_ to _∙₂_)

    _≈_ = PointwisePair.Pointwise _≈₁_ _≈₂_

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

    postulate  A×B-isSemigroup :  IsSemigroup _≈_ _∙_

open OSemigroup {{...}}

eq1 : 2 ∙ 3 ≈ 6
eq1 = refl

pair : ℕ × ℕ
pair = (2 , 3) ∙ (2 , 2)

eq2 : pair ≈ (4 , 6)
eq2 = (refl , refl)
--------------------------------------------------------------------




> On 15/11/2018 14:17, Sergei Meshveliani wrote:
> > On Wed, 2018-11-14 at 14:08 +0100, Guillaume Allais wrote:
> >
> >> [..]
> >> `instance` is a bit like instance in Haskell: everything declared in the
> >> block is made available for instance resolution. The difference in Agda
> >> is of course that you can also declare record values *outside* of instance
> >> blocks. They are then *not* used by the automatic instance resolution.
> >> But the user can have access to them like any other value.
> >> [..]
> >
> > For example, I declare 
> >
> >  record Setoid {c} ℓ (Carrier : Set c) :  Set (suc (c ⊔ ℓ))  where
> >      infix 4 _≈_
> >      field
> >        _≈_           : Rel Carrier ℓ
> >        isEquivalence : IsEquivalence _≈_
> >
> > (after the suggestion by Guillaume Brunerie).
> > 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)
> >  
> > The word `instance' is not applied.
> > On the other hand, the two instances for _≈_ are actually resolved.
> >
> > For this particular declaration for Setoid, what possibility is lost by
> > skipping instance declarations?