On 7/30/12 9:51 PM, Christian Sternagel wrote:
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,...)
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.)
Urk. Should've been "many" :) I was waffling between a few different
quantifiers there, and it seems the "m" was an unfortunate casualty of
that conflict.
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
