typelevel / algebra

Experimental project to lay out basic algebra type classes
https://typelevel.org/algebra/
Other
378 stars 69 forks source link

Law testing guidelines #209

Open denisrosset opened 6 years ago

denisrosset commented 6 years ago

(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.

TomasMikula commented 6 years ago

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.