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

On 2008-03-15, Conor McBride wrote:

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.

Which is worth doing. But I think, in the end very little interesting could end up passing that muster totally. Once you weaken it a bit, the guarantees are gone. In practice, I think there are significant number of user defined type that implement Eq that just don't pass this test. We can recognize this, or declare all that code bad.

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.

Well, no, it's not ideal. In fact, it's downright misleading. I also think it's the best we can do before Haskell', in terms of not causing gratuitous code breakage.

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.

Ah. The normal weakening of a total order is a partial order, and I was stuck on that, instead of this weakening, which technically makes it a "total preorder". And I think that's the right semantics for the Ord class, because that's the common case for programming. Can we make a reasonable class hierarchy that supports all these notions? class Equiv a where (~=~), (~/~) :: a -> a -> Bool class Equiv a => Equal a where (==), (/=) :: a -> a -> Bool (==) = (~=~) (/=) = (~/~) class Equiv a => PreOrd a where compare :: a -> a -> Ordering (<), (<~), (>~), (>) :: a -> a -> Bool class (PreOrd a, Equal a) => Ord a where (<=), (>=) :: a -> a -> Bool (<=) = (<~) (>=) = (>~) (And both are orderings are total.) How do we nicely add partial orders? semantically we want class (PartialOrder a) => Order a where compare = narrow partialCompare but "narrow" by necessity has an incomplete pattern match. An easy thing would be instance (Order a) => PartialOrder a where partialCompare = inject compare but this lacks flexibility. Will this flexibility ever be necessary? Quite possibly. But, as usual, newtypes can come to the rescue, at the cost of some akwardness. Should this also be done for Equiv, Equal, PreOrder and Ord?

...

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.

Consider data Treehelp a = Leaf | Branch (Treehelp a) a (Treehelp a) data Tree a = (a -> a -> Ordering, Treehelp a) how do we implement merge :: Tree a -> Tree a -> Tree a so that two incompatible orderings aren't used? Okay, you say, let's not embed the functions in the tree: data Tree a = Leaf | Branch (Tree a) a (Tree a) insert :: (a -> a -> Ordering) -> Tree a -> Tree a merge :: (a -> a -> Ordering) -> Tree a -> Tree a -> Tree a But these two will do something wrong if the trees were constructed with a different function. Instead, if we have merge :: Ord a => Tree a -> Tree a -> Tree a The ordering is carried along in the dictionary, and the typechecker ensures that only trees using the same ordering are merged. Different orders on the same underlying type can be achieved with newtype wrappers.

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

Right. My point of view is that whatever is denoted by = is a notion that lives outside the operators in the language itself, including (==). We can do certain formal manipulations using the definitions in the language.

...

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.

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.

This sounds persuasive, but the example of a sort that feels free to replace equivalent elements shows that although we want two nonequal elements to be treated as "equal" for the purposes of comparison and reordering them, we don't really always mean truely, 100% of the time, equal, because substitution is not, in fact, allowable. And I do think that this is either the common case, or that it doesn't hurt 99% of the time to write code that works for this case.

...

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.

Some people will need to change the way we think whichever semantics we assign. -- Aaron Denney -><-