# Why identity of indiscernibles?

Last modified on November 2, 2020 by Alex

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 -> B with Eq A, f x ~ f y => x ~ y.
• Indiscernibility of identicals: For any function f: A -> B and Eq 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 recently1,2 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?

## Equational reasoning

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.

## Counting types

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.

## Mapping sets

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.