[Haskell-cafe] Is (==) commutative?
Christian Sternagel
c.sternagel at gmail.com
Thu Jul 26 06:52:07 CEST 2012
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).
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.)
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.
cheers
chris
More information about the Haskell-Cafe
mailing list