[Agda] overloading operations

[Sergei Meshveliani]

On Fri, 2018-11-09 at 17:28 +0000, James Wood wrote:
> Agda doesn't do overloading for anything other than constructors, but
> there are still tricks you can use. One I use a lot is making a local
> module definition just to make a quick namespace, and then use dot
> notation to access the contents of that module. In your example, it
> would look like this:
> 
>   module A = Setoid A
>   module B = Setoid B
> 
>   IsCongruent :  (A.Carrier → B.Carrier) → Set _
>   IsCongruent f =  {x y} → x A.≈ y → (f x) B.≈ (f y)
> 
> Perhaps not ideal, but I've found it okay.


Thank you.
Currently I also use such in my example:  P'.∙ε, P'.x∙x⁻¹, P'.∙cong2.

But it is essentially worse than   ∙ε, x∙x⁻¹, ∙cong2.

I also have a renaming of  ≈',  which looks better than  A.≈,
Also  ≈  can be renamed to  ≈A, which looks better than  A.≈.
And all them are worse than ≈.

--
SM


> 
> On 08/11/18 18:16, Sergei Meshveliani wrote:
> > 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
> > 
>