Discussion:
Add fixity for (==) and (/=)
(too old to reply)
Dannyu NDos
2018-09-17 05:37:58 UTC
Permalink
Given that they are instantized for `Bool`s, they are associative, so it
seems approvable to give them a fixity.

(Sidenote: For the monoid over (==) I suggested on last May, I stated that
it determines if there is an even number of `True`s, but that's wrong. It
determines if there is an odd number of `False`s.)
David Feuer
2018-09-17 08:29:13 UTC
Permalink
Please write out the associativity proofs!
Post by Dannyu NDos
Given that they are instantized for `Bool`s, they are associative, so it
seems approvable to give them a fixity.
(Sidenote: For the monoid over (==) I suggested on last May, I stated that
it determines if there is an even number of `True`s, but that's wrong. It
determines if there is an odd number of `False`s.)
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Dannyu NDos
2018-09-17 09:20:37 UTC
Permalink
---------- Forwarded message ---------
From: Dannyu NDos <***@gmail.com>
Date: 2018년 9월 17음 (월) 였후 6:18
Subject: Re: Add fixity for (==) and (/=)
To: <***@gmail.com>


Proof by truth table (F is False, T is True):
p q r (p == q) (q == r) ((p == q) == r) (p == (q == r))
F F F T T F F
F F T T F T T
F T F F F T T
F T T F T F F
T F F F T T T
T F T F F F F
T T F T F F F
T T T T T T T
That proves associativity of (==).

Also note that p /= q ≡ not p == q. Proof:
p q (p /= q) (not p) (not p == q)
F F F T F
F T T T T
T F T F T
T T F F F
And by symmetry of (/=), p /= q ≡ p == not q.

Then:
(p /= q) /= r ≡ (not p == q) == not r ≡ not p == (q == not r) ≡ p /= (q /=
r).
Hence (/=) is associative.

Q.E.D.
David Feuer
2018-09-17 09:22:09 UTC
Permalink
Looks good to me! Do you have an opinion about infixl vs infixr?
Post by Dannyu NDos
---------- Forwarded message ---------
Date: 2018년 9월 17음 (월) 였후 6:18
Subject: Re: Add fixity for (==) and (/=)
p q r (p == q) (q == r) ((p == q) == r) (p == (q == r))
F F F T T F F
F F T T F T T
F T F F F T T
F T T F T F F
T F F F T T T
T F T F F F F
T T F T F F F
T T T T T T T
That proves associativity of (==).
p q (p /= q) (not p) (not p == q)
F F F T F
F T T T T
T F T F T
T T F F F
And by symmetry of (/=), p /= q ≡ p == not q.
(p /= q) /= r ≡ (not p == q) == not r ≡ not p == (q == not r) ≡ p /= (q /=
r).
Hence (/=) is associative.
Q.E.D.
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Dannyu NDos
2018-09-17 09:28:52 UTC
Permalink
Well, infixr is friendlier to parsers.
Post by David Feuer
Looks good to me! Do you have an opinion about infixl vs infixr?
Libraries mailing list
Post by Dannyu NDos
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
C Maeder
2018-09-18 09:34:39 UTC
Permalink
Hi,

infixr seeems right for an equivalence (==) since implication is usually
also right associative.

Implication "==>" corresponds to "<=" on Bool, which might be confusing.
Reverse implication (>=) should be left associative, then.

Cheers Christian
Post by Dannyu NDos
Well, infixr is friendlier to parsers.
Looks good to me! Do you have an opinion about infixl vs infixr?
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Eric Mertens
2018-09-18 15:34:41 UTC
Permalink
Do we have any other good examples where we've got an operator that is
considered associative where the result type isn't identical to the
argument types? It's much more common to allow the types to vary when
there's only one associativity that makes sense for the way an operator is
intended to be used.

a -> a -> a

While it's true that focusing on Bool, (==) satisfies associativity in its
truth table, the types don't work out so cleanly. Outside of Bool it starts
to matter which associativity you pick.

(\x y z -> (x == y) == z) :: Eq a => a -> a -> Bool -> Bool

(\x y z -> x == (y == z)) :: Eq a => Bool -> a -> a -> Bool

Making == associative is just going to lead to harder to understand code
and will require people to memorize which arbitrary choice about the
associativity of the operation was selected by the mailing list in order to
make sense of the types of code using multiple ==.

I see no gain here, and I'd prefer to leave == as is.

Best regards,
Eric Mertens
Post by C Maeder
Hi,
infixr seeems right for an equivalence (==) since implication is usually
also right associative.
Implication "==>" corresponds to "<=" on Bool, which might be confusing.
Reverse implication (>=) should be left associative, then.
Cheers Christian
Post by Dannyu NDos
Well, infixr is friendlier to parsers.
Looks good to me! Do you have an opinion about infixl vs infixr?
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Dannyu NDos
2018-09-18 15:45:49 UTC
Permalink
Well, the motivation to make them associative was that (==) is logical
XNOR, and (/=) is logical XOR. Perhaps we want an alias for
Bool-instantization of them.
Post by Eric Mertens
Do we have any other good examples where we've got an operator that is
considered associative where the result type isn't identical to the
argument types? It's much more common to allow the types to vary when
there's only one associativity that makes sense for the way an operator is
intended to be used.
a -> a -> a
While it's true that focusing on Bool, (==) satisfies associativity in its
truth table, the types don't work out so cleanly. Outside of Bool it starts
to matter which associativity you pick.
(\x y z -> (x == y) == z) :: Eq a => a -> a -> Bool -> Bool
(\x y z -> x == (y == z)) :: Eq a => Bool -> a -> a -> Bool
Making == associative is just going to lead to harder to understand code
and will require people to memorize which arbitrary choice about the
associativity of the operation was selected by the mailing list in order to
make sense of the types of code using multiple ==.
I see no gain here, and I'd prefer to leave == as is.
Best regards,
Eric Mertens
Eric Mertens
2018-09-18 15:58:18 UTC
Permalink
Well, the motivation to make them associative was that (==) is logical XNOR, and (/=) is logical XOR. Perhaps we want an alias for Bool-instantization of them.
We already have such an binary operation in base that is associative: xor.
import Data.Bits
:i xor
class Eq a => Bits a where
...
xor :: a -> a -> a
...
-- Defined in ‘Data.Bits’
True `xor` False `xor` True
False

The thing that would be missing is an xnor operation in Data.Bits.
--
Eric
Richard Eisenberg
2018-09-18 15:57:17 UTC
Permalink
+1 to Eric's argument here. I would prefer to leave these fixities out. Of course, defining Bool-specific instantiations with fixities is a fine idea.

Richard
Do we have any other good examples where we've got an operator that is considered associative where the result type isn't identical to the argument types? It's much more common to allow the types to vary when there's only one associativity that makes sense for the way an operator is intended to be used.
a -> a -> a
While it's true that focusing on Bool, (==) satisfies associativity in its truth table, the types don't work out so cleanly. Outside of Bool it starts to matter which associativity you pick.
(\x y z -> (x == y) == z) :: Eq a => a -> a -> Bool -> Bool
(\x y z -> x == (y == z)) :: Eq a => Bool -> a -> a -> Bool
Making == associative is just going to lead to harder to understand code and will require people to memorize which arbitrary choice about the associativity of the operation was selected by the mailing list in order to make sense of the types of code using multiple ==.
I see no gain here, and I'd prefer to leave == as is.
Best regards,
Eric Mertens
Hi,
infixr seeems right for an equivalence (==) since implication is usually
also right associative.
Implication "==>" corresponds to "<=" on Bool, which might be confusing.
Reverse implication (>=) should be left associative, then.
Cheers Christian
Post by Dannyu NDos
Well, infixr is friendlier to parsers.
Looks good to me! Do you have an opinion about infixl vs infixr?
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Lennart Augustsson
2018-09-18 15:58:06 UTC
Permalink
The (==) and (/=) operators are non-associative on purpose. Writing
x==y==z is much more likely to be a typo than a legitimate use case. We
decided to make them non-associative, even though they are associative.
(Note that they have fixity already.)
Post by Dannyu NDos
Given that they are instantized for `Bool`s, they are associative, so it
seems approvable to give them a fixity.
(Sidenote: For the monoid over (==) I suggested on last May, I stated that
it determines if there is an even number of `True`s, but that's wrong. It
determines if there is an odd number of `False`s.)
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Loading...