Open laMudri opened 5 years ago
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.
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.
I thought it'd be worth summarising this comment here.
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.
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.
Algebra.Morphism.Structures
Function.Structures
Relation.Binary.Indexed.*.Structures
Relation.Binary.Morphism.Structures
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...?
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.
In the algebra hierarchy, we naturally have this diamond.
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ʳ
andzeroˡ
, 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 fulldistrib
andzero
fields.This is causing trouble here. The required
isRightSemimodule
field is of typeIsRightSemimodule (Ring.semiring ring) m ℓm
, but the naturalisRightSemimodule
definition to export is of typeIsRightSemimodule (CommutativeSemiring.semiring commutativeSemiring) m ℓm
, becauseCommutativeRing.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:The
===
are where smart constructors go from the abbreviated structure (likeCommutativeMonoidˡ
) 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.