Some clarity please! (was Re: [Haskell-cafe] Re: (flawed?) benchmark : sort)

[kahl at cas.mcmaster.ca]

Adrian Hey <ahey at iee.org> wrote:

 > I would ask for any correct Eq instance something like the law:
 >    (x==y) = True implies x=y (and vice-versa)

The easiest counterexample are sets (or finite maps)
provided as an abstract data type (i.e., exported without access to the
implementation, in particular constructors).

Different kinds of balanced trees typically do not produce the same
representation for the same set constructed by different construction
expressions.

Therefore, (==) on sets will be expected to produce equality of sets,
which will only be an equivalence on set representations.

 > which implies (f x == f y) = True (for expression types which are
 > instances of Eq).

This specifies that (==) is a congurence for f, and is in my opinion
the right specification:  (==) should be a congurence
on all datatypes with respect to all purely defineable functions.

But at least nowadays people occasionally do export functions
that allow access to representation details,
for example Set.toList is not specified to be representation independent,
and Set.showTree is outright specified to be implementation dependent.

Prelude> :m + Data.Set
Data.Set> showTree (fromList [1,2,3,4]) == showTree (fromList [4,3,2,1])
False
Data.Set> fromList [1,2,3,4] == fromList [4,3,2,1]
True

I consider this as an argument to remove showTree from the interface of
Data.Set, and to either specify toList to produce an ordered list
(replacing toAscList), or to remove it from the interface as well.
(mapMonotonic should of course be removed, too,
 or specified to fail (preferably in some MonadZero)
 if the precondition is violated,
 which should still be implementable in linear time.)

 > but if so would like to appeal to movers and shakers in the
 > language definition to please decide exactly what the proper
 > interpretation of standard Eq and Ord "class laws" are and in the
 > next version of the report give an explanation of these

Strongly seconded, inserting ``precise'' before ``explanation'' ;-)

(And I'd expect equivalences and congruences to be accessible
 on the basis of standard first-year math...)



Wolfram