[Agda] Re: Accessing fields of algebra records

[Sergei Meshveliani]

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