Hi Serge,<br><br>(1)<br> Yes, field identifiers do not need to be unique.<br><br>(2)<br> Yes, this defines a setoid for every Semigroup.<br><br>(2.1)<br> On the lines before, you will see that it says<br> open IsSemigroup isSemigroup public<br>
and that brings isEquivalence from IsSemigroup into scope,<br> so that is what is on the right side of the equality.<br><br>(2.2)<br> The other fields can be inferred because of type dependencies.<br> It is the same thing here, proj₁ is inferred and does not<br>
need to be spelled out:<br><br> vector : Vec ⊤ 1<br> vector = tt ∷ []<br><br> vector′ : Σ ℕ (Vec ⊤)<br> vector′ = record { proj₂ = vector }<br><br>(3) If you try this, you will get the error message:<br>
`The record type Semigroup does not have the fields setoid'<br> If you look carefully at the definition of Semigroup, you'll see<br> that setoid is not defined under the keyword field. Rather,<br> if you have a Semigroup at hand, you can get the setoid of it<br>
(for instance by opening it).<br><br>Cheers,<br>Dan<br><div class="gmail_quote">On Wed, Aug 29, 2012 at 1:43 PM, Serge D. Mechveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">People,<br>
I have a couple of a beginner questions on Semigroup in<br>
Standard library (Agda-2.3.0.1 + lib-0.6).<br>
<br>
The library declares<br>
<br>
--------------------------------------------------<br>
record Setoid c Б└⌠ : Set (suc (c Б┼■ Б└⌠)) where<br>
infix 4 _Б┴┬_<br>
field<br>
Carrier : Set c<br>
_Б┴┬_ : Rel Carrier Б└⌠<br>
isEquivalence : IsEquivalence _Б┴┬_<br>
...<br>
--------------------------------------------------<br>
record IsSemigroup {a Б└⌠} {A : Set a} (Б┴┬ : Rel A Б└⌠)<br>
(Б┬≥ : OpБ┌┌ A) : Set (a Б┼■ Б└⌠) where<br>
open FunctionProperties Б┴┬<br>
field<br>
isEquivalence : IsEquivalence Б┴┬<br>
...<br>
...<br>
--------------------------------------------------<br>
record Semigroup c Б└⌠ : Set (suc (c Б┼■ Б└⌠)) where<br>
infixl 7 _Б┬≥_<br>
infix 4 _Б┴┬_<br>
field<br>
Carrier : Set c<br>
_Б┴┬_ : Rel Carrier Б└⌠<br>
_Б┬≥_ : OpБ┌┌ Carrier<br>
isSemigroup : IsSemigroup _Б┴┬_ _Б┬≥_<br>
<br>
open IsSemigroup isSemigroup public<br>
setoid : Setoid _ _<br>
setoid = record { isEquivalence = isEquivalence }<br>
-------------------------------------------------------<br>
<br>
And it occurs the following.<br>
(1) The setoid value also has operations named Carrier and _Б┴┬_<br>
-- as in the signature of Semigroup.<br>
<br>
(2) The line `setoid = record { isEquivalence = isEquivalence }'<br>
is an implementation for the operation setoid.<br>
<br>
(2.1) What does it mean this `= isEquivalence' ?<br>
Is it IsSemigroup.isEquivalence produced by opening<br>
IsSemigroup ?<br>
<br>
(2.2) This implementation for setoid skips the fields of<br>
Carrier and _Б┴┬_ in Setoid.<br>
I try an example of<br>
record Foo : Set where field f1 : Bool<br>
f2 : Б└∙<br>
r : Foo<br>
r = record { f1 = true }<br>
<br>
And it is not compiled -- until I add a definition for f2.<br>
How does Standard library manage here to skip the two fields in<br>
setoid ?<br>
<br>
(3) The setoid part in Semigroup must agree with the Semigroup<br>
signature values, in particular, to refer to the same<br>
Setoid.Carrier value that Semigroup.Setoid.<br>
That is there must hold for each h : Semigroup<br>
Setoid.Carrier $ Semigroup.setoid h = Semigroup.Carrier h<br>
Right?<br>
Where is this law specified?<br>
For example, an user can define erroneousely<br>
(instead of the Library's):<br>
integerSemigroup : Semigroup _ _<br>
integerSemigroup = record { Carrier = Integer;<br>
setoid = record { Carrier = Bool; ... }<br>
...<br>
}.<br>
It does not agree with algebra, but Agda will take it (?).<br>
Am I missing something?<br>
<br>
Can you explain, please?<br>
Thank you in advance,<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
</blockquote></div><br>