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

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

On 2008-03-14, Conor McBride wrote:

...

Hi

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

...

On 2008-03-13, Conor McBride 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