[Agda] Semigroup declaration

[Dan Rosén]

Hi Serge,

(1)
    Yes, field identifiers do not need to be unique.

(2)
    Yes, this defines a setoid for every Semigroup.

(2.1)
    On the lines before, you will see that it says
        open IsSemigroup isSemigroup public
    and that brings isEquivalence from IsSemigroup into scope,
    so that is what is on the right side of the equality.

(2.2)
    The other fields can be inferred because of type dependencies.
    It is the same thing here, proj₁ is inferred and does not
    need to be spelled out:

        vector : Vec ⊤ 1
        vector = tt ∷ []

        vector′ : Σ ℕ (Vec ⊤)
        vector′ = record { proj₂ = vector }

(3) If you try this, you will get the error message:
    `The record type Semigroup does not have the fields setoid'
    If you look carefully at the definition of Semigroup, you'll see
    that setoid is not defined under the keyword field. Rather,
    if you have a Semigroup at hand, you can get the setoid of it
    (for instance by opening it).

Cheers,
Dan
On Wed, Aug 29, 2012 at 1:43 PM, Serge D. Mechveliani <mechvel at botik.ru>wrote:

> People,
> I have a couple of a beginner questions on Semigroup in
> Standard library  (Agda-2.3.0.1 + lib-0.6).
>
> The library declares
>
> --------------------------------------------------
> record Setoid c Б└⌠ : Set (suc (c Б┼■ Б└⌠)) where
>   infix 4 _Б┴┬_
>   field
>     Carrier       : Set c
>     _Б┴┬_           : Rel Carrier Б└⌠
>     isEquivalence : IsEquivalence _Б┴┬_
>   ...
> --------------------------------------------------
> record IsSemigroup {a Б└⌠} {A : Set a} (Б┴┬ : Rel A Б└⌠)
>                    (Б┬≥ : OpБ┌┌ A) : Set (a Б┼■ Б└⌠) where
>   open FunctionProperties Б┴┬
>   field
>     isEquivalence : IsEquivalence Б┴┬
>     ...
>   ...
> --------------------------------------------------
> record Semigroup c Б└⌠ : Set (suc (c Б┼■ Б└⌠)) where
>   infixl 7 _Б┬≥_
>   infix  4 _Б┴┬_
>   field
>     Carrier     : Set c
>     _Б┴┬_         : Rel Carrier Б└⌠
>     _Б┬≥_         : OpБ┌┌ Carrier
>     isSemigroup : IsSemigroup _Б┴┬_ _Б┬≥_
>
>   open IsSemigroup isSemigroup public
>   setoid : Setoid _ _
>   setoid = record { isEquivalence = isEquivalence }
> -------------------------------------------------------
>
> And it occurs the following.
> (1) The  setoid  value also has operations named  Carrier and _Б┴┬_
>     -- as in the signature of  Semigroup.
>
> (2) The line  `setoid = record { isEquivalence = isEquivalence }'
>     is an implementation for the operation  setoid.
>
> (2.1) What does it mean this `= isEquivalence' ?
>       Is it  IsSemigroup.isEquivalence  produced by opening
>       IsSemigroup ?
>
> (2.2) This implementation for  setoid  skips the fields of
>       Carrier  and  _Б┴┬_  in Setoid.
> I try an example of
>   record Foo : Set where field f1 : Bool
>                                f2 : Б└∙
>   r : Foo
>   r = record { f1 = true }
>
> And it is not compiled -- until I add a definition for f2.
> How does Standard library manage here to skip the two fields in
> setoid ?
>
> (3) The  setoid  part in Semigroup  must agree with the Semigroup
>     signature values, in particular, to refer to the same
>     Setoid.Carrier  value that  Semigroup.Setoid.
> That is there must hold for each  h : Semigroup
>         Setoid.Carrier $ Semigroup.setoid h = Semigroup.Carrier h
> Right?
> Where is this law specified?
> For example, an user can define erroneousely
> (instead of the Library's):
>   integerSemigroup : Semigroup _ _
>   integerSemigroup = record { Carrier = Integer;
>                               setoid  = record { Carrier = Bool; ... }
>                               ...
>                             }.
> It does not agree with algebra, but Agda will take it (?).
> Am I missing something?
>
> Can you explain, please?
> Thank you in advance,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120829/7bc51e57/attachment.html