[Agda] Re: Accessing fields of algebra records

[Andrea Vezzosi]

Yeah, the "open public SubRecord subrecord" parts in the definitions
of these records make this much better usable, however it seems the
stdlib doesn't make this easy to discover.

So in the first example you should be able to just write
"CSR.identityˡ", or simply "identityˡ" if you "open CSR".

Cheers,
Andrea

On Tue, Mar 10, 2015 at 1:36 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> On Tue, 2015-03-10 at 12:39 +0530, N. Raghavendra wrote:
>> At 2015-03-10T10:39:20+05:30, N. Raghavendra wrote:
>>
>> > Hi,
>> >
>> > How do I access the inner fields of complex records, e.g., the
>> > multiplicative identity of a commutative semiring?  If I write this:
>> >
>> > 1*n≡n : (n : ℕ) → 1 * n ≡ n
>> > 1*n≡n = CSR.isCommutativeSemiring.*-isCommutativeMonoid.identityˡ
>> >   where
>> >     module CSR = CommutativeSemiring Data.Nat.Properties.commutativeSemiring
>> >
>> > I get an error.
>> >
>> > Thanks and cheers,
>> > Raghu.
>>
>> After looking at the records tutorial, I've found that this works:
>>
>> 1*n≡n : (n : ℕ) → 1 * n ≡ n
>> 1*n≡n = identityˡ
>>   where
>>     open IsCommutativeMonoid
>>       (CommutativeSemiring.*-isCommutativeMonoid NatProp.commutativeSemiring)
>>
>> but don't know whether this is the best way.
>>
>> Cheers,
>> Raghu.
>>
>
> I thought of how to replace with something simpler the things like
>
>   Foo2.op (Foo1.Foo2 struct1) struct2
>
> where Foo1, Foo2 are records.
>
> If the record  Foo1  has   "open Foo2 _ public"
> in the end
> (may be, with adding "hiding" for some itemes), then
>
>      open Foo1 struct1 using (op; ...)
>
> does work. This saves a lot when one has several nested record levels.
>
> For example, extracting  _+_  from  Ring  is by the code following the
> chain
>   R : Ring --> +comGroup : CommutativeGroup --> +group : Group -->
>   +semigroup : Semigroup --> Semigroup._∙_
>
> (I refer to a certain definition of the hierarchy
> Semigroup -- Group -- ...  diferent to the one of Standard library).
>
> This leads to a very large expression. And this is replaced with
>
>   open Semigroup Ring.+semigroup R using () renaming (_∙_ to _+_)
>
> Due to  "open public"  set somewhere in the records, it jumps over the
> levels of CommutativeGroup and Group.
>
> Regards,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda