Semantics of default instances of Eq

[rklaehn]

I feel very strongly that the default instances for Eq should work according to this definition of equality:

Given any x and y, x = y if, given any predicate P, P(x) if and only if P(y).

This is not the case for e.g. the default Eq instance for map:

Eq.eqv(Map(1 → 0), Map.empty[Int, Int]) evaluates to true. I think for the default Eq this should be false.

The issue in case of map is that the Eq in the implicit scope is VectorEq. This has been implemented that way to allow defining a Group instance for any Map. But I think this should be changed so that MapEq is in scope.

[TomasMikula]

This is also related to this discussion about whether some type classes should come together with a definition of equivalence under which they are lawful.

[johnynek]

I agree with @rklaehn on this. And I think @TomasMikula 's deserves some thought. It should be easy to have consistent typeclasses set up (actually hard to have them set up wrong is what I'd prefer).

[rklaehn]

I think the proper approach if you want a Map with Vector behaviour (non-present elements are zero) is to write a special map with default value that never keeps mappings to the default value. Collections are out of scope for algebra, but just to demonstrate the basic idea I have written one in https://github.com/rklaehn/abc/blob/master/core/src/main/scala/com/rklaehn/abc/TotalArrayMap.scala

By ensuring that mappings to the default value are never stored, you can still use structural equality and nevertheless define a proper Group.

[johnynek]

I'm not sure that totally works. If you want to define for instance Monoid on a Map, what do you do with keys that have one missing item in one of the maps? If you think of the Map as (Set[K], K => Option[V]) then unless we think the semigroup/monoid on Option[V] or on K => W where W: Semigroup is not legit, it is hard to see why we should arbitrarily say there should be no Map Group just because it requires a different Eq.

Also, if they cannot be more than one Eq for a given type (something I don't think we have taken seriously) then I would think we would put implicit instances for appropriate scala types in the companion object for the typeclass (which I think we would not do in algebra, as orphan instances are quite common in scala, perhaps sadly).

I think we should be able to use the standard scala types where possible with algebra typeclasses. I think that means that we need to have clean ways of setting up the right implicits together. Presumably someone is choosing the Group[Map[K, V]] that gives vector-space like semantics. At that moment, they could just set up the Eq[Map[K, V]] too, right? If so, the only question is how.

[rklaehn]

I am not opposed to having more than one Eq instance per type. I just think that the default instance that is imported when you import algebra.std.all._ should behave according to the above definition to prevent surprising behaviour like Eq.eqv(x, y) even though x.count != y.count.

I am totally fine with somebody explicitly importing both VectorGroup and VectorEq. Not sure if it would be a good idea to have a class that implements both Group and Eq, so you can only ever import them together?

[johnynek]

Sorry, I wasn't clear: I totally agree the default instance should have the property you want: i.e. eqv(x, y) implies eqv(f(x), f(y)).

[rklaehn]

Great. Then we're on the same page. So the first thing to do would be to change the Eq to MapEq and remove the typeclasses that are incompatible with this Eq from the implicit scope before people start relying on this behaviour.

Should this rule (eqv(x, y) implies eqv(f(x), f(y)) for Eq in the default implicit scope) be documented somewhere?

[johnynek]

I think it would be good to document it. We should probably make a manual, perhaps using Tut, that we could publish from the repo. This would be good to include.

[kevinmeredith]

Could you please note which import's are required to reproduce Eq.eqv(Map(1 → 0), Map.empty[Int, Int]) evaluating to true?

I tried:

import algebra._
import algebra.std._

scala> Eq.eqv(Map(1 → 0), Map.empty[Int, Int])
<console>:26: error: could not find implicit value for parameter ev: algebra.Eq[scala.collection.immutable.Map[Int,Int]]
       Eq.eqv(Map(1 → 0), Map.empty[Int, Int])

[adelbertc]

@kevinmeredith in general you need import algebra.std.<type>._ to get the instances for <type>. For Map[Int, Int] you'll need both Int and Map so:

scala> :pa
// Entering paste mode (ctrl-D to finish)

import algebra.Eq
import algebra.std.int._
import algebra.std.map._

Eq.eqv(Map((1, 0)), Map.empty[Int, Int])

// Exiting paste mode, now interpreting.

import algebra.Eq
import algebra.std.int._
import algebra.std.map._
res0: Boolean = true

[kevinmeredith]

Thanks, Adelbert. I was curious which implicit Eq was being used to compare these 2 maps.

scala> import scala.reflect.runtime.universe._
import scala.reflect.runtime.universe._

scala> reify { Eq.eqv(Map(1 -> 0), Map.empty[Int, Int]) }
res10: reflect.runtime.universe.Expr[Boolean] = Expr[Boolean]
                 (Eq.eqv(Predef.Map.apply(Predef.ArrowAssoc(1).$minus$greater(0)), 
                            Predef.Map.empty[Int, Int])(`package`.
                                  mapEq(`package`.intAlgebra, `package`.intAlgebra)))

per som-snytt's SO answer.

Looking at map.scala, I guessed that this MapEq would be used to compare the two maps.

Which implicit Eq is being used to compare them? It was not clear to me based on the reify { ... } output.

Also, why does this grep show only 1 result?

$pwd
/Users/Kevin/Workspace/Personal/algebra
$grep -r MapEq . |  grep -v target
./std/src/main/scala/algebra/std/map.scala:class MapEq[K, V](implicit V: Eq[V]) extends Eq[Map[K, V]] {

[non]

So -- initially we were cagey on whether we wanted to use an exact or sparse vector interpretation of Map values. However as @rklaehn says, we want to Eq to connote intersubstitutability (or an indistinguishable equivalence class), which means we need to use the exact definitions.

The instances added to cats.kernel are exact, and once #152 is merged algebra's will be too. We can optionally provide a wrapper for maps to introduce a sparse vector format (and to limit the operations available).

[non]

(Happy to discuss this more here, I had a conversation recently with @tixxit and @johnynek where we agreed that this was the right way to go.)

[johnynek]

See #148 for a related discussion.

[non]

We decided to use a strict interpretation (as per @rklaehn's recommendation) and no longer have any other instances.