Add fixity for (==) and (/=)

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
11 messages Options
Reply | Threaded
Open this post in threaded view
|

Add fixity for (==) and (/=)

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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add fixity for (==) and (/=)

David Feuer
Please write out the associativity proofs!


On Mon, Sep 17, 2018, 1:38 AM Dannyu NDos <[hidden email]> wrote:
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Fwd: Add fixity for (==) and (/=)

Dannyu NDos


---------- Forwarded message ---------
From: Dannyu NDos <[hidden email]>
Date: 2018년 9월 17일 (월) 오후 6:18
Subject: Re: Add fixity for (==) and (/=)
To: <[hidden email]>


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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add fixity for (==) and (/=)

David Feuer
Looks good to me! Do you have an opinion about infixl vs infixr?

On Mon, Sep 17, 2018, 5:21 AM Dannyu NDos <[hidden email]> wrote:


---------- Forwarded message ---------
From: Dannyu NDos <[hidden email]>
Date: 2018년 9월 17일 (월) 오후 6:18
Subject: Re: Add fixity for (==) and (/=)
To: <[hidden email]>


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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add fixity for (==) and (/=)

Dannyu NDos
Well, infixr is friendlier to parsers.

2018년 9월 17일 (월) 오후 6:22, David Feuer <[hidden email]>님이 작성:
Looks good to me! Do you have an opinion about infixl vs infixr?


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Add fixity for (==) and (/=)

C Maeder-2
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 <[hidden email]
> <mailto:[hidden email]>>님이 작성:
>
>     Looks good to me! Do you have an opinion about infixl vs infixr?
>
>         Libraries mailing list
>         [hidden email] <mailto:[hidden email]>
>         http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add fixity for (==) and (/=)

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


On Tue, Sep 18, 2018 at 2:34 AM C Maeder <[hidden email]> 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 <[hidden email]
> <mailto:[hidden email]>>님이 작성:
>
>     Looks good to me! Do you have an opinion about infixl vs infixr?
>
>         Libraries mailing list
>         [hidden email] <mailto:[hidden email]>
>         http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add fixity for (==) and (/=)

Dannyu NDos
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 <[hidden email]>님이 작성:
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

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add fixity for (==) and (/=)

Richard Eisenberg-4
In reply to this post by Eric Mertens
+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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]
> <mailto:[hidden email]>>님이 작성:
>
>     Looks good to me! Do you have an opinion about infixl vs infixr?
>
>         Libraries mailing list
>         [hidden email] <mailto:[hidden email]>
>         http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add fixity for (==) and (/=)

Lennart Augustsson
In reply to this post by Dannyu NDos
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.)

On Sun, Sep 16, 2018 at 22:38 Dannyu NDos <[hidden email]> wrote:
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Add fixity for (==) and (/=)

Eric Mertens
In reply to this post by Dannyu NDos


On Sep 18, 2018, at 8:45 AM, Dannyu NDos <[hidden email]> 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

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries