[Agda] overloading operations

[Guillaume Brunerie]

Den fre 9 nov. 2018 kl 21:44 skrev Sergei Meshveliani <mechvel at botik.ru>:
> 3) Really, will it also support overloading for the operations
>    _∙_, _⁻¹, _+_  in Group, Ring and such structures of Standard
>    library ?

Ideally yes, although I don’t know if anyone actually tried.
There seems to be some of it in agda-prelude (for instance Monoid and
SemiRing), but it seems less developed than the standard library (I
couldn’t find Group or Ring, for instance).

> > [..]
> > >> 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
> > >>>
> > >>
> > >
> > >
> > > _______________________________________________
> > > 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