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

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