[Agda] overloading operations
Guillermo Calderon
calderon at fing.edu.uy
Fri Nov 16 21:46:38 CET 2018
El 16/11/18 a las 15:21, Sergei Meshveliani escribió:
> On Fri, 2018-11-16 at 09:31 +0100, Guillaume Allais wrote:
>> You didn't use `instance` but you declared that the parameters S and S'
>> where instance arguments so they were used by the instance resolution.
>> This however only works for parameters. Ultimately you probably want
>> some concrete instances to be resolved. And that's where your `instance`
>> blocks matter.
>
>
> I am trying to understand the thing by considering examples.
> In the below example, I do not import Semigroup of Standard, instead
> declare OSemigroup (after the sample given by Guillaume Brunerie).
> (in a real program, I am going to redefine Semigroup as using Carrier as
> argument, and Standard semigroup to be possible to imported with
> renaming).
>
Actually, it is not necessary to declare the carrier as a parameter of
the record to work with instances, overloading and this stuff.
See my post bellow in this thread and the next mesage of Guillaume.
> Then, define the instances of OSemigroup for (ℕ, _*_) and for A × B for
> the pointwise operation.
> Then, open OSemigroup {{...}}, and
> use _∙_ to multiply both natural numbers and pairs of natural numbers,
> use _≈_ both in 2 ∙ 3 ≈ 6 and in pair ≈ (4 , 6).
>
> If I move oSemigroup-× out of the `instance' scope, then everything
> is type-checked, except the last operations with `pair'.
>
> This whole instance usage looks similar to Haskell's.
>
> Is this a regular instance usage for Agda ?
>
> Thanks,
>
> ------
> Sergei
>
>
> -----------------------------------------------------------------
> open import Level
> open import Algebra.FunctionProperties using (Op₂)
> open import Algebra.Structures using (IsSemigroup)
> open import Relation.Binary
> open import Relation.Binary.PropositionalEquality using (_≡_; refl)
>
> record OSemigroup {c} (Carrier : Set c) ℓ : Set (c ⊔ suc ℓ) where
> infixl 7 _∙_
> infix 4 _≈_
> field
> _≈_ : Rel Carrier ℓ
> _∙_ : Op₂ Carrier
> isSemigroup : IsSemigroup _≈_ _∙_
>
>
> open import Data.Nat using (ℕ; _*_)
> import Data.Nat.Properties as NProp
> open import Data.Product using (_×_; _,_)
> import Data.Product.Relation.Pointwise.NonDependent as PointwisePair
>
> instance
> *oSemigroup-ℕ : OSemigroup ℕ _
> *oSemigroup-ℕ = record{ _≈_ = _≡_
> ; _∙_ = _*_
> ; isSemigroup = NProp.*-isSemigroup
> }
> oSemigroup-× : {c ℓ c' ℓ' : Level} {A : Set c} {B : Set c'} →
> OSemigroup A ℓ → OSemigroup B ℓ' → OSemigroup (A × B) _
>
> oSemigroup-× {c} {ℓ} {c'} {ℓ'} {A} {B} H H' =
>
> record{ _≈_ = _≈_
> ; _∙_ = _∙_
> ; isSemigroup = A×B-isSemigroup
> }
> where
> open OSemigroup H using () renaming (_≈_ to _≈₁_; _∙_ to _∙₁_)
> open OSemigroup H' using () renaming (_≈_ to _≈₂_; _∙_ to _∙₂_)
>
> _≈_ = PointwisePair.Pointwise _≈₁_ _≈₂_
>
> _∙_ : Op₂ (A × B)
> (x , y) ∙ (x' , y') = (x ∙₁ x' , y ∙₂ y')
>
> postulate A×B-isSemigroup : IsSemigroup _≈_ _∙_
>
> open OSemigroup {{...}}
>
> eq1 : 2 ∙ 3 ≈ 6
> eq1 = refl
>
> pair : ℕ × ℕ
> pair = (2 , 3) ∙ (2 , 2)
>
> eq2 : pair ≈ (4 , 6)
> eq2 = (refl , refl)
> --------------------------------------------------------------------
>
>
>
>
>> On 15/11/2018 14:17, Sergei Meshveliani wrote:
>>> On Wed, 2018-11-14 at 14:08 +0100, Guillaume Allais wrote:
>>>
>>>> [..]
>>>> `instance` is a bit like instance in Haskell: everything declared in the
>>>> block is made available for instance resolution. The difference in Agda
>>>> is of course that you can also declare record values *outside* of instance
>>>> blocks. They are then *not* used by the automatic instance resolution.
>>>> But the user can have access to them like any other value.
>>>> [..]
>>>
>>> For example, I declare
>>>
>>> record Setoid {c} ℓ (Carrier : Set c) : Set (suc (c ⊔ ℓ)) where
>>> infix 4 _≈_
>>> field
>>> _≈_ : Rel Carrier ℓ
>>> isEquivalence : IsEquivalence _≈_
>>>
>>> (after the suggestion by Guillaume Brunerie).
>>> Overloading for the above Setoid operations works like this:
>>>
>>> open Setoid {{...}}
>>>
>>> module _ {α α= β β=} (C : Set α) (C' : Set β)
>>> {{S : Setoid α= C}} {{S' : Setoid β= C'}}
>>> where
>>> IsCongruent : (C → C') → Set _
>>> IsCongruent f =
>>> {x y : C} → x ≈ y → (f x) ≈ (f y)
>>>
>>> The word `instance' is not applied.
>>> On the other hand, the two instances for _≈_ are actually resolved.
>>>
>>> For this particular declaration for Setoid, what possibility is lost by
>>> skipping instance declarations?
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
More information about the Agda
mailing list