[Agda] overloading operations
Sergei Meshveliani
mechvel at botik.ru
Sat Nov 10 13:22:27 CET 2018
Martin, you wrote:
> 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.
In my first reply I have probably confused things about universes.
Now I try once more to understand the idea.
Let us look at the result of this technique. Your demonstration shows
the usage of this technique:
is-order-preserving α β f =
(x y : ⟨ α ⟩) → x ≺⟨ α ⟩ y → f x ≺⟨ β ⟩ f y
But the denotation ≺⟨ α ⟩ and ≺⟨ β ⟩ is not any better than
≺α and ≺β which uses renaming.
Am I missing something?
The goal is overloading. That is this signature needs to be
(x y : ⟨ α ⟩) → x ≺ y → f x ≺ f y (I)
According to the type of f, the first occurrence of ≺ needs to be
recognized by the type checker as on α and the second occurrence of ≺
needs to be recognized as on β.
Agda tends to be considered as an extension of Haskell.
But Haskell allows such overloading (to a certain extent) through the
mechanism of classes and instances. For example, (<), (+), (*).
are declared in Haskell library as certain class members, and are
overloaded like in (I).
I recall difficulties with constant operations and with overlapping
instances, but classes work there, to a certain extent.
Probably, the only remaining hope in Agda is for instance arguments,
something about the ``open ... {{...}}'' denotation.
I try it for Setoid._≈_, Semigroup._∙_, and it does not work.
Guillaume writes that to do this with respect to Standard library
operations, one needs to reorganize Standard library, a bit: to make
Carrier to be an argument to Setoid, and so on.
This means rewriting things in a certain programming style.
Regards,
------
Sergei
> >>
> >>
> >> 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
>
More information about the Agda
mailing list