[Agda] overloading operations

Fri Nov 9 21:28:26 CET 2018

Hi Martin, have you tried with instance arguments?
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