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

[Aaron Denney]

On 2008-03-15, Conor McBride <conor at strictlypositive.org> wrote:
> 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.

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