Someone recently asked me why I think Eq should have more laws than the usual three:
a ~ aa ~ b => b ~ aa ~ b /\ b ~ c => a ~ c
In addition to these three, I would add three more (the first is sort of vacuous):
- Identity of indiscernibles: If for all functions
f: A -> BwithEq A,f x ~ f y => x ~ y. - Indiscernibility of identicals: For any function
f: A -> BandEq B,x ~ y => f x ~ f y. - Indescernibility of identicals (boolean properties): For any function
f: A -> Boolean,x ~ y => f x = f y.
Haskell recentlybase-eq-4-9base-eq-4-14 added indescernibility of identicals to the list of Eq's laws.
This prevents a number of hacky Eq instances such as (x, y) ~ (u, v) iff x ~ u. Why would we want to prevent these?
1. Equational reasoning
Section missing id
Suppose that we do not require these laws, so our Eq is "unlawful". Consider an expression like f (mappend mempty x), can we simplify it to f x? If Monoid laws are defined in terms of unlawful Eq, then we can't really do that. Even though mappend mempty x ~ x, we do not know that substitution under function f is allowed, since f might be observing something about its argument that is not part of the equality as defined by Eq instance.
2. Counting types
Section missing id
A similar issue occurs when we are trying to count values of a polymorphic type like forall a. Monoid a => a. According to the laws of Monoid a, it seems like the only possible value for this polymorphic type is mempty. However, that kind of reasoning ends up being highly non-compositional, since forall a b. Monoid a => (a -> b) -> b suddenly has an infinite number of possible values: \f -> f mempty, \f -> f (mempty |+| mempty), etc. Even though we can't distinguish between mempty and mempty |+| mempty according to our Eq a, that doesn't mean that applying some f : a -> b to it won't allow us to distinguish them.
3. Mapping sets
Section missing id
Suppose we define map :: Eq b => (a -> b) -> Set a -> Set b, can our map function possibly satisfy functor laws?
Consider
data A = A Int Int
class Eq a where
(==) (A x1 y1) (A x2 y2) = x1 == x2
set :: Set (Int, Int)
f :: (Int, Int) -> A
g :: A -> Int
foo :: Set Int
foo = map g (map f set)
Let
set = Set.fromList [(0, 1), (0, 2)]
g (A a b) = b
f (a, b) = A a b
Then
map f set = Set.singleton (A 0 1) -- W.L.O.G.
map g (map f set) = Set.singleton 1
-- but
map (g . f) set = Set.fromList [1, 2]
This would not have been an issue if our Eq was lawful. TODO: proof. Proof for now: intuitively obvious.
Haskell