---------- Forwarded message --------- From: Dannyu NDos <ndospark320@gmail.com> Date: 2018년 9월 17일 (월) 오후 6:18 Subject: Re: Add fixity for (==) and (/=) To: <david.feuer@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.
Looks good to me! Do you have an opinion about infixl vs infixr? On Mon, Sep 17, 2018, 5:21 AM Dannyu NDos <ndospark320@gmail.com> wrote:
---------- Forwarded message --------- From: Dannyu NDos <ndospark320@gmail.com> Date: 2018년 9월 17일 (월) 오후 6:18 Subject: Re: Add fixity for (==) and (/=) To: <david.feuer@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. _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Well, infixr is friendlier to parsers. 2018년 9월 17일 (월) 오후 6:22, David Feuer <david.feuer@gmail.com>님이 작성:
Looks good to me! Do you have an opinion about infixl vs infixr?
Libraries mailing list
Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
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 Am 17.09.2018 um 11:28 schrieb Dannyu NDos:
Well, infixr is friendlier to parsers.
2018년 9월 17일 (월) 오후 6:22, David Feuer <david.feuer@gmail.com <mailto:david.feuer@gmail.com>>님이 작성:
Looks good to me! Do you have an opinion about infixl vs infixr?
Libraries mailing list Libraries@haskell.org <mailto:Libraries@haskell.org> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
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 On Tue, Sep 18, 2018 at 2:34 AM C Maeder <chr.maeder@web.de> wrote:
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
Am 17.09.2018 um 11:28 schrieb Dannyu NDos:
Well, infixr is friendlier to parsers.
2018년 9월 17일 (월) 오후 6:22, David Feuer <david.feuer@gmail.com <mailto:david.feuer@gmail.com>>님이 작성:
Looks good to me! Do you have an opinion about infixl vs infixr?
Libraries mailing list Libraries@haskell.org <mailto:Libraries@haskell.org> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
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. 2018년 9월 19일 (수) 00:34, Eric Mertens <emertens@gmail.com>님이 작성:
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
On Sep 18, 2018, at 8:45 AM, Dannyu NDos <ndospark320@gmail.com> wrote:
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
+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
On Sep 18, 2018, at 11:34 AM, Eric Mertens <emertens@gmail.com> wrote:
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
On Tue, Sep 18, 2018 at 2:34 AM C Maeder <chr.maeder@web.de <mailto:chr.maeder@web.de>> wrote: 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
Am 17.09.2018 um 11:28 schrieb Dannyu NDos:
Well, infixr is friendlier to parsers.
2018년 9월 17일 (월) 오후 6:22, David Feuer <david.feuer@gmail.com <mailto:david.feuer@gmail.com> <mailto:david.feuer@gmail.com <mailto:david.feuer@gmail.com>>>님이 작성:
Looks good to me! Do you have an opinion about infixl vs infixr?
Libraries mailing list Libraries@haskell.org <mailto:Libraries@haskell.org> <mailto:Libraries@haskell.org <mailto:Libraries@haskell.org>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
_______________________________________________ Libraries mailing list Libraries@haskell.org <mailto:Libraries@haskell.org> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
_______________________________________________ Libraries mailing list Libraries@haskell.org <mailto:Libraries@haskell.org> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries> _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
participants (5)
-
C Maeder -
Dannyu NDos -
David Feuer -
Eric Mertens -
Richard Eisenberg