Discussion:
What are the laws for Eq1, Eq2, Ord1, and Ord2?
David Feuer
2018-03-15 21:48:40 UTC
Permalink
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
Oleg Grenrus
2018-03-15 23:55:23 UTC
Permalink
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
Post by David Feuer
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
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
David Feuer
2018-03-16 01:27:01 UTC
Permalink
I believe we should not add a Functor constraint, but for a different
reason. One could write

data Arr a where
I :: Unboxed.Vector Int -> Arr Int
C :: Unboxed.Vector Char -> Arr Char

This has no valid Functor instance, but it has a perfectly sensible Ord1
instance.

As for Map and HashMap, I'd be inclined to remove the "dangerous" instances
and add functions (names to be determined) people can use when they know
what they're doing. The trouble with the instances is that there's no
apparent way to express in the *class* laws what makes an argument valid or
invalid. It becomes ad hoc overloading, and I don't think most Haskellers
are really into that.
Post by Oleg Grenrus
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
Post by David Feuer
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
Post by David Feuer
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
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
Post by David Feuer
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
Gershom B
2018-03-16 03:36:52 UTC
Permalink
So looking at the “bad” examples they both seem to only be bad for Eq2, and be bad because they “abuse” a design choice in the class.

In particular, we have

class Eq2 f where
    liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> f a c -> f b d -> Bool Source#

  — Lift equality tests through the type constructor.

  — The function will usually be applied to equality functions, but the more general type ensures that the implementation uses them to compare elements of the first container with elements of the second.

This is to say that the two types, `a` and `b`, are intended to be equal. However, to prevent implementations from making the error of comparing two values from the first container, they are made distinct. So in the intended usage, this is not called directly but rather via eq2.

eq2 :: (Eq2 f, Eq a, Eq b) => f a b -> f a b -> Bool

What David has pointed out, I think, is that this clever trick, which prevents some bad implementations, is open to abuse in the case of _good_ implementations, since the assumption of the two types being equal is necessary for some structural invariants to hold. (In particular, if the `a` and `b` differ, they will have different ordering properties).

So I see two options here, neither of which involves removing any instances.

A) change the types in the Eq2 and Ord2 classes to not use this clever trick. I think this should not break anything, since according to the documentation, nothing should be making use of the possibility of these types varying.

B) change the documentation of the classes to make explicit that the laws are _only_ expected to apply when the types are equal, and when they are not, the behavior is undefined.

Cheers,
Gershom


On March 15, 2018 at 7:57:34 PM, Oleg Grenrus (***@iki.fi) wrote:

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
Post by David Feuer
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
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
David Feuer
2018-03-16 03:50:44 UTC
Permalink
For Map and HashMap, yes, Eq2 and Ord2 are the problem. For Set and
HashSet, Eq1 and Ord1 are trouble.

The advantage of the flexibility is that for a Functor or Bifunctor you get
an optimization: instead of mapping a function or two over each container
to give them the same type and then comparing the results, you can fuse it
all into one operation. Of course, the same thing could also be done for
each type using rewrite rules, but that's kind of gross.

On Mar 15, 2018 11:36 PM, "Gershom B" <***@gmail.com> wrote:

So looking at the “bad” examples they both seem to only be bad for Eq2, and
be bad because they “abuse” a design choice in the class.

In particular, we have

class Eq2 f where
liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> f a c -> f b d ->
Bool Source#

— Lift equality tests through the type constructor.

— The function will usually be applied to equality functions, but the
more general type ensures that the implementation uses them to compare
elements of the first container with elements of the second.

This is to say that the two types, `a` and `b`, are intended to be equal.
However, to prevent implementations from making the error of comparing two
values from the first container, they are made distinct. So in the intended
usage, this is not called directly but rather via eq2.

eq2 :: (Eq2 f, Eq a, Eq b) => f a b -> f a b -> Bool

What David has pointed out, I think, is that this clever trick, which
prevents some bad implementations, is open to abuse in the case of _good_
implementations, since the assumption of the two types being equal is
necessary for some structural invariants to hold. (In particular, if the
`a` and `b` differ, they will have different ordering properties).

So I see two options here, neither of which involves removing any instances.

A) change the types in the Eq2 and Ord2 classes to not use this clever
trick. I think this should not break anything, since according to the
documentation, nothing should be making use of the possibility of these
types varying.

B) change the documentation of the classes to make explicit that the laws
are _only_ expected to apply when the types are equal, and when they are
not, the behavior is undefined.

Cheers,
Gershom


On March 15, 2018 at 7:57:34 PM, Oleg Grenrus (***@iki.fi) wrote:

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
Post by David Feuer
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
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
Gershom B
2018-03-16 03:55:39 UTC
Permalink
On March 15, 2018 at 11:50:45 PM, David Feuer (***@gmail.com) wrote:

For Map and HashMap, yes, Eq2 and Ord2 are the problem. For Set and
HashSet, Eq1 and Ord1 are trouble.

The advantage of the flexibility is that for a Functor or Bifunctor you get
an optimization: instead of mapping a function or two over each container
to give them the same type and then comparing the results, you can fuse it
all into one operation. Of course, the same thing could also be done for
each type using rewrite rules, but that's kind of gross.

Right. But it is the possibility of this optimization that breaks things.
In particular, `Set` is not a functor (and does not permit mapping over
it), but it _should_ be able to be an instance of Eq1.

-g
David Feuer
2018-03-16 04:08:17 UTC
Permalink
Ah, I think I see what you mean. One option:

class EqFoo1 f where
liftEqSame :: (a -> a -> Bool)
-> f a -> f a -> Bool
-- and/or the more principled
liftEqOnSame ::
Eq b => (a -> b) -> f a -> f a -> Bool
class (Functor f, EqFoo1) => EqBar1 where
liftEqDifferent :: (a -> b -> Bool)
-> f a -> f b -> Bool
-- and/or the more principled
liftEqOnDifferent :: Eq c
=> (a -> c) -> (b -> c) -> f a -> f b -> Bool

This wouldn't be the best for my hypothetical Arr type, but I don't know
that it's an important enough case to worry about.
Post by David Feuer
For Map and HashMap, yes, Eq2 and Ord2 are the problem. For Set and
HashSet, Eq1 and Ord1 are trouble.
The advantage of the flexibility is that for a Functor or Bifunctor you
get an optimization: instead of mapping a function or two over each
container to give them the same type and then comparing the results, you
can fuse it all into one operation. Of course, the same thing could also be
done for each type using rewrite rules, but that's kind of gross.
Right. But it is the possibility of this optimization that breaks things.
In particular, `Set` is not a functor (and does not permit mapping over
it), but it _should_ be able to be an instance of Eq1.
-g
Loading...