
On Mar12, ajb@spamcop.net wrote:
G'day all.
Quoting David Menendez
: 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