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

[Dan Licata]

On Mar12, ajb at spamcop.net wrote:
> G'day all.
> 
> Quoting David Menendez <dave at zednenem.com>:
> 
> >Adrian is arguing that compare a b == EQ should imply compare (f a) (f
> >b) == EQ for all functions f (excluding odd stuff). Thus, the problem
> >with your example would be in the Ord instance, not the sort function.
> 
> Understood, and the Schwartzian transform might be better understood as
> "sortBy" rather than "sort".
> 
> As others have noted, this really is a question of what Eq and Ord
> "mean".  And the answer to that is: Whatever makes the most
> domain-specific sense.

I think the notion of a quotient type (C / ~) may be helpful in this
discussion.  A quotient type represents the equivalence classes of some
carrier type C under some equivalence relation ~.  Functions of type 
(C / ~) -> A are often defined by working with the underlying carrier
type C.  However, not all functions C -> A define functions 
(C / ~) -> A: to be a well-defined function on equivalence classes, the 
function C -> A must respect the equivalence relation ~, in the sense
that c ~ c implies f(c) =_A f(c') where =_A is whatever equality at A
is.  

For example, you can think of a type Set of sets as (List / ~) where ~
equates two lists iff they are permutations of each other.  Then a
function List -> A counts as a function Set -> A iff it takes
permutations to equal A's.  For instance, you can't write a function
tolist :: Set -> List that simply dumps out the underlying
representation, because then you can distinguish different
representatives of the same equivalence class.  

Now, Haskell doesn't let you define quotient types directly, but you can
code them up with abstract types: if you hide the implementation of a
type C and ensure that all functions C -> A respect some equivalence
relation ~, then you effectively have a quotient type (C / ~), because
all functions on C are well-defined on the equivalence classes.  

So, I think a way of summing up the two points of view on Eq are:

(1) You're only allowed to add an 

instance Eq A where
  (==) = ~

if A "is really" (A / ~).  Then all functions on A necessarily respect
==.  

(2) The instance for Eq A is just some equivalence relation ~ that I
might quotient A by.  

I.e., in Eq A, is A the quotient type or the underlying carrier?  Both
are reasonable and useful notions, but it might make sense to have two
different type classes for these two notions, since if you expect one
and get the other you can get into trouble.

-Dan