Re: [Haskell-cafe] Is (==) commutative?
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
Re: [Haskell-cafe] Is (==) commutative?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
On 7/24/12 9:19 PM, Christian Sternagel wrote: Dear all, Thanks for your replies. Just to clarify: I am fully aware that inside Haskell there is no guarantee that certain (intended) requirements on type class instances are satisfied. I was asking whether the intention for Eq is that (==) is commutative, because if it was, I would require that as an axiom for the equivalent of Eq in our formal setting (I'm using the proof assistant Isabelle/HOLCF [1]). Afterwards only types for which one could prove commutativity could be instances of Eq. But if there where already "standard" instances which violated this requirement, adding it in the formal setting would prevent it from being applicable to "standard" Haskell programs. Indeed, the standard wisdom is that Eq ought to denote an equivalence relation. However, the instance for Double and Float is not an equivalence relation. This is "necessary" due to Double/Float vaguely matching the IEEE-754 spec which requires that NaN /= NaN. If NaN is removed, I think Double/Float ought to behave as desired--- though there was a recent kerfluffle about the fact that the CPU-internal representation of Double/Float has more bits of precision than the in-memory representation, so vagaries about when values leave registers to be stored in memory will affect whether two values come out to be equal or not. Not to mention that Float/Double violate numerous laws of other classes; e.g., Ord is not a total ordering because of NaN; Num is not a ring because addition and multiplication are not associative (they are commutative though);... Depending on what your goals are, it may be best to avoid the entire cesspool of floating point numbers. It would limit the applicability of your work, though if analysis of number crunching isn't your goal then it's a legitimately pragmatic option. Another point to bear in mind is that even though Eq is widely recognized as denoting an equivalence relation, people sometimes willfully subvert this intention. I'm thinking in particular of the fact that the Num class has, until recently, required an Eq instance--- which in turn precludes some useful/cute Num instances like lifting Num operations over (Num b => a -> b), or implementing powerseries as infinite lists, etc. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
[Re-sent as my first post did not make it through.] Hi Christian, Am Mittwoch, den 25.07.2012, 10:19 +0900 schrieb Christian Sternagel: > Btw: Isabelle/HOLCF unifies all error values and nontermination in a > single bottom element _|_. Currently we are using the following axioms > for our formal Eq class (where I'm using Haskell syntax although the > real sources [2] use Isabelle/HOLCF syntax which is slightly different; > (=) is meta-equality). > >(x == y) = True ==> x = y >(x == y) = False ==> not (x = y) >(x == _|_) = _|_ >(_|_ == y) = _|_ I am slightly worried about the latter two; after all one might find it reasonable to specify instance Eq () where _ == _ = True or, maybe slightly more sensible instance Eq Void where _ == _ = True But I checked and both the instances of (), the instance of Data.Void (in the void package) and the derived instance for empty data types are strict: Prelude> data V Prelude> :set -XStandaloneDeriving Prelude> deriving instance Eq V Prelude> (error "1" :: V) == (error "2" :: V) *** Exception: Void == Greetings, Joachim -- Joachim Breitner e-Mail: m...@joachim-breitner.de Homepage: http://www.joachim-breitner.de Jabber-ID: nome...@joachim-breitner.de signature.asc Description: This is a digitally signed message part ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
On 7/25/12, Christian Sternagel wrote: > Dear Alexander, > > On 07/26/2012 01:09 PM, Alexander Solla wrote: >> On 7/25/12, Christian Sternagel wrote: >>> 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). >> >> Indeed. This is true for the interpretation of any function. But you >> apparently want to treat (==) as equality. This may or may not be >> possible, depending on the interpretation you choose. Does _|_ == >> _|_, or _|_ =/= _|_, or do these questions not even make semantic >> sense in the object language? That's what you need to answer, and the >> solution to your problem will become clear. Note that picking any of >> these commits you to a "philosophical" position, insofar as the >> commitment will induce a metalanguage which excludes expressions from >> other metalanguages. > for my specific case (HOLCF) there is already a fixed metalanguage which > has logical equality (=) and differentiates between type 'bool' (True, > False) for logical truth and type 'tr' (TT, FF, _|_) for truth-valued > computable functions (including nontermination/error). Logical equality > satisfies '_|_ = _|_'. Now in principle (==) is just an arbitrary > function (for each instance) but I gather that there is some intended > use for the type class Eq (and I strongly suspect that it is to model > equality ;), I merely want to find out to what extend it does so). Yes, in my opinion, its purpose is to model mathematical/logical equality. That said, you brought up a very important point which you need to address. I'll discuss it more below. I will be using scare-quotes quite a bit. I'm not being sarcastic -- please ask if you don't understand what I mean. > > Currently the axioms of the formal eq class include > > (_|_ == y) = _|_ > (x == _|_) = _|_ > > (and this decision was just based on how ghci evaluates corresponding > expressions). > > The equations you use above would be (roughly) written '(_|_ == _|_) = > TT' and '(_|_ /= _|_) = TT' in HOLCF and neither of them is satisfied, > since both expressions are logically equivalent to _|_ (in HOLCF). (But > still both expressions make sense.) Okay, you have a metalanguage. And it places limits on what you can express. But you can also put limits on what you can express, to induce a sublanguage of the metalanguage. I don't know how "natural" this idea is given your circumstances and goals, but you may want to consider it. I promise I'll get to the meat of my email soon. > > During the discussion I revisited the other two axioms I was using for > eq... and now I am wondering whether those make sense. The other two > axioms where > > (x == y) = TT ==> x = y > (x == y) = FF ==> not (x = y) > > The second one should be okay, but the first one is not true in general, > since it assumes that we would only ever use Eq instances implementing > syntactic equality (which should be true for deriving?). E.g., for the > data type > >data Frac = Frac Int Int > > we would have 'not (Frac 1 2 = Frac 2 4)' in HOLCF (since we have > injectivity of all constructors). But nobody prevents a programmer from > writing an Eq instance of Frac that compares 'normal forms' of fractions. Now, /this/ is an example of what I've been trying to get at. (To be fair, it's a generalization of what I've been trying to get at) You put it in "behavioral" terms -- "nothing stops a programmer", whereas I've been trying to put it in "interpretive" terms (... is ..., but ... means many things -- you have to pick an interpretation) A hypothetical programmer can write: > data Fraction = Fraction Int Int > data Rational = Rational Int Int and have different semantics for each. In particular, we should treat Fraction 1 2 to be distinct from Fraction 2 4, /as fractions/. And Rational 1 2 should be the same as Rational 2 4, /as rational numbers/. These "implied" semantics are just as important as the minimum Haskell demands (in my opinion). The minimum Haskell demands is not (and cannot) be rich enough to distinguish between intentions/intensions. "Obviously", Fraction and Rational are intimately related (the rationals "should" be a ring of fractions in "normal form"). And functions between Fraction and Rational "should" preserve the "correct" relationships. But, what are these? We can come up with theorems, but some things are nothing but the programmer/mathematician's choice. In other words, by choosing a semantic where (Rational 1 2) == (Rational 2 4), a programmer/mathematician has *generated* a sublanguage of Haskell by imposing his *intended* semantics. This is an example of "intensions" versus "extensions" in logic. So, your task is... difficult. From my point of view,
Re: [Haskell-cafe] Is (==) commutative?
Dear Alexander, On 07/26/2012 01:09 PM, Alexander Solla wrote: On 7/25/12, Christian Sternagel wrote: 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). Indeed. This is true for the interpretation of any function. But you apparently want to treat (==) as equality. This may or may not be possible, depending on the interpretation you choose. Does _|_ == _|_, or _|_ =/= _|_, or do these questions not even make semantic sense in the object language? That's what you need to answer, and the solution to your problem will become clear. Note that picking any of these commits you to a "philosophical" position, insofar as the commitment will induce a metalanguage which excludes expressions from other metalanguages. for my specific case (HOLCF) there is already a fixed metalanguage which has logical equality (=) and differentiates between type 'bool' (True, False) for logical truth and type 'tr' (TT, FF, _|_) for truth-valued computable functions (including nontermination/error). Logical equality satisfies '_|_ = _|_'. Now in principle (==) is just an arbitrary function (for each instance) but I gather that there is some intended use for the type class Eq (and I strongly suspect that it is to model equality ;), I merely want to find out to what extend it does so). Currently the axioms of the formal eq class include (_|_ == y) = _|_ (x == _|_) = _|_ (and this decision was just based on how ghci evaluates corresponding expressions). The equations you use above would be (roughly) written '(_|_ == _|_) = TT' and '(_|_ /= _|_) = TT' in HOLCF and neither of them is satisfied, since both expressions are logically equivalent to _|_ (in HOLCF). (But still both expressions make sense.) During the discussion I revisited the other two axioms I was using for eq... and now I am wondering whether those make sense. The other two axioms where (x == y) = TT ==> x = y (x == y) = FF ==> not (x = y) The second one should be okay, but the first one is not true in general, since it assumes that we would only ever use Eq instances implementing syntactic equality (which should be true for deriving?). E.g., for the data type data Frac = Frac Int Int we would have 'not (Frac 1 2 = Frac 2 4)' in HOLCF (since we have injectivity of all constructors). But nobody prevents a programmer from writing an Eq instance of Frac that compares 'normal forms' of fractions. cheers chris ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
On 7/25/12, Christian Sternagel wrote: > 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). Indeed. This is true for the interpretation of any function. But you apparently want to treat (==) as equality. This may or may not be possible, depending on the interpretation you choose. Does _|_ == _|_, or _|_ =/= _|_, or do these questions not even make semantic sense in the object language? That's what you need to answer, and the solution to your problem will become clear. Note that picking any of these commits you to a "philosophical" position, insofar as the commitment will induce a metalanguage which excludes expressions from other metalanguages. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
Sorry, I forgot to reply to the list. On 07/26/2012 11:53 AM, Alexander Solla wrote: (consider, e.g., 'head undefined' vs. 'head [undefined]') This was a typo, I meant 'tail undefined' vs. 'tail [undefined]'. I'm not arguing one way or the other (I know what I do, unless there's a need to do the other). What I'm saying is there are lots of ways to interpret a language, and we can choose between them. If you want to analyze Haskell, you will have to choose an interpretation for it. Haskell, as a logic, is paraconsistent (i.e., it's unsound. So your theory for Haskell either needs to keep contradiction in the object language (the "partial" case where we do not identify bottoms) or take it out of the object language and put it into the analytical meta-language. The intention is not to use Haskell as a logic, but to use an existing logic (HOLCF, reference in an earlier mail; thus the interpretation is already fixed to a high degree) to formally verify Haskell programs. In order to do that the program to be verified has to be "rewritten" inside the logic and everything that is proved about this "formal variant" of the program should be transferable to the real program (assuming that "Haskell's semantics" was captured correctly). Another problem is if the formalization is too strict, i.e., requires properties from functions that are not satisfied in practice and that's where my original question about commutativity of (==) came from. If there are "reasonable" Haskell programs for which (==) is non-commutative, we should not require it, since we could not formalize those programs then. cheers chris The classically valid inference: (x == y) = _|_ => (y == x) = _|_ On 7/25/12, Christian Sternagel wrote: Dear Alexander, Let me clarify again: by "we identify all bottoms" I mean that any error and also nontermination is identified with _|_ . However, I did not mean that [_|_] is identified with _|_ (since the point of a formal treatment is exactly to correctly consider the lazy semantics of Haskell). In Haskell there definitely is a difference between 'undefined' and '[undefined]' (consider, e.g., 'head undefined' vs. 'head [undefined]') so this must be taken in to account in a rigorous treatment. Btw: I didn't get which inference you meant when you where saying it is "classically valid". cheers chris On 07/26/2012 11:13 AM, Alexander Solla wrote: Depending on the context, it may or may not be wise to distinguish between undefined and [undefined]. This is a matter of strictness, laziness, and totality. If you identify all bottoms as one, you essentially restrict yourself to (what might as well be, for the purposes of this discussion) a strict subset of the Haskell language. If you distinguish between values that "contain" bottom and "are" bottom, then you need to deal with the semantics of laziness. Like I said, it is classically valid, so choosing these semantics means that it will be safe. But the undecidability of comparing distinct bottoms means that you have to make a choice. On 7/24/12, Christian Sternagel wrote: It's a classically valid inference, so you're "safe" in that respect, and it is true that evaluating x == y requires traversing x and y, so that if x or y "are" bottom, (x == y) and (y == x) will both be bottom. Well, (x == y) could result in bottom, even if neither x nor y are bottom, e.g., [undefined] == [undefined]. -cheers chris ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
Dear Alexander, Let me clarify again: by "we identify all bottoms" I mean that any error and also nontermination is identified with _|_ . However, I did not mean that [_|_] is identified with _|_ (since the point of a formal treatment is exactly to correctly consider the lazy semantics of Haskell). In Haskell there definitely is a difference between 'undefined' and '[undefined]' (consider, e.g., 'head undefined' vs. 'head [undefined]') so this must be taken in to account in a rigorous treatment. Btw: I didn't get which inference you meant when you where saying it is "classically valid". cheers chris On 07/26/2012 11:13 AM, Alexander Solla wrote: Depending on the context, it may or may not be wise to distinguish between undefined and [undefined]. This is a matter of strictness, laziness, and totality. If you identify all bottoms as one, you essentially restrict yourself to (what might as well be, for the purposes of this discussion) a strict subset of the Haskell language. If you distinguish between values that "contain" bottom and "are" bottom, then you need to deal with the semantics of laziness. Like I said, it is classically valid, so choosing these semantics means that it will be safe. But the undecidability of comparing distinct bottoms means that you have to make a choice. On 7/24/12, Christian Sternagel wrote: It's a classically valid inference, so you're "safe" in that respect, and it is true that evaluating x == y requires traversing x and y, so that if x or y "are" bottom, (x == y) and (y == x) will both be bottom. Well, (x == y) could result in bottom, even if neither x nor y are bottom, e.g., [undefined] == [undefined]. -cheers chris ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
Depending on the context, it may or may not be wise to distinguish between undefined and [undefined]. This is a matter of strictness, laziness, and totality. If you identify all bottoms as one, you essentially restrict yourself to (what might as well be, for the purposes of this discussion) a strict subset of the Haskell language. If you distinguish between values that "contain" bottom and "are" bottom, then you need to deal with the semantics of laziness. Like I said, it is classically valid, so choosing these semantics means that it will be safe. But the undecidability of comparing distinct bottoms means that you have to make a choice. On 7/24/12, Christian Sternagel wrote: >> It's a classically valid inference, so you're "safe" in that respect, >> and it is true that evaluating x == y requires traversing x and y, so >> that if x or y "are" bottom, (x == y) and (y == x) will both be bottom. > Well, (x == y) could result in bottom, even if neither x nor y are > bottom, e.g., [undefined] == [undefined]. -cheers chris > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
It's a classically valid inference, so you're "safe" in that respect, and it is true that evaluating x == y requires traversing x and y, so that if x or y "are" bottom, (x == y) and (y == x) will both be bottom. Well, (x == y) could result in bottom, even if neither x nor y are bottom, e.g., [undefined] == [undefined]. -cheers chris ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
Dear all, Thanks for your replies. Just to clarify: I am fully aware that inside Haskell there is no guarantee that certain (intended) requirements on type class instances are satisfied. I was asking whether the intention for Eq is that (==) is commutative, because if it was, I would require that as an axiom for the equivalent of Eq in our formal setting (I'm using the proof assistant Isabelle/HOLCF [1]). Afterwards only types for which one could prove commutativity could be instances of Eq. But if there where already "standard" instances which violated this requirement, adding it in the formal setting would prevent it from being applicable to "standard" Haskell programs. Btw: Isabelle/HOLCF unifies all error values and nontermination in a single bottom element _|_. Currently we are using the following axioms for our formal Eq class (where I'm using Haskell syntax although the real sources [2] use Isabelle/HOLCF syntax which is slightly different; (=) is meta-equality). (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. The question is whether we should also add. (x == y) = _|_ ==> (y == x) = _|_ Which would directly imply (x == y) = (y == x) cheers chris [1] http://isabelle.in.tum.de (and http://isabelle.in.tum.de/dist/library/HOL/HOLCF/) [2] http://sourceforge.net/p/holcf-prelude ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
On 24/07/12 14:44, timothyho...@seznam.cz wrote:
There's always this, for ALL types a :( So even where you would think that the
documentation can claim that a given Eq instance follows the law of
commutativity, it really cannot.
Once you invoke unsafePerformIO, you can break the type system, and probably
execute random assembly code and write to any memory location. So, at this point
all bets for the rest of the program are of. It is up to the programmer to
verify that all the necessary invariants still hold when you do unsafe stuff.
In other words, the issue here is not with a particular Eq instance, it is with
unsafePerformIO.
Essentially `unsafePerformIO (x :: IO Int)` is not really an Int, but rather a
value that behaves like one in most but not all cases.
Also, let a = unsafePerformIO x in (a,a) is *not* the same thing as
(unsafePerformIO x,unsafePerformIO x). For your entertainment:
λ> do m <- newEmptyMVar ;putMVar m 1 ; let {a =(unsafePerformIO (do v <-
takeMVar m; putMVar m 2; return v)); b = (unsafePerformIO (do v <- takeMVar m;
putMVar m 1 ; return v))} ; print (a == b); print (b == a)
False
False
Twan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
On 24/07/12 14:39, Jonas Almström Duregård wrote: Hi, I suppose you need to define what commutativity means in the presence of undefined values. For instance if error "0" is different from error "1" then you do not have commutativity. Also nontermination needs to be considered, for instance "(fix $ \x->x) == undefined" typically fails to terminate but "undefined == (fix $ \x->x)" typically yields an error. Regards, Jonas In the usual Haskell semantics, all bottoms are considered to be the same. In other words, there is only one. You could implement this by setting undefined to nontermination, and error _ = undefined. In fact, the Haskell report does exactly this. Any error messages you get are only visible in IO land, where anything can happen anyway. So _|_ == x = _|_ holds for (almost) all types, except perhaps for (). Though in practice also undefined == () = undefined. Twan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
There's always this, for ALL types a :( So even where you would think that the documentation can claim that a given Eq instance follows the law of commutativity, it really cannot. Prelude Control.Concurrent System.IO.Unsafe> do m <- newEmptyMVar ;putMVar m 1 ; print $ (unsafePerformIO (do v <- takeMVar m; putMVar m 2; return v)) == (unsafePerformIO (do v <- takeMVar m; putMVar m 1 ; return v)) ; print $ (unsafePerformIO (do v <- takeMVar m; putMVar m 1; return v)) == (unsafePerformIO (do v <- takeMVar m; putMVar m 2 ; return v)) False True -- Původní zpráva -- Od: Jonas Almström Duregård Datum: 24. 7. 2012 Předmět: Re: [Haskell-cafe] Is (==) commutative? "Hi, I suppose you need to define what commutativity means in the presence of undefined values. For instance if error "0" is different from error "1" then you do not have commutativity. Also nontermination needs to be considered, for instance "(fix $ \x->x) == undefined" typically fails to terminate but "undefined == (fix $ \x->x)" typically yields an error. Regards, Jonas On 24 July 2012 10:10, Christian Sternagel wrote: > Dear all, > > with respect to formal verification of Haskell code I was wondering whether > (==) of the Eq class is intended to be commutative (for many classes such > requirements are informally stated in their description, since Eq does not > have such a statement, I'm asking here). Or are there any known cases where > commutativity of (==) is violated (due to strictness issues)? > > cheers > > chris > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe (http://www.haskell.org/mailman/listinfo/haskell-cafe) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe (http://www.haskell.org/mailman/listinfo/haskell-cafe)"___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
Hi, I suppose you need to define what commutativity means in the presence of undefined values. For instance if error "0" is different from error "1" then you do not have commutativity. Also nontermination needs to be considered, for instance "(fix $ \x->x) == undefined" typically fails to terminate but "undefined == (fix $ \x->x)" typically yields an error. Regards, Jonas On 24 July 2012 10:10, Christian Sternagel wrote: > Dear all, > > with respect to formal verification of Haskell code I was wondering whether > (==) of the Eq class is intended to be commutative (for many classes such > requirements are informally stated in their description, since Eq does not > have such a statement, I'm asking here). Or are there any known cases where > commutativity of (==) is violated (due to strictness issues)? > > cheers > > chris > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
On 24/07/12 13:32, Frank Recker wrote: I agree, that (==) should be symmetric. However, it is easy to write Eq-instance, which violates this law: It is impossible to specify laws such as symmetry in Haskell, which is why they are usually stated in the documentation. However, this style of documentation is a relatively recent trend (last 5 years or so). I suspect that is why the documentation for the Eq class does not specify the laws for an equivalence relation. So in your formal verification, the symmetric property of every Eq-instance has to be an axiom. An alternative for equational reasoning is to not use Eq, but just directly use syntactic equality. I.e. write (=) instead of (==). > I frankly don't know, whether the Haskell specification says > anything about this. I checked, and it doesn't say anything about laws for Eq instances. The closest it comes is with the remark that "The Ord class is used for totally ordered datatypes", but there is no requirement that Ord and Eq be coherent, or even that (==) and (/=) are coherent. Twan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
Forgot to copy the list. Sorry for the duplicates :( On Jul 24, 2012 1:35 PM, "Tristan Seligmann" wrote: > On Jul 24, 2012 12:32 PM, "Twan van Laarhoven" wrote: > > > > On 2012-07-24 10:10, Christian Sternagel wrote: > >> > >> Dear all, > >> > >> with respect to formal verification of Haskell code I was wondering > whether (==) > >> of the Eq class is intended to be commutative (for many classes such > >> requirements are informally stated in their description, since Eq does > not have > >> such a statement, I'm asking here). Or are there any known cases where > >> commutativity of (==) is violated (due to strictness issues)? > > > > > > Strictness plays no role for Eq, since to test for equality both sides > will have to be fully evaluated. > > I don't think this is necessarily true. For example: > > (==) :: (Eq a) => Maybe a -> Maybe a -> Bool > Nothing == Nothing = True > Nothing == Just _ = False > Just _ == Nothing = False > Just x == Just y = x == y > > This particular example is still commutative, however (at least I think it > is). > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
On Tue, July 24, 2012 12:30, Twan van Laarhoven wrote: > On 2012-07-24 10:10, Christian Sternagel wrote: >> Dear all, >> >> with respect to formal verification of Haskell code I was wondering >> whether (==) >> of the Eq class is intended to be commutative (for many classes such >> requirements are informally stated in their description, since Eq does >> not have >> such a statement, I'm asking here). Or are there any known cases where >> commutativity of (==) is violated (due to strictness issues)? > > Strictness plays no role for Eq, since to test for equality both sides > will have > to be fully evaluated. I think (==) is supposed to be equivalence > relation, > which is symmetric (i.e. commutative); as well as reflexive and > transitive. > > There are some cases of (==) not being reflexive, Floats being the most > notable > one, but many people consider that to be a bug. I can't think of any > instances > that violate symmetry. I agree, that (==) should be symmetric. However, it is easy to write Eq-instance, which violates this law: -- begin code data Foo = Foo Int deriving Show instance (Eq Foo) where (==) (Foo x) (Foo y) | x==0 = False | x==1 = True | otherwise = False value_1 = Foo 0 value_2 = Foo 1 compare_1 = value_1 == value_2 compare_2 = value_2 == value_1 -- end code compare_1 is False whereas compare_2 is True. So in your formal verification, the symmetric property of every Eq-instance has to be an axiom. I frankly don't know, whether the Haskell specification says anything about this. Frank ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is (==) commutative?
On 2012-07-24 10:10, Christian Sternagel wrote: Dear all, with respect to formal verification of Haskell code I was wondering whether (==) of the Eq class is intended to be commutative (for many classes such requirements are informally stated in their description, since Eq does not have such a statement, I'm asking here). Or are there any known cases where commutativity of (==) is violated (due to strictness issues)? Strictness plays no role for Eq, since to test for equality both sides will have to be fully evaluated. I think (==) is supposed to be equivalence relation, which is symmetric (i.e. commutative); as well as reflexive and transitive. There are some cases of (==) not being reflexive, Floats being the most notable one, but many people consider that to be a bug. I can't think of any instances that violate symmetry. Twan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Is (==) commutative?
Dear all, with respect to formal verification of Haskell code I was wondering whether (==) of the Eq class is intended to be commutative (for many classes such requirements are informally stated in their description, since Eq does not have such a statement, I'm asking here). Or are there any known cases where commutativity of (==) is violated (due to strictness issues)? cheers chris ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
