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

[Christian Sternagel]

On 07/26/2012 11:53 AM, Alexander Solla wrote:
> The classically valid inference:
>
> (x == y) = _|_ => (y == x) = _|_
Btw: whether this inference is valid or not depends on the semantics of 
(==) and that's exactly what I was asking about. In Haskell we just have 
type classes, thus (==) is more or less arbitrary (apart from its type). 
But usually there are certain intentions and in HOLCF we can make those 
intentions formal by using axiomatic type classes (i.e., type classes 
together with axioms that have to be satisfied by all instances; and 
when establishing an instance we have to formally prove that all the 
axioms are indeed satisfied).

cheers

chris