Hi Dan, On 21 June 2012 04:21, Dan Burton wrote:

Hi George,

I didn't have access to my computer over the weekend, so I apologize for not actually running the examples I provided. I was simply projecting what I thought could reasonably be assumed about the behavior of a Set.

Derek attempted to clarify your points and also provided executable examples. I think his code is closely related and raises similar issues to what you have just provided.

Data.Set.Monad's departure from those assumptions is a double-edged sword, and so I'd just like to clarify a couple things.

I disagree on this. I think these particular Eq and Ord instances are double-edged swords (and rather dangerous ones) especially in the set-oriented code where almost every set-oriented function relies on correct behaviour of functions related to equality and ordering. As I have pointed out in my previous email (in response to Derek's email) these particular instances not only break useful properties of Data.Set.Monad, but they also break useful properties of the underlaying Data.Set library (and useful properties of many other standard libraries and functions too, see [1]).

Regarding antisymmetry, if I also define

instance Ord Foo where   (==) = (==) `on` a

then would that count as satisfying the law?

Probably, you mean here Eq instead of Ord. If a <= b and b <= a then a = b (antisymmetry) It all depends on what one means by "=". Opinions differ on this, see [1]. If we mean "==", which is a function to Bool, from the Eq class, then it does satisfy the antisymmetry law. But in this case, the question arises what are the laws that Eq instances should satisfy. Should it be that x == y implies x = y? But once again what does "=" mean here. It depends on who you ask (once again see [1]). But, my opinion is that if you can write a pure function f that can tell them apart (i.e., f x /= f y), I find it a very strange notion of equality. And this is actually what breaks many useful properties of Data.Set.Monad, as well as, Data.Set.

In any event, I find it an amusing coincidence that Data.Set.Monoid does essentially the same thing as Foo: it retains some extra information, and provides an Eq instance that asserts equality modulo dropping the extra information.

No, it does not. Data.Set.Monad hides the internal representation of the Set data type and does not export functions that can inspect its internal representation. (There are a few functions like showTree that allow inspection of the structure, but such functions are clearly marked). In other words, the Set data type is exported as an abstract data type. In contrast, the structure of the Foo data type is exposed and functions are explicitly provided that tell apart two values that are proclaimed to be equal by the Eq instance. As it turns out (demonstrated by Derek and yourself) such questionable Eq instances can be used to confuse the Data.Set.Monad and Data.Set libraries.

So I have a question and a concern. Loading this file into ghci: hpaste.org/70245

ghci> foo1 == foosTransform1 True ghci> foo2 == foosTransform2 False

given x == y, where x and y are Sets, we cannot guarantee that fmap f x == fmap f y, due to the extra information retained for the sake of obeying functor laws.

My question is this: how does the library manage to obey functor laws?

It simply assumes that (map f) . (map g) = map (f . g) for the underlaying primitive set type and evaluates ((fmap f) . (fmap g)) as (fmap (f . g)). You cannot directly see the aforementioned evaluation steps in the run function. Instead, please expand the definition of fmap in terms of Bind and Return and follow the evaluation rules using Bind's associativity and Return's left identity.

My concern is this: the aforementioned behavior should be clearly documented in the haddocks. Presumably, people will not know about the extra information being retained. The following, out of context (where most debugging happens), could be quite confusing:

ghci> foosTransform1 fromList [Foo {a = 1, b = 4}] ghci> fmap restoreA foosTransform1 fromList [Foo {a = 1, b = 1},Foo {a = 2, b = 2},Foo {a = 3, b = 3},Foo {a = 4, b = 4}]

The data seems to pop out of nowhere. Even if Ord instances like the one for Foo shouldn't exist, they almost certainly will anyways, because the Haskell type system doesn't prevent them. Users of the library should be informed accordingly.

I agree, it should be documented that the library relies on (map f) . (map g) = map (f . g) to hold for Data.Set, for those (I would still call them questionable) Eq and Ord instances where the above property does not hold things break in the Data.Set.Monad library as well. Having said that, questionable Eq instances break so many other functions in other standard libraries [1], that documenting every such case would be a significant undertaking. My opinion is to informally impose restrictions on Eq and Ord instances instead, just like we do for Functor, Applicative, Monad and other type classes, and imply that those restrictions are met when talking about specific function properties that have Eq or Ord constraints. I am not saying that this is a trivial undertaking, but would be a more principled approach. It would require the Haskell community and, especially, standard library and language specification developers to agree on a suitable notion of equality that Eq instances should satisfy. Cheers, George

Dan Burton 801-513-1596

On Mon, Jun 18, 2012 at 2:40 PM, George Giorgidze wrote:

...

Hi Dan,

Thanks for your feedback and your question regarding the functor laws.

Please try your example in GHCi and/or evaluate it by hand. The library does not violate the functor laws.

I committed quick check properties for functor laws, as well as, laws for other type classes to the repo. You can give it a try. It is also possible, with a little bit of effort, to prove those properties by hand.

Speaking of laws, BTW, your contrived Ord instance violates one of the Ord laws. The documentation for Ord says that: "The Ord class is used for totally ordered datatypes". Your definition violates the antisymmetry law [1]:

If a <= b and b <= a then a == b

by reporting two elements that are not equal as equal.

Cheers, George

[1] http://en.wikipedia.org/wiki/Totally_ordered

Hi Alexander, Thanks for commenting on this issue. On 21 June 2012 16:34, Alexander Solla wrote:

These nits don't need to be picked.  The theory of equivalence relations is extremely well understood.  This is a topic covered by the sophomore mathematics level.

I did not say that the theory of equivalence relations is not well understood. All I have said is that [1] demonstrates that people have different ideas as to what an Eq instance should satisfy. And, yes, it is all about picking a suitable notion for Eq and designating other (possibly related and useful) notions for other type classes. Being an equivalence relation is just one of them. But, to be honest, I find this rather confusing. I thought, and I suspect I am not the only one, Eq was about equality and not about equivalence. I have just had a look at the Haskell 2010 and Prelude. When it comes to the Eq type class, precise definition of what its instances should satisfy is missing. But crucially, both texts talk about equality and not about equivalence. The word equivalence is not even mentioned in the context of the Eq class. This may sound to much of a technical/terminological point, but I believe the terminology we use is important, especially, in the context of Haskell where formal reasoning about programs is not unusual. Also, I find the use of the == symbol to denote equivalence rather than equality rather questionable. The way lhs2tex typesets the == symbol, makes this even more questionable. Again this may sound to much of a symbolical point, but I believe the symbols we use are important, especially, in the context of Haskell where formal reasoning about programs is not unusual. I would like to kindly ask you to provide a reference designating Eq for equivalence and not for equality and stating that only being an equivalence relation is required. Thanks in advance. Why not use the Eq type class (as the current Haskell 2010 and Prelude texts suggest) for a stronger notion of equality (observational equality with a suitable notion of observation is one candidate), and designate weaker notions such as being just an equivalence relation to different type classes?

...

But, my opinion is that if you can write a pure function f that can tell them apart (i.e., f x /= f y), I find it a very strange notion of equality.

There's your problem.

Unfortunately, this is not only my problem. In addition to mailing list discussions I referred to in the earlier email sent to Derek [2,3] (these discussions are about functor and monad instances for sets), a paper by John Hughes about "Restricted Data Types in Haskell" [4] and a draft by Oleg Kiselyov about "Restricted Monads" [5] are also relevant. Both, John and Oleg, use monad instances for sets as primary examples. However, their properties can be easily violated by Eq instances provided by Derek and Dan. John's and Oleg's constructions, for the monad laws to hold, rely on Eq to be equality and not just an equivalence relation.

It is straight-forward to generate an equivalence relation that can tell things apart with respect to a different equivalence relation.  Equivalence relations do not need to agree!

See above, I thought Eq was about equality and not about equivalence.

If you really want to keep distinct equivalence relations apart semantically, just use a newtype wrapper to explicitly "name" the relation.

This is certainly possible. Can you point to a library or a document that exemplifies this approach for dealing with different notions of equality and/or equivalence. Maybe there are already conventions in place that I am not aware of. Thanks in advance.

...

I am not saying that this is a trivial undertaking, but would be a more principled approach. It would require the Haskell community and, especially, standard library and language specification developers to agree on a suitable notion of equality that Eq instances should satisfy.

That has already happened.  A relation merely has to satisfy the equivalence relation axioms.

Can you provide a reference? When this was agreed and where is this specified? Thanks in advance, George [1] http://www.haskell.org/pipermail/haskell-cafe/2008-March/thread.html [2] http://www.haskell.org/pipermail/haskell-cafe/2010-July/080977.html [3] http://haskell.1045720.n5.nabble.com/Functor-instance-for-Set-td5525789.html [4] http://www.cs.utexas.edu/users/ham/richards/FP%20papers/restricted-datatypes... [5] http://okmij.org/ftp/Haskell/types.html#restricted-datatypes