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

[Conor McBride]

Hi folks

I'm late into this thread, so apologies if
I'm being dim.

On 13 Mar 2008, at 16:17, kahl at cas.mcmaster.ca wrote:

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

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