[Agda] many ways to import the same thing from record

[mechvel at scico.botik.ru]

mechvel at scico.botik.ru писал 2020-06-06 23:32:
> Can anybody, please, explain something concerning the _attached code_?
> 


Here is a reduced example (zip is attached, for any occasion):


-------------------------------------------------------------------
record Subsetoid α α= p (S : Setoid α α=) :  Set (α ⊔ α= ⊔ suc p)
   where
   field  member : (Setoid.Carrier S) → Set p

record Submagma α α= p (magma : Magma α α=) :  Set (α ⊔ α= ⊔ suc p)
   where
   field  subsetoid : Subsetoid α α= p (Magma.setoid magma)

module _ {α α=} (R : Semiring α α=)
   where
   open Semiring R using (0#; +-magma; *-magma)

   open Magma +-magma using (setoid)     -- I
   -- open Magma *-magma using (setoid)  -- II

   open Setoid setoid using (_≉_)

   nzSubsetoid : Subsetoid α α= α= setoid
   nzSubsetoid = record{ member = (_≉ 0#) }

   submagma : Submagma α α= α= *-magma
   submagma = record{ subsetoid = nzSubsetoid }
----------------------------------------------------------------------

Agda-2.6.1 reports an error
"
.......*-isMonoid /=
.......+-isCommutativeMonoid
"
After switching the comment from line II to line I, it is type-checked.

Why Agda makes difference between (Magma.setoid +-magma)
and (Magma.setoid *-magma) ?

There is a tree made by import steps, with the root in Semiring.
There are many paths in it which lead to the same Setoid.
Probably the type checker evaluates all these paths to the same tree 
node
presenting this setoid.
Because in a Semiring, +-magma and *-magma share the setoid.
?

Thank you in advance for explanation.

------
Sergei



The effect is that the same setoid can be imported in many ways from
> Semiring, and by even more ways from CommutativeRing, and so on.
> And in some programs the type checker is satisfied only with one of
> such ways.
> 
> This relates both to Agda programming in general and to standard 
> library.
> 
> The example implements a part of a proof for the statement:
> for a  Semiring  having the property
> ``nz*nz : ∀ {x y} → x ≉ 0# → y ≉ 0# → (x * y) ≉ 0#``
> (call it  FooSemiring)
> it holds that the  subset of nonzero elements  is a Magma, if the `_∙_`
> operation is put the restriction of `_*_` to Nonzero.
> 
> The code defines the notions of Subset and Submagma,
> and tries to form a Submagma for Nonzero in any FooSemiring.
> But Agda-2.6.1 reports
> 
>   Algebra.IsSemiringWithoutAnnihilatingZero.*-isMonoid /=
>   Algebra.IsSemiringWithoutAnnihilatingZero.+-isCommutativeMonoid
>   when checking that the expression nzSubsetoid has type
>   Subsetoid α α= α= (Magma.setoid *-magma)
> 
> It is about the last two lines
> ```
>  nzSubmagma : Submagma α α= α= *-magma
>  nzSubmagma = submagmaᶜ nzSubsetoid closed*
> ```
> I have an impression that it happens the following.
> nzSubsetoid  is formed for the base `setoid` imported form FooSemiring,
> and this setoid is extracted from `Semiring.+-monoid`
> - probably this is put so in lib-1.3, by occasion.
> But it could as well extract it from `Semiring.*-monoid`.
> 
> Further, the Submagma record has `magma` as argument, and in the
> definition of Submagma, `setoid` is exracted from this `magma`.
> And the argument in the type of  nzSubmagma  is set `Semiring.*-magma`,
> because it aims at the multiplicative magma of a Semiring.
> 
> Mathematically, `+-magma` and `*-magma` of (Semiring R) have the same 
> setoid
> inside.
> Does Agda refer to these setoids somehow with the same reference?
> 
> Probably, in my program, the type checker does not identify these 
> setoids.
> To check this, I split this setoid import to the two steps:
> ```
>  open FooSemiring R using (Carrier; ...; *-magma)
>  open Magma *-magma using (setoid)
> ```
> instead of importing is directly from FooSemiring.
> Now Agda is satisfied.
> 
> Something is suspicious here.
> As there are many levels in the record hierarchy for algebra in
> standard library, it occurs that the same thing can be imported
> from the top domain by hundreds of ways. And for almost all of these
> ways, the type checker will report an error - for some programs.
> This presents a problem.
> Because it is easier to import everything needed by a single `open` 
> declaration
> for the top record rather than to search for a lucky chain of imports.
> May be, this is due to a bug in Agda?
> I do not know how standard library can help here.
> 
> Am I missing something?
> 
> Thanks,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Test.agda.zip
Type: application/zip
Size: 524 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200608/fd2f4325/attachment.zip>