WIP: Switch laws to cats-core encoding

[LukaJCB]

This isn't close to finished, but should update the build to RC1 soon :)

[coltfred]

Am I correct in remembering that this is holding up the publish for cats 1.0-RC1?

[LukaJCB]

I just finished up the lattice laws and would love to get some feedback before I start with the Ring laws. :)

[denisrosset]

I would split the absorption law in two pieces, so that the return type is IsEq[A]

[denisrosset]

Why not split in two laws that return IsEq[A]?

[denisrosset]

A JoinSemilattice does not extend Semilattice, so why should the laws follow the same pattern?

[denisrosset]

Hi @LukaJCB , now I'm convinced that the new cats-core law encoding is bad for algebra/spire.

It has a lot of code duplication between the discipline and non-discipline parts. The law delegation implemented in lattices and rings is only visible in the discipline package, which negates the clarity advantage of having straightforward declarations of laws without the discipline encoding.

Anyway, I don't have a strong opinion for algebra as Spire is probably going to keep its own law implementations to cater for primitive types that approximate a lawful type (for example integers).

[LukaJCB]

Hey Denis, thanks for checking in! I think that's a good decision. We'll have to see on the algebra front (as it might move into the cats repo at some point)

[johnynek]

Personally, I think this whole discipline style is pretty terrible.

I don't know why law methods returning scalacheck Prop on objects aren't actually better.

[denisrosset]

@johnynek which style do you find terrible? the current algebra style, the cats-core style, both?

What would you advocate?

(I'm in the middle of refactoring laws for Spire, and am trying for find good middle ground)

[johnynek]

Frankly both.

I would do:

object Laws {
  def associativity[T: Semigroup: Arbitrary: Eq]: Prop =
    forAll { (a: T, b: T, c: T) =>
      val right = Semigroup[T].combine(a, Semigroup[T].combine(b, c))
      val left = Semigroup[T].combine(Semigroup[T].combine(a, b), c)
      Eq[T].eqv(left, right)
    } :| "Semigroup Associativity"
}

etc...

and I would build up to things like

def monoidLaws[T: Monoid: Arbitrary: Eq]: Prop

by calling the others.

Then users can check the properties using scalacheck or scalatest (both can check Prop).

I don't see the need to build this inheritance heavy framework around what should just be functions that return Prop.

[denisrosset]

@johnynek How does it behave when checking the resulting Prop? Does it perform minSuccessful tests for each embedded property, or distributes the 100 cases randomly among the checked properties? Do you have a code example written in that style?

[TomasMikula]

I agree that discipline is pretty terrible. Some time ago I tried to summarize what bothered me with discipline. (The approach I implemented in that project is not great either—it uses == on "law sets" to avoid duplicate laws in case there is diamond inheritance.) Maybe it's really better to explicitly state all the laws of a type class without inheriting any (but reusing implementation).

[denisrosset]

@TomasMikula Actually, the parents vs bases distinction enables the reuse of the semigroup/monoid/group laws to test the additive and multiplicative substructures of rings. So this complexity has a justification.

[TomasMikula]

It's not the only way, and it's not a simple one, either. Why do you need the distinction in this specific case of rings?

[denisrosset]

I guess the original justification was to avoid duplication of the semigroup/monoid/group laws for the additive and multiplicative structures in a ring. The alternative is to have a hierarchy for additive structures, a hierarchy for multiplicative structures, and rings inherit both.

I guess it's a tradeoff.

[TomasMikula]

I mean, why do you need the distinction between parents and bases? Why not have just one type of inheritance? I guess the motivation there was to avoid inheriting the same laws twice in case of diamond inheritance (such as MonadLaws inheriting functor laws twice, once from ApplicativeLaws and once from FlatMapLaws), but I don't think it is a good solution (for reasons listed in the above link).

[denisrosset]

In parents, you avoid checking laws twice, which corresponds to the case you mention. In bases, you allow duplication, because you are testing different parts of a structure, e.g. a ring contains an additive and a multiplicative monoid, so you need to test the monoid laws twice.

I don't see a way out of having two kind of inheritance relations, short of duplicating laws.

BTW @non is the original author of discipline; I'm merely trying to find an optimal way to test numerical stuff in Spire. As of now, all solutions I have seen have drawbacks.

[TomasMikula]

I don't see a way out of having two kind of inheritance relations, short of duplicating laws.

Principled avoids duplication with one kind of inheritance. MonadLaws would inherit FunctorLaws twice, but that would be detected by comparing the two FunctorLaws instances for equality (which reduces to comparing typeclass instances for equality, which is the ugly part of that approach and why I'm not really advocating to use it; though failing to have a meaningful universal equality of typeclass instances would just mean that you get some duplication, but not lose any checks).

One of the problems with discipline is that if I choose a parent, I don't really know which laws I'm inheriting, without studying the hierarchy of the parent (which could change over time without warning). I would therefore resort to just use bases (in order to not miss any checks), but then I have duplicities and thus missed the whole point.

[denisrosset]

In that case, you lose the possibility of checking both Ring[A].additive: Monoid[A] and Ring[A].multiplicative: Monoid[A]; for this case, you need to use twice the monoid laws.

For that purpose, bases are used when checking an 'embedded structure: for example the semigroups/monoids that appears in lattices, and the monoids/groups that appear in rings/fields. If I were to perform the same checks with Principled, only one of the derived semigroups/monoids would be checked, as the other one would be eliminated by the equality checks.

BTW, I don't think there is any use of bases in cats at the moment.

[TomasMikula]

If I were to perform the same checks with Principled, only one of the derived semigroups/monoids would be checked, as the other one would be eliminated by the equality checks.

It wouldn't be eliminated, because the two law sets for monoid would compare as different (because the two Monoid instances would compare as different).

BTW, I don't think there is any use of bases in cats at the moment.

Do cats use discipline much at all?

[denisrosset]

@TomasMikula thanks for the clarification!

[denisrosset]

@johnynek Thanks for intervening. We can indeed remove all abstractions.

We pay a small price, the repetition of the Semigroup. prefix, and of the [A:Arbitrary:Eq] implicits.

I also removed the Rules abstraction, as to provide a single site that documents relevant laws for a typeclass.

Parents are handled by merging Maps, and bases are handled by adding a prefix to the properties of the derived instance (not yet done).

object GroupLaws {

  def semigroup[A:Arbitrary:Eq](implicit A: Semigroup[A]): Map[String, Prop] =
    Map(
      "Semigroup.associativity" -> forAll { (x: A, y: A, z: A) =>
        A.combine(A.combine(x, y), z) ?== A.combine(x, A.combine(y, z))
      },

      "Semigroup.combineN(x, 1) === x" -> forAll { (x: A) =>
        A.combineN(x, 1) ?== x
      },

      "Semigroup.combineN(x, 2) === x |+| x" -> forAll { (x: A) =>
        A.combineN(x, 2) ?== A.combine(x, x)
      },

      "Semigroup.combineAllOption" -> forAll { (xs: Vector[A]) =>
        A.combineAllOption(xs) ?== xs.reduceOption(A.combine)
      }
    )

  def band[A:Arbitrary:Eq](implicit A: Band[A]): Map[String, Prop] =
    semigroup[A] ++ Map(
      "Band.idempotence" -> forAll { (x: A) =>
        A.combine(x, x) ?== x
      }
    )
}

[TomasMikula]

Nice. Maybe don't add the Semigroup. prefix?

[denisrosset]

The prefix is a convention to avoid name collisions.

Now looking at a proof-of-concept translation of all algebra laws. The encoding above could be a tad slower for the big nested hierarchies.

[TomasMikula]

The prefix is a convention to avoid name collisions.

I mean, optionally add a prefix when inheriting.

[denisrosset]

I want to avoid fancy abstraction as much as possible. With this encoding, given a failed test, a simple string search reveals the corresponding law.

[TomasMikula]

That's a good argument 👍

[LukaJCB]

Closing this now :)