Unusual EqLaws definition

[hiroshi-cl]

I found that EqLaws has an unusual definition:

cats/kernel-laws/shared/src/main/scala/cats/kernel/laws/EqLaws.scala

Lines 36 to 37 in d40b884

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

Equivalency that I know doesn't have antisymmetry law, that is typically included in order.
I wonder where is the source of this kind of equivalency definition.

[johnynek]

It's a weird name. It doesn't seem to be anything about antisymmetry.

It's more that any pure function that maps A to itself preserves Eq.

Why would you expect that? I guess it is some argument about if two A values are eqv than any transformation of them into other As should preserve that equality.

It's weird if you think a1 == a2 but then f(a1) != f(a2) by the same Eq.

So, I think the law is sensible but where I comes from I don't recall.

[hiroshi-cl]

Thank you for your reply.

it is some argument about if two A values are eqv than any transformation of them into other As should preserve that equality.
It's weird if you think a1 == a2 but then f(a1) != f(a2) by the same Eq.

No. It's not obvious property and too strong restriction.
Many equality don't satisfy this law and only homomorphic transformations can preserve their equality.

For example, let's think about def eq(a: Int, b: Int): Boolean = a % 6 == b % 6.
In this case, (x: Int) => x / 3 doesn't preserve this equality.
3 == 9 but (3 / 3) != (9 / 3)

[johnynek]

@hiroshi-cl I see what you mean. My math is a bit rusty, but I think you want an Equivalence relation:

https://en.wikipedia.org/wiki/Equivalence_relation

but what Eq is really about is an Equality:
https://en.wikipedia.org/wiki/Equality_(mathematics)

Eq is about "...asserting that the quantities have the same value."

this text in Equivalence Relation describes:

Equality is both an equivalence relation and a partial order. Equality is also the only relation on a set that is reflexive, symmetric and antisymmetric. In algebraic expressions, equal variables may be substituted for one another, a facility that is not available for equivalence related variables. The equivalence classes of an equivalence relation can substitute for one another, but not individuals within a class.

I would say you want a new type class, like:

trait Equivalence[A] {
  def equiv(a: A, b: A): Boolean
}

The problem with equivalence is you probably don't want any of them to be implicit. For the whole type class pattern to work you really want there to be one privileged instance for a given type. With an Equivalence relation, that's not really the case.

How does that sound?

[hiroshi-cl]

I'm not convinced what you mean but introducing a new type class sounds a good idea.
Thank you.