[Agda] overloading operations

[James Wood]

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.

James

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
> 

-- 
James Wood,
Department of Computer and Information Sciences,
University of Strathclyde.
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.