[Haskell-cafe] Is (==) commutative?
c.sternagel at gmail.com
Tue Jul 31 03:51:18 CEST 2012
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
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.)
More information about the Haskell-Cafe