# 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 -> 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 recently^{1,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

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.