[Agda] overloading operations

[Guillermo Calderon]

El 16/11/18 a las 15:21, Sergei Meshveliani escribió:
> 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).
> 

Actually, it is not necessary to declare the carrier as a parameter of 
the record to work with instances, overloading and this stuff.

See my post bellow in this thread and the next mesage of Guillaume.



> 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?
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>