What are the laws for Eq1, Eq2, Ord1, and Ord2?

[Oleg Grenrus]

My hand-wavy intuition:

Eq witnesses an equality. a -> a -> Bool type isn't enough to guarantee
that,
so we have laws.

The Eq1 class has member

    liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool

the type `a -> b -> Bool` is not an equality decision procedure,
but rather an isomorphism one.

It looks like for me, that liftEq gives a natural transformation from
`Iso a b` to `Iso (f a) (f b)`. Does this make sense?

The liftEq2 is the same. We have to think Map as not of

  Hask * Hask -> Hask (wrong)

Functor but

  OrdHask * Hask -> Hask (OrdHask: Ord-types and monotone functions)

Then, comparing Map k () with Map (Down k) () with \k (Down k') = k == k'
is not well defined, as that "isomorphism candidate" doesn't respect
ordering.
(as an example, for k = Integer, \k (Down k') = k == negate k' would
work, or
even \n m -> n == succ m, for n m :: Integer)

Similar argument can be used on (Eq k, Hashable k) requirement of
HashMap k v,
with constraints giving an additional Hashable structure. The motivational
example is being able to compare

    HashMap Text Foo   and   HashMap BusinessId Foo'

directly, where
 
    newtype BusinessId = BusinessId Text deriving newtype (Eq, Hashable)


As Hashable is somewhat arbitrary, I cannot think of other use-cases
(preserving Hashable is next to impossible otherwise then via newtype
deriving).  However, for Map there might be A, B such that `Map A v` and
`Map
B v` are comparable, i.e. there is monotone f :: A -> B, and

    compareAB a b = f a `compare` b

which we can use as a first argument for liftCompare2 (Ord2). (There is
mapKeysMonotonic which can be used to achieve the same effect!
unordered-containers could have similar unsafe function too).  That said, I
didn't have such use case myself (yet!?).

When writing the instances, I was thinking what's (a -> b -> Ordering),
and at this point I have to wave hands even more. I don't know how to
complete
the following sentence

    The ??? to total order is as isomorphism to equality.

As a side-note: we have
- `~` witnessing nominal equality
- `Coercible` witnessing structural equality
- It would be very cool to being to say `CoercibleInstance Hashable`,
which is
  satisfied when `Hashable` is `newtype` derived. Is it roles, refining
kinds,
  or something else, I don't know. But I feel it would be useful.  It can be
  used to give `mapKeysMonotonic` a safe type (at least in some cases!)
  Maybe if `Constraint ~ Type`, we could simply require `Coercible (Hashable
  k) (Hashable k')`, but how it would fit the roles?

So I do agree, that Eq1 f has functorial feel and it's "natural",
this is what its type tells. But if you imply that we should add
`Functor` or
`Bifunctor` super-classes, then I disagree, based on above arguments.
Yes, the functions are unsafe to use (to get meaningful results),
but I see a value for them.

An example of legitimate (in above sence) instance of Eq1 which isn't a
functor is Eq1 Set. As long as `eq :: a -> b -> Bool` respects the
ordering of
`a` and `b`, we can compare `Set a` with `Set b`.
<Insert a riddle about comparing sets of apples and oranges,
if one can compare apples with oranges, so fruit comparison diagram
commutes>

Cheers, Oleg


> I was looking at the Eq2 instances for Data.Map and Data.HashMap, and
> the Eq1 instances for Set and HashSet, and I realized that they're a
> bit ... weird. My instinct is to remove these instances immediately,
> but I figure I should first check with the community (and Oleg, who
> added them to begin with) to make sure they don't make some sort of
> sense I don't understand. In particular, these instances compare keys
> in the order in which they appear in the container. That order may be
> completely unrelated to the given key comparison function.
>
> Data.Map example: suppose I have a Map k () and a Map (Down k) (),
> where Down is from Data.Ord. If I call liftEq2 (\x (Down y) -> x == y)
> (==), I will get what looks to me like a totally meaningless result.
>
> Data.HashMap example: suppose I have a HashMap Int () and a Hashmap
> String (). If I call liftEq2 (\x y -> show x == y) (==), that won't
> return True even if the strings in the second map are actually the
> results of applying show to the numbers in the first map.
>
> Intuitively, I think Eq1 f only makes sense if the shape of f x does
> not depend on the values of type x, and Eq2 p only makes sense if the
> shape of p x y does not depend on the values of types x and y. Is
> there a way to formalize this intuition with class laws? I believe
> that in the case of a Functor, parametricity will guarantee that
>
>   liftEq eq (f <$> xs) (g <$> ys) == liftEq (\x y -> eq (f x) (g y)) xs ys
>
> Are there *any* legitimate instances of Eq1 or Ord1 that are not
> Functors? Are there *any* legitimate instances of Eq2 or Ord2 that are
> not Bifunctors? My intuition says no. We might wish we could write
> instances for unboxed arrays or vectors, but I believe that is totally
> impossible anyway.
>
> David


On 15.03.2018 23:48, David Feuer wrote:
> I was looking at the Eq2 instances for Data.Map and Data.HashMap, and
> the Eq1 instances for Set and HashSet, and I realized that they're a
> bit ... weird. My instinct is to remove these instances immediately,
> but I figure I should first check with the community (and Oleg, who
> added them to begin with) to make sure they don't make some sort of
> sense I don't understand. In particular, these instances compare keys
> in the order in which they appear in the container. That order may be
> completely unrelated to the given key comparison function.
>
> Data.Map example: suppose I have a Map k () and a Map (Down k) (),
> where Down is from Data.Ord. If I call liftEq2 (\x (Down y) -> x == y)
> (==), I will get what looks to me like a totally meaningless result.
>
> Data.HashMap example: suppose I have a HashMap Int () and a Hashmap
> String (). If I call liftEq2 (\x y -> show x == y) (==), that won't
> return True even if the strings in the second map are actually the
> results of applying show to the numbers in the first map.
>
> Intuitively, I think Eq1 f only makes sense if the shape of f x does
> not depend on the values of type x, and Eq2 p only makes sense if the
> shape of p x y does not depend on the values of types x and y. Is
> there a way to formalize this intuition with class laws? I believe
> that in the case of a Functor, parametricity will guarantee that
>
>   liftEq eq (f <$> xs) (g <$> ys) == liftEq (\x y -> eq (f x) (g y)) xs ys
>
> Are there *any* legitimate instances of Eq1 or Ord1 that are not
> Functors? Are there *any* legitimate instances of Eq2 or Ord2 that are
> not Bifunctors? My intuition says no. We might wish we could write
> instances for unboxed arrays or vectors, but I believe that is totally
> impossible anyway.
>
> David


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180316/f3f8f1a6/attachment.sig>