[Haskell-cafe] Is (==) commutative?
wren ng thornton
wren at freegeek.org
Mon Jul 30 06:29:30 CEST 2012
On 7/24/12 9:19 PM, Christian Sternagel wrote:
> (x == y) = True ==> x = y
> (x == y) = False ==> not (x = y)
> (x == _|_) = _|_
> (_|_ == y) = _|_
> Those axioms state that (==) is sound w.r.t. to meta-equality and strict
> in both it's arguments.
An immediate problem that arises here is: what exactly does
meta-equality denote in Isabelle/HOLCF? If it is meant to denote
syntactic identity or Leibniz equality a la Coq, then the first axiom is
certainly too strong for any interesting data types (e.g., Rational,
Data.Set, Data.Map, Data.IntSet,...)
While Eq is intended to denote an equivalence relation, it is just that;
it is not an equality relation. This means you should be treating Eq as
defining a setoid (or partial setoid, for instances like Double/Float).
That is, you must distinguish between the raw type and the type
quotiented by its (==). The containers libraries have taken pains to try
and ensure that the difference cannot be observed within Haskell, but
not all instances are so doctrinaire.
More information about the Haskell-Cafe