Re: [Haskell-cafe] [Haskell] ANNOUNCE: set-monad

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