Homomorphism-based equality

[romac]

From @vkuncak e-mail:

Dear all,

Some important news about equality. After reading some discussions on
Coq mailing list on that topic, I don't feel bad that it took some time
for them to come.

First, I am writing to mention that Jad has a version of observational
equality in System FR defined using our CBV-like reduction. Congrats!
This is the core equality that ignores types. It seems like a clear
improvement over our previous notion. Because it does not depend on
types, it will be highly reusable for other purposes.

Next, it is also clear that we would like user-defined notion of
equality, which is meant to be coarser. Here I also think we made some
progress on how to proceed. My suggestion is to use a homomorphism to
define equality:

trait Eq[A] {
  def code(x: A): EqualsUniverse
  def ===(x: A, y: A): Boolean = {
   code(x) === code(y) // reflexive, symmetric, transitive - because == is
  }
}

This takes care of it being an equivalence relation without having to
check any laws, so we get some correctness by construction there. We use
this trait as a type class, defining instances Eq[List[A]] given Eq[A],
and so on.

The EqualsUniverse is an uninterpreted sort that has built-in logical
equality that solvers understand and treat efficiently:

trait EqualsUniverse {
  // real equality, where we can substitute equals for equals
  def ===(that: EqualsUniverse): Boolean
}

The solvers should make no assumption on the cardinality of
EqualsUniverse; it should certainly be permitted to be infinite. I
believe this is slightly better than saying that EqualsUniverse is, say,
BigInt.

A question in my mind remained how to define actual congruences with
respect to operations. I think the following is an attractive solution;
hopefully it is not too cumbersome. For each operation for which we care
that === is a congruence, we introduce it as a magma (apparently less
ambiguous notion than Groupoid that some people use to denote a
structure with one operation). Magma always builds on Eq. It's a type
where you have equality and one operation, combine:

trait Magma[A] {
  def eq: Eq[A]
  def combine(x: A, y: A): A

  @law
  def congruent(x1: A, x2: A, y1: A, y2: A): Boolean = {
    import eq._
    (x1 === x2 && y1 === y2) ==
      (combine(x1, y1) === combine(x2, y2))
  }
}

Then Semigroup and all other structures build on Magma, so they get
congruence.

The congruent law translates to:

(code(x1) == code(x2) && code(y1) == code(y2)) ==
  (code(combine(x1, y1)) === code(combine(x2, y2)))

Unlike equivalence properties, we do not get homomorphism properties
automatically. To construct homomorphisms in practice, it is in fact
useful to introduce them into hierarchy directly, because it would allow
us to define equality more easily by mapping to other structures where
we have user-defined equality. So, Eq[A] should imply (and in some way
be no more than) Magma2Morphism[A,EqualsUniverse].

trait Magma2Morphism[A,B] {
  def h(x:A): B
  def mA: Magma[A]
  def mB: Magma[B]

  @law
  def hom(x1: A, x2: A): Boolean = { // usual definition of homomorphism
    mB.eq.===(h(mA.combine(x1, x2)), mB.combine(h(x1), h(x2)))
  }

  @law
  def eqHom(x1: A, x2: A): Boolean = {
    mA.eq.===(x1, x2) ==mB.eq.===(h(x1), h(x2))
  }
}

Whereas hom is the usual definition of homomorphism, we also need to
ensure that h itself is well defined with respect to equality, which
is what eqHom does. Expanding the definition in eqHom we get

(mA.eq.code(x1) === mA.eq.code(x2)) ==
  (mB.eq.code(h(x1)) === mB.eq.code(h(x2)))

In the case where we define structures using homomorphisms (e.g. define
rationals in terms of reduced rationals), we will have that h is the
reduction function and we would define

mA.eq.code(x) = mB.eq.code(h(x))

which would reduce the eqHom condition to a trivial implication P ==P.

The Magma1Morphism would be like Magma2Morphism but for unary operation
combine1. Also, there may be more things we need to do when we have
structures with more complex operations, especially if they involve
multiple carrier types. I would be happy to discuss how this is done in
Cats or what happens inside Isabelle/HOL libraries, Coq libraries, or
Lean libraries. Theoretically it sounds better to avoid n-ary operations
and define machinery to work with products. It could be that using
Functors would take care of multiple operations of different arity.

Viktor