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

Hi On 13 Mar 2008, at 23:33, Aaron Denney wrote:

On 2008-03-13, Conor McBride wrote:

...

Hi

On 13 Mar 2008, at 22:28, ajb@spamcop.net wrote:

...

G'day all.

Quoting Adrian Hey :

...

What's disputed is whether or not this law should hold: (a == b) = True implies a = b

Apart from possibly your good self, I don't think this is disputed. Quotient types, as noted elsewhere in this thread, are very useful.

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.

Now, it may be the case that fooBy functions are then the right thing, but it's not clear to me at all that this is true.

And if the fooBy option works, then why would the foo option fail for equivalence classes?

It seems reasonable to construct quotients from arbitrary equivalences: if fooBy works for the carrier, foo should work for the quotient. 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.

...

A bit more structure for order-related classes would surely help here.

Say what?

Don't panic!

If I don't have a total ordering, then it's possible two elements are incomparable

Quite so.

-- what should a sort algorithm do in such a situation?

Not care. Produce a resulting list where for any [..., x, ..., y, ...] in the result, y <= x implies x <= y. Vacuously satisfied in the case of incomparable elements. In the case of a total order, that gives you y <= x implies x = y (and everything in between), but for a preorder, you put less in, you get less out. Will that do? Conor