algebra
algebra copied to clipboard
Law testing guidelines
(This comment is not about the simpler encoding discussed in #206.)
I remarked that the laws structure does not follow the typeclass structure exactly. For example, we have tests for Lattice[A] with BoundedJoinSemilattice[A]
, which simply collect laws of Lattice
and BoundedJoinSemilattice
, however the corresponding combined typeclass does not exist.
Combinations with DistributiveLattice[A]
do not exist: thus we have the quite obtuse fragment
def generalizedBool(implicit A: GenBool[A]) = new LogicProperties(
name = "generalized bool",
parents = Seq(),
ll = new LatticeProperties(
name = "lowerBoundedDistributiveLattice",
parents = Seq(boundedJoinSemilattice, distributiveLattice),
join = Some(boundedSemilattice(A.joinSemilattice)),
meet = Some(semilattice(A.meetSemilattice))
),
in the definition of generalizedBool
.
Laws should serve as executable documentation, and this goes against the spirit.
I don't know what is the good solution there
Solution 1: the law hierarchy follows the typeclass hierarchy. Extra laws that occur when multiple types interact are proposed separately (i.e. lattices with partial orders). For this to work, we need a way to merge RuleSets.
Solution 2: close the hierachy by adding all combinations. That would double the size of the lattice laws, as every instance would have a distributive copy alongside.
I'll try to come up with something better with my reformulation of laws; in case it does not go through, I'll let this issue remind us of the problem.
I admit the quoted snippet is terrible: Looking at it, I have no idea whether and what laws are inherited twice, or whether we don't miss any important laws. (This is despite the fact that according to git blame
it was me who wrote this code 2 years ago, so hopefully I knew at that time.)
Solution 1: the law hierarchy follows the typeclass hierarchy. Extra laws that occur when multiple types interact are proposed separately
Not sure what exactly you mean by "proposed separately", but yes, I think the law hierarchy should match the typeclass hierarchy.