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?




This would not have been an issue if our Eq was lawful. TODO: proof. Proof for now: intuitively obvious.