[Haskell-cafe] Is (==) commutative?

[Alexander Solla]

On 7/25/12, Christian Sternagel <c.sternagel at gmail.com> wrote:
> On 07/26/2012 11:53 AM, Alexander Solla wrote:
>> The classically valid inference:
>>
>> (x == y) = _|_ => (y == x) = _|_
> Btw: whether this inference is valid or not depends on the semantics of
> (==) and that's exactly what I was asking about. In Haskell we just have
> type classes, thus (==) is more or less arbitrary (apart from its type).

Indeed.  This is true for the interpretation of any function.  But you
apparently want to treat (==) as equality.  This may or may not be
possible, depending on the interpretation you choose.  Does _|_ ==
_|_, or _|_ =/= _|_, or do these questions not even make semantic
sense in the object language?  That's what you need to answer, and the
solution to your problem will become clear.  Note that picking any of
these commits you to a "philosophical" position, insofar as the
commitment will induce a metalanguage which excludes expressions from
other metalanguages.