[Haskell-cafe] Re: (flawed?) benchmark : sort

[Conor McBride]

Hi

On 14 Mar 2008, at 21:39, Aaron Denney wrote:

> On 2008-03-14, Conor McBride <conor at strictlypositive.org> wrote:
>> Hi
>>
>> On 13 Mar 2008, at 23:33, Aaron Denney wrote:
>>
>>> On 2008-03-13, Conor McBride <conor at strictlypositive.org> wrote:
>>>> For a suitable notion of = on quotients, and with a
>>>> suitable abstraction barrier at least morally in place,
>>>> is that really too much to ask?
>>>
>>> I really think it is.  I don't think the case of "equivalent for  
>>> this
>>> purpose, but not that purpose" can be ignored.
>>
>> Sure. But use the right tools for the job.
>
> So what are the right tools then?  Why is a typeclass not the right
> tool?

I guess I mean to distinguish *equality*, which is
necessarily respected by all observations (for some
notion of observation which it's important to pin
down), from coarser equivalences where respect takes
careful effort.

Take Roman's example of alpha-equivalence for the
lambda-terms with strings for bound variables. No
way would I ever call that "equality", because
respecting alpha-equivalence takes quite a lot of
care. (Correspondingly, I'd switch to a
representation which admitted equality.)

[..]

>> Of
>> course, if you want to expose the representation
>> for some other legitimate purpose, then it wasn't
>> equality you were interested in, so you should
>> call it something else.
>
> I'm perfectly happy calling it Equivalence.

I'm perfectly happy having equivalences around,
but if "Eq" means "has an equivalence" rather
than "has equality", then I'm not very happy
about the use of the == sign.

[..]

> That's a workable definition, but I don't know if I'd call it a
> sort, precisely.  The standard unix tool "tsort" (for "topological
> sort", a bit of a misnomer) does this.
>
>> Will that do?
>
> Unfortunately, one can't just reuse the standard algorithms.

Indeed. (Does anyone know a topological sort
algorithm which behaves like an ordinary sort if
you do give it a total order? Or a reason why
there's no such thing?)

So you're probably right that

   x <= y \/ y <= x

should hold for the order relation used by
library sort. That's not the axiom I was
thinking of dropping when I said sort's type
was too tight (it was you who brought up
incomparability): I was thinking of dropping
antisymmetry.

> If a sort can't support the standard "sort on this key" technique, and
> don't munge everything for two keys that compare equal, something is
> wrong.  And I don't think sort is that special a case.

I quite agree. That's why I'm suggesting we
drop antisymmetry as a requirement for sorting.


>
> Instances, rather than explicit functions, are nice because they  
> let us
> use the type system to ensure that we never have incompatible  
> functions
> used when combining two data structures, or pass in a function that's
> incompatible with the invariants already in a data structure built  
> with
> another function.

I'm not sure what you mean here.


> So we surely do need an equivalence relation typeclass.  And there are
> Eq instances that aren't quite equality, but are equivalences, and  
> work
> with almost all code that takes Eq instances.

My main concern is that we should know where we
stand. I think it would be a very good thing if
we knew what the semantic notion of equality
should be for each type. What notion of equality
should we use in discussion? What do we mean when
we write "laws" like

   map f . map g = map (f . g)

? I write = to distinguish it from whatever
Bool-valued function at some type or other
that we might call ==.

Given sneaky ways to observe memory pointers or
fairly ordinary ways to expose representations
which are supposed to be abstract, it's clearly
impossible to ensure that = is absolutely always
respected. It would be good if it was clear which
operations were peculiar in this way. I'd like to
know when I can reason just by replacing equals
for equals, and when more care is required (eg,
when ensuring that substitution respects alpha-
equivalence).

 From the point of view of reasoning (informally
or formally) it then becomes useful to know that
some binary Bool-valued function is sound with
respect to = and complete when one argument is
defined and finite. It's useful to know that one
is testing equality, rather than just some
equivalence, because equality supports stronger
reasoning principles.

Equivalences are useful too, but harder to work
with. I quite agree that we should support them,
and that it is reasonable to do so via
typeclasses: if a type supports multiple useful
equivalences, then the usual newtype trick is
a reasonable enough way to manage it.

>
> The only time treating equalities as equivalences won't work is  
> when we
> need to coalesce equivalent elements into one representative, and the
> choice of representative matters.


Another time when treating equalities just as
equivalences won't do is when it's time to think
about whether your program works. This issue is
not just an operational one, although in the
case of TypeRep, for example, it can get pretty
near the bone.


> So, do we mark equivalencies as special, or observational equality as
> special?  Which is the tagging class, and which has the methods?  I
> think it's pretty clear that the way to go is have (==) and (/=) live
> in Equiv, and have Equal be a tagging class.  An equivalence is not a
> special type of equality, but equality is a special type of  
> equivalence.

Isn't it misleading to use the == symbol for
something less than equality? One could keep
== as a method of Equal, defined to coincide
with ~=~ or whatever is the equivalence method.

An alternative, contrary to your assertion,
is to introduce an equivalence as the equality
on a quotient via a newtype. That's a
conventional "type with funny structure" use
of newtype and it has the advantage of keeping
just the one class, and of providing a
syntactic cue (unpacking the newtype) to tell
you when you've stepped outside the domain of
observations for which equational reasoning
just works. The point is to make it clear, one
way or another, which modes of reasoning
apply.


>
> Given all that, I think current Eq as Equivalence makes sense, and we
> need to add an Equal class for things where we truly can't tell
> equivalent elements apart.

You may ultimately be right, but I don't think
you've made the case. Moreover, if you are
right, then people will need to change the way
they think and write about Eq and == in the
murk of its impoverished meaning.

I don't suppose I'd complain too much at any
outcome which allows the stronger discipline
to expressed somehow. If we have to make the
weaker notion the default, isn't that a little
sad?

All the best

Conor