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

Hi folks I'm late into this thread, so apologies if I'm being dim. On 13 Mar 2008, at 16:17, kahl@cas.mcmaster.ca wrote:

Adrian Hey wrote:

...

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

I wish I knew what = meant here. Did somebody say? I don't think it's totally obvious what equational propositions should mean. Nor do I think it's desirable to consider only those propositions expressible in QuickCheck. If = is reflexive and distinguishes undefined from True, then x = y implies (x == y) = True will be tricky to satisfy for quite a lot of types. What about undefined == undefined or repeat 'x' == repeat 'x' ? For some suitable (slightly subtle) definition of "finite", you might manage x finite and x = y implies (x == y) = True One rather intensional definition of x = y might be "x and y have a common n-step reduct" with respect to some suitable operational semantics. I don't think this is what Adrian had in mind, but it certainly falls foul of Wolfram's objection.

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.

This suggests that we should seek to define x = y on a type by type basis, to mean "x and y support the same observations", for some suitable notion of observation, which might depend crucially on what operations are exported from the (notional or actual) module which defines the type. If so, it's clearly crucial to allow some observations which rely on waiting for ever, in order to avoid _|_-induced collapse. Something of the sort should allow this...

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

...but this...

...

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.

...is more troublesome. Take f = repeat. Define f = f. I'd hope x == y = True would give us x = y, and that x == y would be defined if at least one of x and y is finite. That implies f x = f y, which should guarantee that f x == f y is not False.

But at least nowadays people occasionally do export functions that allow access to representation details,

[..]

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.

Perhaps that's a little extreme but I agree with the sentiment. How about designating such abstraction- breaking functions "nosy", in the same way that functions which might break purity are "unsafe".

(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.)

What's wrong with mapMonotonic that isn't wrong with, say, sortBy?, or Eq instances for parametrized types?

...

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...)

Before we can talk about what == should return, can we settle what we mean by = ? I think we need to pragmatic about breaking the rules, given suitable documentation and maybe warnings. We should at least aspire to some principles, which means we should try to know what we're talking about and to know what we're doing, even if we don't always do what we're talking about. I'll shut up now. Potatoes to peel Conor