[Agda] overloading operations

[Guillaume Brunerie]

Oh, nice! It’s much simpler than I thought.

You can use anonymous declarations to get rid of the dummy
identifiers, and you don’t have to write their types.
So the whole instance block can be shortened to

instance
  _ = A
  _ = B

Alternatively, if A and B are instance arguments of the module, then
there is not need for an instance block at all.

Best,
Guillaume
Den ons 14 nov. 2018 kl 16:10 skrev Guillermo Calderon <calderon at fing.edu.uy>:
>
>
> Hi,
>
> This works:
>
> ```
>    ...
>
>    open Setoid   {{...}}
>
>    instance
>      A' : Setoid α α=
>      A' = A
>
>      B' : Setoid β β=
>      B' = B
>
>    C  = Setoid.Carrier A
>    C' = Setoid.Carrier B
>
>    IsCongruent :  (C → C') → Set _
>    IsCongruent f = {x y : C} → x ≈ y → (f x) ≈ (f y)            -- (II)
>
> ```
>
> Unfortunately, I have to introduce dummy identifiers A' and B' in order
> to declare the instances. Perhaps, there exists a way to avoid it.
>
> Regards,
>
> Guillermo
>
>
>
> El 8/11/18 a las 15:16, Sergei Meshveliani escribió:
> > 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
> >
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda