[Agda] overloading operations

[Guillaume Brunerie]

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)


Best,
Guillaume
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