Much of the work applies to all rings, and some of the algebra applies to weaker algebraic structures, but the generalizations weren't made during development because of constraints whose solutions were discovered late in development of the first version (esp. Issue #24). See also the comments for dotBasisRIsIndex.
Those issues are likely to be affected by an update in Idris version. The algebraic hierarchy may have to change to reflect more recent versions of the language and packages.
Ultimately, the gaussian elimination algorithm works for any Bezout domain, in a way explicitly represented in the present types, so that level of generality is the ideal situation.
Generalizing Data.Matrix.LinearCombinations to other verified rings with unity would signify this is possible.
Note that because of diamond instance problems, some proofs become significantly complicated by posing them for less general structures than they apply to. The proof of ringOpIsDistributiveSubR, for instance, does not work if one assumes one has a VerifiedRingWithUnity rather than a VerifiedRing.
runKleisli
commented
6 years ago
(also involves refactoring)
Much of the work applies to all rings, and some of the algebra applies to weaker algebraic structures, but the generalizations weren't made during development because of constraints whose solutions were discovered late in development of the first version (esp. Issue #24). See also the comments for
dotBasisRIsIndex.Those issues are likely to be affected by an update in Idris version. The algebraic hierarchy may have to change to reflect more recent versions of the language and packages.
Ultimately, the gaussian elimination algorithm works for any Bezout domain, in a way explicitly represented in the present types, so that level of generality is the ideal situation.
Generalizing Data.Matrix.LinearCombinations to other verified rings with unity would signify this is possible.
Note that because of diamond instance problems, some proofs become significantly complicated by posing them for less general structures than they apply to. The proof of
ringOpIsDistributiveSubR, for instance, does not work if one assumes one has aVerifiedRingWithUnityrather than aVerifiedRing.