In CommutativeRing, Ring.semiring ≠ CommutativeSemiring.semiring

[laMudri]

In the algebra hierarchy, we naturally have this diamond.

         CommutativeRing (CR)
        /                    \
Ring (R)                      CommutativeSemiring (CSR)
        \                    /
            Semiring (SR)

I shall abbreviate these CR, R, CSR, and SR.

In the standard library, the SR instance for CR comes from the CSR instance. CSR uses the commutativity property to cut down the number of fields of CSR, so we only have fields distribʳ and zeroˡ, and the versions on the opposite side follow by commutativity. Via R, this is not a possibility because of the lack of commutativity, so there are full distrib and zero fields.

This is causing trouble here. The required isRightSemimodule field is of type IsRightSemimodule (Ring.semiring ring) m ℓm, but the natural isRightSemimodule definition to export is of type IsRightSemimodule (CommutativeSemiring.semiring commutativeSemiring) m ℓm, because CommutativeRing.semiring = CommutativeSemiring.semiring ∘ CommutativeRing.commutativeSemiring. These types are not definitionally equal.

I don't understand how conflicts like this are handled further down in the hierarchy (like at AbelianGroup), but maybe that approach could be replicated successfully. My personal preference would be that the main structures in the hierarchy are unabbreviated, containing redundant lemmas, and we then have smart constructors to avoid explicit redundant proofs. Then, we would get hierarchies like this:

             Ring...
                |
            /---/
            |
            |      /== AbelianGroupˡ
      AbelianGroup === AbelianGroupʳ
     /            \
Group              CommutativeMonoid === CommutativeMonoidˡ (has identityˡ)
     \            /                  \== CommutativeMonoidʳ (has identityʳ)
         Monoid

The === are where smart constructors go from the abbreviated structure (like CommutativeMonoidˡ) to the canonical structure in the hierarchy. Abbreviated structures play no part in the hierarchy, and should not be used except from in the smart constructor.

[MatthewDaggitt]

Hmm I really like this proposal. It's always bugged me (#239) that sometimes the records don't inherit the way you think they should. This seems like a really neat way of side-stepping the problem and although not backwards compatible requires only a very minimal change to existing code (i.e. prepend the smart constructor in front of the record construction).

I don't understand how conflicts like this are handled further down in the hierarchy (like at AbelianGroup)

So I think the reason that you're running into this problem for modules is that for the first time you're breaking the pattern by parameterising "structures" with "packages" which isn't done anywhere else in the library. The "packages" don't compose in the same way that you're trying to make your "structures" compose and hence you run into the sort of conflicts above. I might add a comment on the PR discussing this.

[JacquesCarette]

This is nice - but I wouldn't spend too much effort on it. When you have ~30 structures in your Algebra library, there's a limited number of natural diamonds that occur. When you get to ~300, there are way, way more of them, and this kind of patch is not sufficient anymore. I'm not quite ready to make a concrete proposal about an alternate way to handle things; in the meantime, what is proposed here is definitely better than the status quo.

[laMudri]

I thought it'd be worth summarising this comment here.

Definitely things to do

Algebra.Structures

There are basically two hierarchies living in this file. One is the monoid-group-ring sequence, capturing quantity-like structures. The other is band-semilattice-bounded semilattice-lattice sequence, capturing an algebraic version of orders with meets and/or joins.

The ring sequence is being redone in #985.

The lattice sequence needs to be redone heavily. It also contains some errors of nomenclature (IsBoundedLattice is really about bounded semilattices) and conspicuous holes (actual bounded lattices). I think it would be best to extract this sequence out into an Algebra.Lattice module hierarchy, or something like this. This would let us deprecate everything broken in the Algebra hierarchy and largely start from scratch.

Relation.Binary.Structures

The only thing worth reviewing is IsStrictTotalOrder. Being based on a strict order rather than a non-strict order, the only relevant weaker definition hierarchically is IsStrictPartialOrder. However, instead of inheriting from there, IsStrictTotalOrder derives irreflexivity and respecting of equality from the compare field. This is based around the Tri type family, where Tri A B C says that exactly 1 of A, B, and C is true, and the other two are false. It'd be interesting to know how people find programming with this to be, given that it looks a bit awkward. Possibly a good refactoring would be to just have a ternary coproduct of x < y, x ≈ y, and x > y, and have this be part of the default definition of IsStrictTotalOrder. Then, the current stuff can be converted into that like we do with biased structures. While we're at it, maybe strict orders should be put in a Relation.Binary.Strict module hierarchy.

Possibly things to do

Relation.Binary.Lattice

This module builds up a hierarchy of lattice-like structures from an order-theoretic perspective. It builds up from the Relation.Binary hierarchy. There are several potential problems:

• IsDistributiveLattice has a ∧-distribˡ-∨ field, rather than an unbiased ∧-distrib-∨ field. This is not an immediate problem, because the order-theoretic lattice hierarchy contains no notion of non-commutative meet/join. However, it may be a problem when interfacing with the algebraic lattice hierarchy, though I haven't thought this through. In any case, it should be possible to build a distributive lattice from ∧-distribʳ-∨ alone, too.
• IsDistributiveLattice also should have a dual member ∨-distrib-∧, at least as a proof if not a field. Again, it should be possible to build a distributive lattice by proving this rather than ∧-distrib-∨.
• IsBooleanAlgebra insists that the internal hom _⇨_ be defined in terms of ¬_ and _∨_. I imagine this causes trouble for instances such as the universe of decidable types, where the internal hom should be based on the function arrow to maintain compatibility with the universe of all types. I'm not sure what axioms to enforce to rectify things, though.

Algebra.Morphism

This file appears to be on its way to deprecation, but is currently the most complete collection of algebraic morphism definitions. If all of these definitions are ported over to Algebra.Morphism.Structures, similar problems to what already exist will arise.

The only potential problem I see is in IsGroupMorphism, which has ⁻¹-homo as a proof rather than a field. The situation here is similar to that with IsDistributiveLattice, where the lack of fields doesn't propagate weakwardsly through the hierarchy, but it should be possible to build a group morphism by proving just the multiplication and inverse laws, and not the identity law.

Fine

• Algebra.Morphism.Structures
• Function.Structures
• Relation.Binary.Indexed.*.Structures
• Relation.Binary.Morphism.Structures

[jamesmckinna]

For once, happy to find a long-standing issue is still open. But the discussion here, along perhaps with that on #1617 , might get lost in the wash... is there a better way for us to archive these long-standing library-design issues...?

[JacquesCarette]

In my own projects (here on github), I've been using the wiki feature to make sure such discussion gets a more archival home. Another possibility is markdown files in the repo itself. We are slowly collecting design information in the documentation itself. There might be other options as well.

I don't really care which option is picked - but I'm with @jamesmckinna that this ought to be preserved in a more durable fashion that via issues.

[jamesmckinna]

Is this also related to the problem I've tripped over in #2771 because there are two possible underlying IsEquivalence substructures (or richer such, even) if the composite structure is defined in the 'natural' way, rather than as 'monoid/group plus additional multiplicative structure'?

UPDATED: Ah, no that's more like https://github.com/agda/agda-stdlib/issues/1617

[JacquesCarette]

Basic issue: records and the current tools we have for declaring them are insufficient tools to help us represent theories and their relations adequately. Records are the low-level 'compilation' target for a "proper" network of theories.

There are all sorts of features that we'd want for theories (such as multiple interfaces, known meta-language, functors to/from other theories, construction means like pullbacks and cartesian lifts, etc) that are not features that make sense for all records.

Dependent records are alluringly close, and work fine up to a certain scale of network of theories, and then fall flat. We're encountering that pain more and more frequently.

[jamesmckinna]

Candidate feature-request issue for the main agda tracker: telescopic rows as first-class objects, with records their reification as types?

[JacquesCarette]

That certainly would be an excellent start!