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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
