[Agda] overloading operations

[Guillaume Allais]

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.

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?
>
> Thanks,
>
> ------
> Sergei
>
>


-------------- 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/20181116/0990b255/attachment.sig>