On 7/24/12 9:19 PM, Christian Sternagel wrote:
(x == y) = True ==> x = y (x == y) = False ==> not (x = y) (x == _|_) = _|_ (_|_ == y) = _|_
Those axioms state that (==) is sound w.r.t. to meta-equality and strict in both it's arguments.
An immediate problem that arises here is: what exactly does meta-equality denote in Isabelle/HOLCF? If it is meant to denote syntactic identity or Leibniz equality a la Coq, then the first axiom is certainly too strong for any interesting data types (e.g., Rational, Data.Set, Data.Map, Data.IntSet,...) While Eq is intended to denote an equivalence relation, it is just that; it is not an equality relation. This means you should be treating Eq as defining a setoid (or partial setoid, for instances like Double/Float). That is, you must distinguish between the raw type and the type quotiented by its (==). The containers libraries have taken pains to try and ensure that the difference cannot be observed within Haskell, but not all instances are so doctrinaire. -- Live well, ~wren