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

[George Giorgidze]

Hi Dan,

On 21 June 2012 04:21, Dan Burton <danburton.email at gmail.com> 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 <giorgidze at gmail.com>
> 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
>
>