[Haskell-cafe] Is (==) commutative?
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).
More information about the Haskell-Cafe