On Wed, Apr 21, 2010 at 1:44 AM, Edward Kmett <ekmett@gmail.com> 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