Why identity of indiscernibles?
Someone recently asked me why I think
Eq should have more laws than the usual three:
a ~ a
a ~ b => b ~ a
a ~ b /\ b ~ c => a ~ c
In addition to these three, I would add two more (even though the first is sort of vacuous):
- Identity of indiscernibles: If for all functions
f: A -> Bwith
f x ~ f y => x ~ y.
- Indiscernibility of identicals: For any function
f: A -> Band
x ~ y => f x ~ f y.
- Indescernibility of identicals (boolean properties): For any function
f: A -> Boolean,
x ~ y => f x = f y.
This prevents a number of hacky
Eq instances such as
(x, y) ~ (u, v) iff x ~ u. Why would we want to prevent these?
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
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 . 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.
Suppose we define
map :: Eq b => (a -> b) -> Set a -> Set b, can our
map function possibly satisfy functor laws?
This would not have been an issue if our
Eq was lawful. TODO: proof. Proof for now: intuitively obvious.