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

[Alexander Solla]

On 7/25/12, Christian Sternagel <c.sternagel at gmail.com> wrote:
> Dear Alexander,
>
> On 07/26/2012 01:09 PM, Alexander Solla wrote:
>> 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.

> for my specific case (HOLCF) there is already a fixed metalanguage which
> has logical equality (=) and differentiates between type 'bool' (True,
> False) for logical truth and type 'tr' (TT, FF, _|_) for truth-valued
> computable functions (including nontermination/error). Logical equality
> satisfies '_|_ = _|_'. Now in principle (==) is just an arbitrary
> function (for each instance) but I gather that there is some intended
> use for the type class Eq (and I strongly suspect that it is to model
> equality ;), I merely want to find out to what extend it does so).

Yes, in my opinion, its purpose is to model mathematical/logical
equality.  That said, you brought up a very important point which you
need to address.  I'll discuss it more below.

I will be using scare-quotes quite a bit.  I'm not being sarcastic --
please ask if you don't understand what I mean.

>
> Currently the axioms of the formal eq class include
>
> (_|_ == y) = _|_
> (x == _|_) = _|_
>
> (and this decision was just based on how ghci evaluates corresponding
> expressions).
>
> The equations you use above would be (roughly) written '(_|_ == _|_) =
> TT' and '(_|_ /= _|_) = TT' in HOLCF and neither of them is satisfied,
> since both expressions are logically equivalent to _|_ (in HOLCF). (But
> still both expressions make sense.)


Okay, you have a metalanguage.  And it places limits on what you can
express.  But you can also put limits on what you can express, to
induce a sublanguage of the metalanguage.  I don't know how "natural"
this idea is given your circumstances and goals, but you may want to
consider it.

I promise I'll get to the meat of my email soon.

>
> During the discussion I revisited the other two axioms I was using for
> eq... and now I am wondering whether those make sense. The other two
> axioms where
>
> (x == y) = TT ==> x = y
> (x == y) = FF ==> not (x = y)
>
> The second one should be okay, but the first one is not true in general,
> since it assumes that we would only ever use Eq instances implementing
> syntactic equality (which should be true for deriving?). E.g., for the
> data type
>
>    data Frac = Frac Int Int
>
> we would have 'not (Frac 1 2 = Frac 2 4)' in HOLCF (since we have
> injectivity of all constructors). But nobody prevents a programmer from
> writing an Eq instance of Frac that compares 'normal forms' of fractions.

Now, /this/ is an example of what I've been trying to get at.  (To be
fair, it's a generalization of what I've been trying to get at)  You
put it in "behavioral" terms -- "nothing stops a programmer", whereas
I've been trying to put it in "interpretive" terms (... is ..., but
... means many things -- you have to pick an interpretation)

A hypothetical programmer can write:

> data Fraction = Fraction Int Int
> data Rational = Rational Int Int

and have different semantics for each.  In particular, we should treat
Fraction 1 2 to be distinct from Fraction 2 4, /as fractions/.  And
Rational 1 2 should be the same as Rational 2 4, /as rational
numbers/.  These "implied" semantics are just as important as the
minimum Haskell demands (in my opinion).  The minimum Haskell demands
is not (and cannot) be rich enough to distinguish between
intentions/intensions.

"Obviously", Fraction and Rational are intimately related (the
rationals "should" be a ring of fractions in "normal form").  And
functions between Fraction and Rational "should" preserve the
"correct" relationships.  But, what are these?  We can come up with
theorems, but some things are nothing but the
programmer/mathematician's choice.

In other words, by choosing a semantic where (Rational 1 2) ==
(Rational 2 4), a programmer/mathematician has *generated* a
sublanguage of Haskell by imposing his *intended* semantics.  This is
an example of "intensions" versus "extensions" in logic.

So, your task is... difficult.  From my point of view, you will have
to axiomatize at least one set of "best practices" for Haskell
programming, and target /that/ Haskell sublanguage in your HOLCF
analyzer.  You can even do more than one Haskell sublanguage, but as I
said before, each set of "best practices" will commit you to a
different "philosophical" position.