[Agda] overloading operations

[Martín Hötzel Escardó]

Hi Sergei, I have a situation very similar to yours.

An ordinal is a type equipped with a relation _≺_ and a justification 
that it is a well-order. Moreover, this order has an automatically 
derived partial order _≼_.

If α is an ordinal, then I write ⟨ α ⟩ for the underlying type of α and
x ≺⟨ α ⟩ y and x ≼⟨ α ⟩ y for its underlying orders (given and derived).

The notation ⟨_⟩ for the underlying type is defined directly, just as a 
projection.

The notations for the given and derived orders are given by "syntax" 
declarations,

   syntax underlying-order  α x y = x ≺⟨ α ⟩ y
   syntax underlying-porder α x y = x ≼⟨ α ⟩ y

where the underlying things are again projections.

I found that this worked quite well (although it would have been much 
better if Agda could infer the "subscript" α for the orders, given that 
x and y are known to live in the type ⟨ α ⟩).

Here are some examples from
http://www.cs.bham.ac.uk/~mhe/agda-new/OrdinalOfOrdinals.html

is-order-preserving
  is-monotone
  is-order-reflecting
  is-order-embedding
  is-order-equiv
  is-initial-segment
  is-simulation
   : (α : Ordinal U) (β : Ordinal V) → (⟨ α ⟩ → ⟨ β ⟩) → U ⊔ V ̇

is-order-preserving α β f = (x y : ⟨ α ⟩) → x ≺⟨ α ⟩ y → f x ≺⟨ β ⟩ f y

is-monotone α β f         = (x y : ⟨ α ⟩) → x ≼⟨ α ⟩ y → f x ≼⟨ β ⟩ f y

is-order-reflecting α β f = (x y : ⟨ α ⟩) → f x ≺⟨ β ⟩ f y → x ≺⟨ α ⟩ y

...

(Warning: I use U,V,W for type universes rather than "Set i" notation, 
but this is another story. Additionally, U,V,W are "variables", a newly 
introduced feature which is available in the development version only.)

I presume you could define a type "Setoid U" of setoids in the universe 
U with very much the same underlying-type and underlying-equivalence 
notation.

Martin


On 09/11/2018 18:41, mechvel at botik.ru wrote:
> 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
>>>
>>
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
http://www.cs.bham.ac.uk/~mhe