[Agda] overloading operations

Martin Escardo m.escardo at cs.bham.ac.uk
Fri Nov 9 22:51:55 CET 2018



On 09/11/2018 20:28, guillaume.brunerie at gmail.com wrote:
> Hi Martin, have you tried with instance arguments?

Thanks! I will try your suggestion below and if it works well with the 
whole development (27k lines, 100 files) I may adopt it.

Martin

> Here is a self-contained example, based on your code, showing how to get
> 
> is-order-preserving α β f = (x y : ⟨ α ⟩) → x ≺ y → f x ≺ f y
> 
> The main changes are that I define Ordinal using a special Σ-type
> where the second field is an instance field, and then _≺_ takes the
> ordinal structure as an instance argument.
> 
> 
> open import Agda.Primitive public
>    using (_⊔_)
>    renaming (lzero to U₀
>            ; lsuc to _⁺
>            ; Level to Universe
>            ; Setω to Uω
>            )
> 
> variable
>   U V W U' V' W' : Universe
> 
> _̇ : (U : Universe) → _
> U ̇ = Set U
> 
> record Σ {U V} {X : U ̇} (Y : X → V ̇) : (U ⊔ V) ̇ where
>    constructor _,_
>    field
>     pr₁ : X
>     pr₂ : Y pr₁
> 
> open Σ public
> 
> infixr 4 _,_
> 
> postulate
>    is-well-order : {U V : Universe}
>                    {X : U ̇}
>                    (_<_ : X → X → V ̇) → (U ⊔ V) ̇
> 
> OrdinalStructure : U ̇ → U ⁺ ̇
> OrdinalStructure {U} X = Σ \(_<_ : X → X → U ̇) → is-well-order _<_
> 
> {- A Σ-type where the second field is an instance argument -}
> record Σ⦃⦄ {U V} {X : U ̇} (Y : X → V ̇) : (U ⊔ V) ̇ where
>    constructor σ
>    field
>     pr₁ : X
>     {{pr₂}} : Y pr₁
> 
> Ordinal : ∀ U → U ⁺ ̇
> Ordinal U = Σ⦃⦄ \(X : U ̇) → OrdinalStructure X
> 
> ⟨_⟩ : Ordinal U → U ̇
> ⟨ σ X ⟩ = X
> 
> _≺_ : {X : U ̇} {{_ : OrdinalStructure X}} → X → X → U ̇
> _≺_ {{_<_ , o}} = _<_
> 
> is-order-preserving : (α : Ordinal U) (β : Ordinal V) → (⟨ α ⟩ → ⟨ β
> ⟩) → (U ⊔ V) ̇
> is-order-preserving α β f = (x y : ⟨ α ⟩) → x ≺ y → f x ≺ f y
> Den fre 9 nov. 2018 kl 20:49 skrev Martín Hötzel Escardó
> <m.escardo at cs.bham.ac.uk>:
>>
>> 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
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda

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


More information about the Agda mailing list