[Haskell-cafe] [Haskell] ANNOUNCE: set-monad

[George Giorgidze]

Hi Alexander,

Thanks for commenting on this issue.

On 21 June 2012 16:34, Alexander Solla <alex.solla at gmail.com> wrote:
>
> 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.pdf
[5] http://okmij.org/ftp/Haskell/types.html#restricted-datatypes