Hi Alexander,
Thanks for commenting on this issue.
On 21 June 2012 16:34, Alexander Solla
These nits don't need to be picked. The theory of equivalence relations is extremely well understood. This is a topic covered by the sophomore mathematics level.
I did not say that the theory of equivalence relations is not well understood. All I have said is that [1] demonstrates that people have different ideas as to what an Eq instance should satisfy. And, yes, it is all about picking a suitable notion for Eq and designating other (possibly related and useful) notions for other type classes. Being an equivalence relation is just one of them. But, to be honest, I find this rather confusing. I thought, and I suspect I am not the only one, Eq was about equality and not about equivalence. I have just had a look at the Haskell 2010 and Prelude. When it comes to the Eq type class, precise definition of what its instances should satisfy is missing. But crucially, both texts talk about equality and not about equivalence. The word equivalence is not even mentioned in the context of the Eq class. This may sound to much of a technical/terminological point, but I believe the terminology we use is important, especially, in the context of Haskell where formal reasoning about programs is not unusual. Also, I find the use of the == symbol to denote equivalence rather than equality rather questionable. The way lhs2tex typesets the == symbol, makes this even more questionable. Again this may sound to much of a symbolical point, but I believe the symbols we use are important, especially, in the context of Haskell where formal reasoning about programs is not unusual. I would like to kindly ask you to provide a reference designating Eq for equivalence and not for equality and stating that only being an equivalence relation is required. Thanks in advance. Why not use the Eq type class (as the current Haskell 2010 and Prelude texts suggest) for a stronger notion of equality (observational equality with a suitable notion of observation is one candidate), and designate weaker notions such as being just an equivalence relation to different type classes?
But, my opinion is that if you can write a pure function f that can tell them apart (i.e., f x /= f y), I find it a very strange notion of equality.
There's your problem.
Unfortunately, this is not only my problem. In addition to mailing list discussions I referred to in the earlier email sent to Derek [2,3] (these discussions are about functor and monad instances for sets), a paper by John Hughes about "Restricted Data Types in Haskell" [4] and a draft by Oleg Kiselyov about "Restricted Monads" [5] are also relevant. Both, John and Oleg, use monad instances for sets as primary examples. However, their properties can be easily violated by Eq instances provided by Derek and Dan. John's and Oleg's constructions, for the monad laws to hold, rely on Eq to be equality and not just an equivalence relation.
It is straight-forward to generate an equivalence relation that can tell things apart with respect to a different equivalence relation. Equivalence relations do not need to agree!
See above, I thought Eq was about equality and not about equivalence.
If you really want to keep distinct equivalence relations apart semantically, just use a newtype wrapper to explicitly "name" the relation.
This is certainly possible. Can you point to a library or a document that exemplifies this approach for dealing with different notions of equality and/or equivalence. Maybe there are already conventions in place that I am not aware of. Thanks in advance.
I am not saying that this is a trivial undertaking, but would be a more principled approach. It would require the Haskell community and, especially, standard library and language specification developers to agree on a suitable notion of equality that Eq instances should satisfy.
That has already happened. A relation merely has to satisfy the equivalence relation axioms.
Can you provide a reference? When this was agreed and where is this specified? Thanks in advance, George [1] http://www.haskell.org/pipermail/haskell-cafe/2008-March/thread.html [2] http://www.haskell.org/pipermail/haskell-cafe/2010-July/080977.html [3] http://haskell.1045720.n5.nabble.com/Functor-instance-for-Set-td5525789.html [4] http://www.cs.utexas.edu/users/ham/richards/FP%20papers/restricted-datatypes... [5] http://okmij.org/ftp/Haskell/types.html#restricted-datatypes