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

[James Wood]

Hi,

I fix an instance of this kind of issue in my definition of module-like
structures. The code is somewhere around
https://agda.github.io/agda-stdlib/Algebra.Module.Structures.html#4428 .

An R-S-bimodule is a commutative monoid over which we have a left
R-module and a right S-module which are compatible with each other. If
we formalise just that, we end up requiring two proofs of
`IsCommutativeMonoid` – one from the left and one from the right. To
avoid that, I had to introduce notions of left R-module and right
S-module lacking `IsCommutativeMonoid` proofs (`IsPreleftSemimodule`,
`IsPrerightSemimodule`), to allow for the possibility of sharing when we
have multiple. Another approach would be to parametrise over the
`IsCommutativeMonoid` proof, as Matthew suggested.

Ideally, we would have language support for this kind of sharing in
hierarchies, but as it is, I don't think I can recommend any refactoring
to stdlib's main algebraic hierarchy. To do for `IsEquivalence` what I
did for `IsCommutativeMonoid` would require a lot of new definitions,
and probably refactorings just to get around having so many new
definitions. It also probably would break nearly all code defining an
instance of an algebraic structure, though a fix would not be too hard
to apply in each case.

Regards,
James

On 08/06/2020 15:49, Matthew Daggitt wrote:
> Apologies, I didn't send this to the list when I replied the first time
> round.
> 
>     Hi Sergei,
> 
>      
> 
>         There are many paths in it which lead to the same Setoid.
> 
>      
> 
>     Unfortunately this is not true. The `Setoid`s from `+-magma` and
>     `*-magma` in your examples are different setoids. They have the same
>     binary equality relation, but the proof of `isEquivalence` may
>     differ and therefore Agda does not consider them identical. 
>     This is not a problem with Agda, but with how the record hierarchy
>     is designed. I'm not sure there is a good solution for the problem,
>     short of parameterising every record in the hierarchy by a `Setoid`.
>     However that brings its own set of problems...
>     Best,
>     Matthew
> 
> 
> 
> On Mon, Jun 8, 2020 at 10:42 PM Nils Anders Danielsson <nad at cse.gu.se
> <mailto:nad at cse.gu.se>> wrote:
> 
>     On 2020-06-08 14:27, mechvel at scico.botik.ru
>     <mailto:mechvel at scico.botik.ru> wrote:
>     > 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.
>     > ?
> 
>     I have not checked the example very carefully, but I don't think that
>     the two setoids are necessarily equal: they might have distinct proofs
>     of (say) transitivity. Perhaps it would make sense to change the library
>     so that the two setoids are equal (or to stop using setoids).
> 
>     -- 
>     /NAD
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C0cbff6bde77d407c655308d80bbb3d5f%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637272246536645255&sdata=QztLn3zW3%2BPfLUPIqb4%2FDL5EcrTx12X8Cp4oZc4qvs0%3D&reserved=0>
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C0cbff6bde77d407c655308d80bbb3d5f%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637272246536665246&sdata=eaJYr%2B7gSf2KY3GLv4q3hU%2FvxO%2FoI6YCzq7Iksyif%2FM%3D&reserved=0
>