
On Wed, Apr 21, 2010 at 5:25 AM, Max Rabkin
On Wed, Apr 21, 2010 at 1:44 AM, Edward Kmett
wrote: Eq doesn't state anywhere that the instances should be structural, though in general where possible it is a good idea, since you don't have to worry about whether or not functions respect your choice of setoid.
Wikipedia's definition of structural equality is an object-oriented one, but if by structural equality you mean the natural equality on algebraic datatypes (as derived automatically), I don't believe this is quite the case. If the type is abstract, surely the Eq instance need only be a quotient w.r.t. the operations defined on it. Thus, for example, two Sets can be considered equal if they contain the same elements, rather than having identical tree shapes (except that Data.Set exports unsafe functions, like mapMonotonic which has an unchecked precondition).
Yes. My point about why falling back on structural equality is a good idea when possible, is that then you don't have to work so hard to make sure that x == y => f x == f y holds. When your equality instance isn't structural you need to effectively prove a theorem every time you work with the structure to avoid violating preconceptions. My post was acknowledging the expedience of such methods. I think we are using a lot of words to agree with one another. ;) -Edward Kmett
--Max