Extending Discipline Law Testing Operators

[TonioGela]

TLDR: can we add --> to Discipline?

A few days ago, I had the chance to speak with @djspiewak about the law testing we perform in cats, and our conversation became about the style in which laws are written.

A good number of our laws at the moment are written in this style:

  def antiSymmetryEq(x: A, y: A, f: A => A): IsEq[Boolean] =
    (!E.eqv(x, y) || E.eqv(f(x), f(y))) <-> true

which adheres to this simple structure:

def rule: IsEq[Boolean] =  (!a) || b <-> true

This style is not particularly loved by Daniel (nor me) as it's a bit hermetic and doesn't let you reason in terms of "rewrite equivalences", and for this reason, I began writing a PR that refactors these laws.

---

While writing though I realized that a law like

def rule: IsEq[Boolean] =  (!a) || b <-> true

can't generally be rewritten in a more readable way such as

def rule: IsEq[Boolean] =  a <-> b

since a <-> b expresses a co-implication while (!a) || b <-> true expresses a mere implication a --> b

To demonstrate this it's enough to compare the truth table of !a || b and the one of a => b (the co-implication truth table is added too)

a	b	!a	!a or b	a => b	a <=> b
T	T	F	T	T	T
T	F	F	F	F	F
F	T	T	T	T	F
F	F	T	T	T	T

This made me realize that there are cases in our law tests where the only thing we can always prove is an implication between two expressions, but not vice-versa: if you consider the example I pasted earlier:

  def antiSymmetryEq(x: A, y: A, f: A => A): IsEq[Boolean] =
    (!E.eqv(x, y) || E.eqv(f(x), f(y))) <-> true

it can be easily noticed that this should be an implication since the equality of the arguments ALWAYS implies that f(x) == f(y), but the equality of the function's value in two points doesn't imply that the points coincide.

---

I personally found that expressing this kind of relationship between expressions is important, and that is important to express it in an easy and readable way.

For this reason, I'm here to propose adding another operator alongside the well-known <->, which expresses an implication and that will let us rewrite the previous law as

  def antiSymmetryEq(x: A, y: A, f: A => A): IsEq[Boolean] =
    E.eqv(x, y) --> E.eqv(f(x), f(y))

Making it more readable and easy to express (again, IMHO).

Another beneficial side effect of introducing this operator is that we can clearly express weaker and stronger laws in a clear and distinguishable way.

This refers to the fact that I found a bunch of laws written in the weak form !(a) || b <-> true (that were probably copy-pasted from surrounding laws) that can be rewritten in the stronger form a <-> b, making them more meaningful and valuable as they will demonstrate (or better, verify a gazillion of times) even the b => a implication (think for example E.eqv(x, y) <-> E.eqv(bijective_f(x), bijective_f(y)))

Last but not least, --> can be leveraged to rewrite complicated laws like

  def compare(x: A, y: A): IsEq[Boolean] = {
    val c = E.compare(x, y)
    (((c < 0) == E.lt(x, y)) && ((c == 0) == E.eqv(x, y)) && ((c > 0) == E.gt(x, y))) <-> true
  }

in a simpler way

  def compare(x: A, y: A): IsEq[Boolean] = {
    val c = E.compare(x, y)
    (c < 0) --> E.lt(x, y) && (c == 0) --> E.eqv(x, y) && (c > 0) --> E.gt(x, y)
  }

(ofc, we'll need to introduce a && combinator for expressions built with -->)

---

I would love to know what you think about it. I personally believe that this can add value to Discipline, and that's the reason I'm proposing it.

I haven't talked about any implementation detail as the modification seems easy to me (I obviously have a branch in my fork with a POC), and as I wanted to focus more on the content itself.

Also, --> is just an idea. I'm prepared to 🚲-shed about it 😇