Thanks Wren, for the explanations (also in your previous mail)! On 07/30/2012 01:29 PM, wren ng thornton wrote:
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,...) Yes, we also stumbled about this (but I was only discussing it on the isabelle mailing list and not here, sorry). The conclusion was that for many type classes there are several "interesting" (whatever that means) instances. Thus, in the formalization we will use different "formal" type classes for different intended use-cases of Haskell type classes (e.g., one eq class for syntactic equality and another one that merely requires an equivalence relation, ...). That just means that there will not be a bijection between the formal class hierarchy and the actual class hierarchy of Haskell, but should not pose any further problems (I hope).
Btw: I don't agree that the axioms are too strong for *any* interesting data types ;). What about Bool, Int, [a], ...? (Again, this depends on how we interpret "interesting"; in formalizations the threshold for being interesting is typically lower.) cheers chris