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

[mechvel at scico.botik.ru]

(Sorry, the topic may look now as of standard library)


On 2020-06-08 17:49, Matthew Daggitt wrote:
> 
>>> 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...


Probably, people would agree that for the standard algebra hierarchy it 
is not
good to allow, for example, for Semiring, different proofs for 
IsEquivalence _≈_
in +-magma and in *-magma. Allowing this would not add anything good 
even for
constructive mathematics.

Please, consider the attached suggestion. It defines the hierarchy part 
from
Setoid to Semiring' (a simplified contrived version for Semiring).

As to me, it looks nice.
And I expect that with this definition, the setoid is the same for 
+-magma
and for *-magma.
Is it?

This is an approach to define Class, SubClasss, SubSubClass ...
where  SubClass has Class as an argument. The scheme is

record Class ...

record IsSubClass (c : Class) (op : Op Carrier) ... where
        field
          <SubClass axioms for  c  and  op>

record SubClass ... where field class      : Class
                                 op         : ...
                                 isSubClass : IsSubClass class op

record IsSubSubClass (sc : SubClass) (op2 : ...) where
        field
          <SubSubClass axioms for  sc  and  op2>

record SubSubClass ... where
        field
          subclass      : SubClass
          op2           : ...
          isSubSubClass : IsSubSubClass subclass op2

and so on.


The argument of the backwards compatibility
-------------------------------------------
does not sound convincing.
Because
a) so far, each new lib version still breaks almost all the user's 
application modules,
b) it is not difficult to port the application to a new version,
c) each application specifies the needed Agda version (and hence the lib 
version),
    install this version and enjoy,
Probably, we need to continue this way until it becomes stable in 
somewhat a natural way.

On the other hand,
------------------
if there are only two setoids in this case (as James wrote),
then, maybe the difficulties are not so great. One sees a report of kind
"additive thing /= multiplicative thing" and guesses to change the place 
to import
setoid from.
I am not sure, subtle difficulties can be hidden there.
In such situations it usually happens that someone invents some horrible 
example.

--
SM




> On Mon, Jun 8, 2020 at 10:42 PM Nils Anders Danielsson <nad at cse.gu.se>
> wrote:
> 
>> On 2020-06-08 14:27, 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
>> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: Structures.agda
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200608/aa193cc9/attachment.ksh>