[Agda] overloading operations

[Guillaume Allais]

You don't need to add the prefix `Overloaded` anywhere: you can merely
import `Algebra` (without opening it) and give your new structures the
same names as the ones in the standard library. You can then refer to the
ones in `Algebra` by using qualified names e.g. `Algebra.Monoid`.

`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.

By default the standard library does not declare anything as an `instance`.
If you want resolution to use some of the structures made available in the
stdlib, you will need to put all of these into an instance block like I did
in my example for Nat and Integer.

Cheers,
--
gallais


On 12/11/2018 19:05, Sergei Meshveliani wrote:
> 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
>


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181114/db8e881c/attachment.sig>