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

Christian Sternagel c.sternagel at gmail.com
Thu Jul 26 05:49:06 CEST 2012


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



More information about the Haskell-Cafe mailing list