[Haskell-cafe] Is (==) commutative?

[Christian Sternagel]

Dear all,

Thanks for your replies. Just to clarify: I am fully aware that inside 
Haskell there is no guarantee that certain (intended) requirements on 
type class instances are satisfied. I was asking whether the intention 
for Eq is that (==) is commutative, because if it was, I would require 
that as an axiom for the equivalent of Eq in our formal setting (I'm 
using the proof assistant Isabelle/HOLCF [1]). Afterwards only types for 
which one could prove commutativity could be instances of Eq. But if 
there where already "standard" instances which violated this 
requirement, adding it in the formal setting would prevent it from being 
applicable to "standard" Haskell programs.

Btw: Isabelle/HOLCF unifies all error values and nontermination in a 
single bottom element _|_. Currently we are using the following axioms 
for our formal Eq class (where I'm using Haskell syntax although the 
real sources [2] use Isabelle/HOLCF syntax which is slightly different; 
(=) is meta-equality).

   (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. The question is whether we should also add.

   (x == y) = _|_ ==> (y == x) = _|_

Which would directly imply

   (x == y) = (y == x)

cheers

chris

[1] http://isabelle.in.tum.de (and 
http://isabelle.in.tum.de/dist/library/HOL/HOLCF/)
[2] http://sourceforge.net/p/holcf-prelude