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

7 messages
Open this post in threaded view
|

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

 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 _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Open this post in threaded view
|

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

 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`. 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 _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries signature.asc (836 bytes) Download Attachment
Open this post in threaded view
|

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

Open this post in threaded view
|

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

Open this post in threaded view
|