[Agda] overloading operations

[Sergei Meshveliani]

On Fri, 2018-11-09 at 18:46 +0100, Guillaume Brunerie wrote:
> Hi Sergei,
> 
> Unless I missed something, it does not seem possible to do what you
> want because of the way setoids are set up in the standard library. In
> order for instance arguments to work, you need an IsSetoid type taking
> the carrier type as an argument (rather than a Setoid module having
> the carrier type as a field). Here is how it would work:
> 
> 
> open import Level           using (suc; _⊔_)
> open import Relation.Binary using (Rel; IsEquivalence)
> 
> record IsSetoid {c} ℓ (Carrier : Set c) : Set (suc (c ⊔ ℓ)) where
>   infix 4 _≈_
>   field
>     _≈_           : Rel Carrier ℓ
>     isEquivalence : IsEquivalence _≈_
> 
> open IsSetoid {{...}}
> 
> module _ {α α= β β=} (A : Set α) {{A-setoid : IsSetoid α= A}} (B : Set
> β) {{B-setoid : IsSetoid β= B}}
>   where
> 
>   IsCongruent :  (A → B) → Set _
>   IsCongruent f = {x y : A} → x ≈ y → (f x) ≈ (f y)
> 


Thank you.
Imagine the version  lib-II  of Standard library which defines IsSetoid
this way.
How many changes will this cause in the definitions in the classical
algebra structures: Setoid, Semigroup, Monoid ... CommutativeRing 
?
Will  _∙_ of Semigroup, _⁻¹ of Group, _+_ of Ring, and such, 
become overloadable?

Anybody tried such a library?

Thanks,

------
Sergei



> Den tors 8 nov. 2018 kl 19:16 skrev Sergei Meshveliani <mechvel at botik.ru>:
> >
> > Can anybody, please, explain how to arrange operation overloading
> > (something like classes) ?
> >
> > The first example is
> >
> > ----------------------------------------------------------------
> > open import Level           using (_⊔_)
> > open import Relation.Binary using (Setoid)
> >
> > module _ {α α= β β=} (A : Setoid α α=) (B : Setoid β β=)
> >   where
> >   open Setoid   -- {{...}}
> >
> >   C  = Setoid.Carrier A
> >   C' = Setoid.Carrier B
> >
> >   IsCongruent :  (C → C') → Set _
> >   IsCongruent f =
> >                 {x y : C} → _≈_ A x y → _≈_ B (f x) (f y)    -- (I)
> >
> >              -- {x y : C} → x ≈ y → (f x) ≈ (f y)            -- (II)
> >
> > ----------------------------------------------------------------
> >
> >
> > The line (I) does work.
> > Then I try the line (II), with un-commenting {{...}}.
> > And it is not type-checked.
> > I hoped for that it would find that the first ≈ is on C, while the
> > second ≈ is on C'. But it does not.
> >
> > And real examples are like this:
> >
> > -----------------------------------------------------------------------
> > module _ {α α= β β=} (G : Group α α=) (G' : Group β β=)
> >  where
> >  ...
> >  homomorphismPreservesInversion :
> >    (mHomo : MonoidHomomorphism)
> >    (let f = MonoidHomomorphism.carryMap mHomo) (x : C) →
> >                                                f (x ⁻¹) ≈' (f x) ⁻¹'
> >  homomorphismPreservesInversion
> >                 (monoidHomo ((f , f-cong) , f∙homo) f-preserves-ε) x =
> >    begin≈'
> >      f x'                     ≈'[ ≈'sym (∙ε' fx') ]
> >      fx' ∙' ε'                ≈'[ ∙'cong2 (≈'sym (x∙'x⁻¹ fx)) ]
> >      fx' ∙' (fx ∙' fx ⁻¹')    ≈'[ ≈'sym (≈'assoc fx' fx (fx ⁻¹')) ]
> >      (fx' ∙' fx) ∙' fx ⁻¹'    ≈'[ ∙'cong1 (≈'sym (f∙homo x' x)) ]
> >      f (x' ∙ x) ∙' fx ⁻¹'     ≈'[ ∙'cong1 (f-cong (x⁻¹∙x x)) ]
> >      f ε ∙' fx ⁻¹'            ≈'[ ∙'cong1 f-preserves-ε ]
> >      ε' ∙' fx ⁻¹'             ≈'[ ε'∙ (fx ⁻¹') ]
> >      (f x) ⁻¹'
> >    end≈'
> >    where
> >    x' = x ⁻¹;   fx = f x;   fx' = f x'
> > ----------------------------------------------------------------------
> >
> > Here the carriers of G and G' are C and C',
> > ≈ is on C,  ≈' is on C' (by renaming),
> > _∙_ on C, _∙'_ on C',
> > ε is of G, ε' of G',
> > _⁻¹ is of G,  _⁻¹' of G',
> > and so on.
> >
> > It is desirable to make the code more readable by canceling some of the
> > above renaming. For example, to replace ε' with ε and _∙'_ with _∙_.
> > Is it possible to do this by using something like
> > open Group {{...}}
> > ?
> >
> > Thanks,
> >
> > ------
> > Sergei
> >
> >
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>