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

Fri Jun 22 03:52:06 CEST 2012

On Thu, Jun 21, 2012 at 8:30 AM, George Giorgidze <giorgidze at gmail.com> wrote:
> Hi Derek,
>
> Thanks for providing the executable example that demonstrates your
> point. It is an interesting one. See my response below. I think it
> takes us into the discussion as to what constitutes reasonable/law
> abiding instances of Eq and Ord and what client code that uses Eq and
> Ord instances can assume.
>
> To give out my point in advance, Eq and Ord instances similar to yours
> (i.e., those that proclaim two values as equal but at the same time
> export or allow for function definitions that can observe that they
> are not equal; that is, to tell them apart) not only break useful
> properties of the Data.Set.Monad wrapper but they also break many
> useful properties of the underlaying Data.Set, and many other standard
> libraries and functions.

I will readily admit that the Ord instance arguably does not satisfy
the laws one would want (though it is consistent with the Eq
instance).  It arguably is supposed to produce a total order which it
does not.  However, Eq is only required to be an equivalence relation
(and even that is stretching the definition of "required"), and the Eq
instance is certainly an equivalence relation.  Furthermore, the only
reason your library requires an Ord instance is due to the underlying
Data.Set requiring it.  You could just as well use a set
implementation that didn't require Ord and the same issue would occur.
 I mention this to remove the "bad" Ord instance from consideration.

For me saying two Haskell expressions are equal means observation
equality.  I.e. I can -always- substitute one for the other in any
context.  I tolerate "equal" meaning "equal modulo bottom", because
unless you are catching asynchronous exceptions, which Haskell 2010
does not support, the only difference is between whether you get an
answer or not, not what that answer is if you get it which is only so
harmful.  For Data.Set.Monad, fmap f . fmap g = fmap (f . g) holds (at
least modulo bottom) for all f and g as required by the Functor laws.

I have no problem if you want to say fromList . toList = id -given-
(==) is the identity relation on defined values, but omitting the
qualification is misleading and potentially dangerous.  The Haskell
Report neither requires nor enforces that those relations hold, which
is particularly underscored by the fact, as you yourself demonstrated
that even -standard- types fail to satisfy even the laws that you
perhaps can interpret the Haskell Report as requiring.  There have
been violations of type safety due to assuming instances satisfied
laws that they didn't.

>
> On 20 June 2012 04:03, Derek Elkins <derek.a.elkins at gmail.com> wrote:
>>
>> This is impressive because it's false.  The whole point of my original
>> response was to justify Dan's intuition but explain why it was misled
>> in this case.
>>
>
> No, In my opinion, it is not false. The fact that you need to wrap the
> expression between fmap f and fmap g suggests that the problem is with
> mapping the functions f and g and not with toList and fromList as you
> suggest. See below for clarifications.
>
> Let us concentrate on the ex4 and ex6 expressions in your code. These
> two most clearly demonstrate the issue.
>
>> import Data.Set.Monad
>>
>> data X = X Int Int deriving (Show)
>>
>> instance Eq X where
>>    X a _ == X b _ = a == b
>>
>> instance Ord X where
>>    compare (X a _) (X b _) = compare a b
>>
>> f (X _ b) = X b b
>>
>> g (X _ b) = X 1 b
>>
>> xs = Prelude.map (\x -> X x x) [1..5]
>>
>> ex4 = toList $ fmap f . fmap g $ fromList xs
>>
>> ex6 = toList $ fmap f . fromList . toList . fmap g $ fromList xs
>
> print ex4 gives us [X 1 1,X 2 2,X 3 3,X 4 4,X 5 5]
>
> and
>
> print ex6 gives us [X 5 5]
>
> From the first look, it looks like that (fromList . toList) is not
> identity. But if tested and checked separately it is. Maybe something
> weird is going on with (fmap f) and (fmap g) and/or their composition.
> Before we dive into that let us try one more example:
>
> ex7 = toList $ fmap f . (empty `union`) . fmap g $ fromList xs
>
> print ex7 just like ex6 gives us [X 5 5] should we assume that (empty
> `union`) is not identity either?

Correct.  It is not.

This hints that, probably something
> is wrong with (fmap f), (fmap g), or their composition.
>
> Let us check.
>
> If one symbolically evaluates ex4 and ex6 (I did it with pen and paper
> and I am too lazy to type it here), one can notice that:
>
> ex4 boils down to evaluating Data.Set.map (f . g) (Data.Set.fromList xs)
>
> while
>
> ex6 boils down to evaluating Data.Set.map f (Data.Set.map g
> (Data.Set.fromList xs))
>
> (BTW, is not it great that Data.Set.Monad managed to fuse f and g for ex4)
>
> So for your Eq and Ord instances and f and g functions the following
> does not hold for the underlaying Data.Set library:
>
> map f . map g = map (f . g)
>
> So putting identity functions like (fromList . toList) or (empty
> `union`) prevents the fusion and allows one to observe that (map f .
> map g) is not the same  as (map (f . g)) for the underlaying Data.Set
> and for your particular choice of f and g.
>
> This violates the second functor law. So does this mean that I (and
> few other people [1, 2]) should not have attempted to turn Set into a
> functor? I do not think so.

You didn't turn Data.Set.Set into a Functor.  You turned
Data.Set.Monad.Set into a Functor, and (modulo bottom) it indeed is
one.  It pretty much is one regardless of what the "underlying" type
is.  Rather little is required from the underlying type.  That's why
this technique works generally.  As an exercise, you can see what laws
are actually required from Data.Set.Set for this to be a monad.

>
> (BTW, what distinguishes the approach used in Data.Set.Monad from
> other efforts is that it does not require changes in the definitions
> of standard Functor and Monad type classes).
>
> In my opinion, the problem here lies with the Eq and Ord instances of
> the X data type AND with the function f that can tell apart two values
> that are proclaimed to be equal by the Eq instance. As I said, such
> instances and accompanied functions not only break useful properties
> of Data.Set.Monad, but also useful properties of the library that
> underlies it (i.e., the original Data.Set), and possibly many other
> standard libraries and functions (see [4]).

It certainly is the case that a lot of the laws are conditional on the
satisfaction of laws on the used instances.

>
> Putting the functor laws aside, there are even more fundamental
> set-oriented properties that can be broken by Ord instances that are
> not law abiding. See the following GHCi session taken from [3]:
>
> Prelude> import Data.Set
> Prelude Data.Set> let x = fromList  [0, -1, 0/0, -5, -6, -3] :: Set Float
> Prelude Data.Set> member 0 x
> True
> Prelude Data.Set> let x' = insert (0/0) x
> Prelude Data.Set> member 0 x'
> False
>
> Is this because Data.Set is broken? No, in my opinion, this is because
> the Ord instance of Float does not satisfy the Ord laws (about total
> order).

Actually, it's worse than that.  (==) on Float doesn't even satisfy
being an equivalence relation.

>
> To summarise, in my opinion the problem here lies with the fact that
> the Eq and Ord instances for the X data type proclaim two values as
> equal when it can be easily observed that they are not equal (in this
> case with the function f). Note, that the functions of Data.Set.Monad
> and Data.Set rely on your Eq and Ord instances.
>
> Of course, there would be nothing wrong with the Eq and Ord instances
> for X as long as you would export it as abstract data type and you
> would not export functions that can observe two values to be different
> when your Eq instance says they are equal. One could also clearly mark
> functions that can tell two equal (in the sense of Eq) values apart as
> unsafe (perhaps maybe even in the SafeHaskell sense).
>
> The opinions may differ, but I think the raised issue is more about
> what the specifications of Eq and Ord should be and what the client
> code that uses Eq and Ord instance can assume. There has been a long
> discussion on this topic [4].
>
> Again the opinions may differ, but I think in this case the problem
> lies with the Eq and Ord instances for the X data type and not with
> the Data.Set.Monad and (its underlaying) Data.Set libraries.
>
> Derek and Dan, thanks for the interesting example. I would be
> interested to hear whether you have an example that could potentially
> break set-oriented, and/or monad and functor laws for element types
> where Eq instance respects observational equality and Ord instance
> respects total order.
>
> Cheers, George
>
> [1] http://www.haskell.org/pipermail/haskell-cafe/2010-July/080977.html
> [2] http://haskell.1045720.n5.nabble.com/Functor-instance-for-Set-td5525789.html
> [3] http://stackoverflow.com/questions/6399648/what-happens-to-you-if-you-break-the-monad-laws
> [4] http://www.haskell.org/pipermail/haskell-cafe/2008-March/thread.html