[Agda] overloading operations
Guillaume Allais
guillaume.allais at ens-lyon.org
Sun Nov 11 12:42:49 CET 2018
Hi Sergei,
Note that you don't the stdlib to change to be able to use Guillaume's
approach: you can add a layer on top of the stdlib giving a definition
of Semigroup exposing the Carrier and add a generic instance converting
from the stdlib's style to that new style. Self-contained example:
===================================================================
open import Level
open import Algebra
open import Algebra.Structures
open import Algebra.FunctionProperties.Core
open import Relation.Binary
record OverloadedSemigroup {c} (Carrier : Set c) ℓ : Set (c ⊔ suc ℓ) where
infixl 7 _∙_
infix 4 _≈_
field
_≈_ : Rel Carrier ℓ
_∙_ : Op₂ Carrier
isSemigroup : IsSemigroup _≈_ _∙_
instance
OS : ∀ {c ℓ} {{S : Semigroup c ℓ}} →
OverloadedSemigroup (Semigroup.Carrier S) ℓ
OS {{S}} = record { Semigroup S }
import Data.Nat.Properties as NProp
import Data.Integer.Properties as ZProp
instance
*-ℕ : Semigroup _ _
*-ℕ = NProp.*-semigroup
*-ℤ : Semigroup _ _
*-ℤ = record { isSemigroup = ZProp.*-isSemigroup }
open import Data.Integer
open import Relation.Binary.PropositionalEquality
open OverloadedSemigroup {{...}}
abs-homomorphism : (m n : ℤ) → ∣ m ∙ n ∣ ≡ ∣ m ∣ ∙ ∣ n ∣
abs-homomorphism m n = {!!}
===================================================================
Cheers,
--
gallais
On 10/11/18 13:22, Sergei Meshveliani wrote:
> 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
>>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181111/b9e91b88/attachment.sig>
More information about the Agda
mailing list