Proposal: Data.Bool.implies

Niklas Hambüchen

18 Jan 2016 18 Jan '16

2:17 a.m.

I propose to add to Data.Bool: -- | Boolean implication. implies :: Bool -> Bool -> Bool implies True x = x implies False _ = True infix 4 `implies` -- same as (==) The request for this is quite old (see e.g. http://neilmitchell.blogspot.de/2007/02/logical-implication-in-haskell.html). I believe that by not trying to use an operator for it, and keeping it in Data.Bool, we can avoid doing anything wrong. A quick superficial search on Stackage Hoogle suggests that adding this function should create no breakage (4 packages define their own function called `implies`, none of them import Data.Bool). `infix` instead of `infixl` or `infixr` to force you to bracket it; for the same reason it has the same precedence as `==`.

Show replies by date

David Feuer

18 Jan 18 Jan

4:12 a.m.

-1. We already have a `<=` operator. On Sun, Jan 17, 2016 at 9:17 PM, Niklas Hambüchen wrote:

...

I propose to add to Data.Bool:

-- | Boolean implication. implies :: Bool -> Bool -> Bool implies True x = x implies False _ = True

infix 4 `implies` -- same as (==)

The request for this is quite old (see e.g. http://neilmitchell.blogspot.de/2007/02/logical-implication-in-haskell.html).

I believe that by not trying to use an operator for it, and keeping it in Data.Bool, we can avoid doing anything wrong.

A quick superficial search on Stackage Hoogle suggests that adding this function should create no breakage (4 packages define their own function called `implies`, none of them import Data.Bool).

`infix` instead of `infixl` or `infixr` to force you to bracket it; for the same reason it has the same precedence as `==`. _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

Jon Purdy

5:23 a.m.

+1. “<=” has the wrong strictness. In “a `implies` b”, “b” should not be evaluated if “a” is false. As a strawman, I’d propose that the Ord instance for Bool be changed—but this is more likely to break existing code, however slightly. On Sun, Jan 17, 2016 at 8:12 PM, David Feuer wrote:

...

-1. We already have a `<=` operator.

On Sun, Jan 17, 2016 at 9:17 PM, Niklas Hambüchen wrote:

...
I propose to add to Data.Bool:

-- | Boolean implication. implies :: Bool -> Bool -> Bool implies True x = x implies False _ = True

infix 4 `implies` -- same as (==)

The request for this is quite old (see e.g.

http://neilmitchell.blogspot.de/2007/02/logical-implication-in-haskell.html ).

...
I believe that by not trying to use an operator for it, and keeping it in Data.Bool, we can avoid doing anything wrong.

A quick superficial search on Stackage Hoogle suggests that adding this function should create no breakage (4 packages define their own function called `implies`, none of them import Data.Bool).

`infix` instead of `infixl` or `infixr` to force you to bracket it; for the same reason it has the same precedence as `==`. _______________________________________________ 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

David Feuer

6:14 a.m.

I think changing the Ord instance for Bool *may* be the way to go. Yes, the lazy one is likely a bit less efficient in some cases, but I somehow doubt many are relying on it to be fast. Moreover, people expect most Bool operations to short-circuit (I even seem to have lost that fight wrt the Data.Bits operations, which I firmly believe should be *strict*). instance Ord Bool where False <= _ = True True <= x = x True >= _ = True False >= x = not x False < x = x True < _ = False False > _ = False True > x = not x On Mon, Jan 18, 2016 at 12:23 AM, Jon Purdy wrote:

...

+1. “<=” has the wrong strictness. In “a `implies` b”, “b” should not be evaluated if “a” is false.

As a strawman, I’d propose that the Ord instance for Bool be changed—but this is more likely to break existing code, however slightly.

On Sun, Jan 17, 2016 at 8:12 PM, David Feuer wrote:

...
-1. We already have a `<=` operator.

On Sun, Jan 17, 2016 at 9:17 PM, Niklas Hambüchen wrote:

...
I propose to add to Data.Bool:

-- | Boolean implication. implies :: Bool -> Bool -> Bool implies True x = x implies False _ = True

infix 4 `implies` -- same as (==)

The request for this is quite old (see e.g.

http://neilmitchell.blogspot.de/2007/02/logical-implication-in-haskell.html).

I believe that by not trying to use an operator for it, and keeping it in Data.Bool, we can avoid doing anything wrong.

A quick superficial search on Stackage Hoogle suggests that adding this function should create no breakage (4 packages define their own function called `implies`, none of them import Data.Bool).

`infix` instead of `infixl` or `infixr` to force you to bracket it; for the same reason it has the same precedence as `==`. _______________________________________________ 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

Bardur Arantsson

6:41 a.m.

On 01/18/2016 07:14 AM, David Feuer wrote:

...

I think changing the Ord instance for Bool *may* be the way to go.

If that happens then perhaps an "implies" alias in Data.Bool might still be relevant? I, for one, would almost certainly not have discovered "<=" if I were looking for this function. That said, I don't think I've ever had a need for "implies", so... +0 for an alias, I guess.

Evan Laforge

6:57 a.m.

I have only very rarely needed 'implies' and when I do I'm happy with 'if a then b else False'. But if I needed to do that a lot, I would write my own function and certainly never use (<=), because I wouldn't guess that (<=) has the same logic as implies. And even if it does, isn't the means more important than the end? For the same reason I wouldn't write 'not a || b' because when I want to say implies I'll just directly say implies. On Mon, Jan 18, 2016 at 11:44 AM, David Feuer wrote:

...

I think changing the Ord instance for Bool *may* be the way to go. Yes, the lazy one is likely a bit less efficient in some cases, but I somehow doubt many are relying on it to be fast. Moreover, people expect most Bool operations to short-circuit (I even seem to have lost that fight wrt the Data.Bits operations, which I firmly believe should be *strict*).

instance Ord Bool where False <= _ = True True <= x = x

True >= _ = True False >= x = not x

False < x = x True < _ = False

False > _ = False True > x = not x

On Mon, Jan 18, 2016 at 12:23 AM, Jon Purdy wrote:

...
+1. “<=” has the wrong strictness. In “a `implies` b”, “b” should not be evaluated if “a” is false.

As a strawman, I’d propose that the Ord instance for Bool be changed—but this is more likely to break existing code, however slightly.

On Sun, Jan 17, 2016 at 8:12 PM, David Feuer wrote:

...
-1. We already have a `<=` operator.

On Sun, Jan 17, 2016 at 9:17 PM, Niklas Hambüchen wrote:

...
I propose to add to Data.Bool:

-- | Boolean implication. implies :: Bool -> Bool -> Bool implies True x = x implies False _ = True

infix 4 `implies` -- same as (==)

The request for this is quite old (see e.g.

http://neilmitchell.blogspot.de/2007/02/logical-implication-in-haskell.html).

I believe that by not trying to use an operator for it, and keeping it in Data.Bool, we can avoid doing anything wrong.

A quick superficial search on Stackage Hoogle suggests that adding this function should create no breakage (4 packages define their own function called `implies`, none of them import Data.Bool).

`infix` instead of `infixl` or `infixr` to force you to bracket it; for the same reason it has the same precedence as `==`. _______________________________________________ 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

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

David Feuer

7:04 a.m.

I agree with you that not a || b says something a bit different from a `implies` b in a more general logical context. However, I believe that a <= b says exactly the same thing. It's true that it may not be quite obvious to everyone, but anyone thinking enough about logic to *want* an implies function should probably be willing to learn such things. On Mon, Jan 18, 2016 at 1:57 AM, Evan Laforge wrote:

...

I have only very rarely needed 'implies' and when I do I'm happy with 'if a then b else False'. But if I needed to do that a lot, I would write my own function and certainly never use (<=), because I wouldn't guess that (<=) has the same logic as implies. And even if it does, isn't the means more important than the end? For the same reason I wouldn't write 'not a || b' because when I want to say implies I'll just directly say implies.

On Mon, Jan 18, 2016 at 11:44 AM, David Feuer wrote:

...
I think changing the Ord instance for Bool *may* be the way to go. Yes, the lazy one is likely a bit less efficient in some cases, but I somehow doubt many are relying on it to be fast. Moreover, people expect most Bool operations to short-circuit (I even seem to have lost that fight wrt the Data.Bits operations, which I firmly believe should be *strict*).

instance Ord Bool where False <= _ = True True <= x = x

True >= _ = True False >= x = not x

False < x = x True < _ = False

False > _ = False True > x = not x

On Mon, Jan 18, 2016 at 12:23 AM, Jon Purdy wrote:

...
+1. “<=” has the wrong strictness. In “a `implies` b”, “b” should not be evaluated if “a” is false.

As a strawman, I’d propose that the Ord instance for Bool be changed—but this is more likely to break existing code, however slightly.

On Sun, Jan 17, 2016 at 8:12 PM, David Feuer wrote:

...
-1. We already have a `<=` operator.

On Sun, Jan 17, 2016 at 9:17 PM, Niklas Hambüchen wrote:

...
I propose to add to Data.Bool:

-- | Boolean implication. implies :: Bool -> Bool -> Bool implies True x = x implies False _ = True

infix 4 `implies` -- same as (==)

The request for this is quite old (see e.g.

http://neilmitchell.blogspot.de/2007/02/logical-implication-in-haskell.html).

I believe that by not trying to use an operator for it, and keeping it in Data.Bool, we can avoid doing anything wrong.

A quick superficial search on Stackage Hoogle suggests that adding this function should create no breakage (4 packages define their own function called `implies`, none of them import Data.Bool).

`infix` instead of `infixl` or `infixr` to force you to bracket it; for the same reason it has the same precedence as `==`. _______________________________________________ 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

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

Bardur Arantsson

7:19 a.m.

On 01/18/2016 08:04 AM, David Feuer wrote:

...

I agree with you that not a || b says something a bit different from a `implies` b in a more general logical context. However, I believe that a <= b says exactly the same thing. It's true that it may not be quite obvious to everyone, but anyone thinking enough about logic to *want* an implies function should probably be willing to learn such things.

I would think using "<=" would be actively harmful for readers in that the arrow points the wrong way from the usual...? (I realize in this case it's the comparison operator and that conventions may differ, but...)

Brent Yorgey

4:59 p.m.

I disagree. The equivalence between `implies` and (<=) depends on the ordering chosen for Bool, which is completely arbitrary, and is not something people thinking about logic should be expected to know or learn. For example, the Coq standard library happens to choose the other order, with True < False. -Brent On Mon, Jan 18, 2016 at 1:04 AM David Feuer wrote:

...

I agree with you that not a || b says something a bit different from a `implies` b in a more general logical context. However, I believe that a <= b says exactly the same thing. It's true that it may not be quite obvious to everyone, but anyone thinking enough about logic to *want* an implies function should probably be willing to learn such things.

...
I have only very rarely needed 'implies' and when I do I'm happy with 'if a then b else False'. But if I needed to do that a lot, I would write my own function and certainly never use (<=), because I wouldn't guess that (<=) has the same logic as implies. And even if it does, isn't the means more important than the end? For the same reason I wouldn't write 'not a || b' because when I want to say implies I'll just directly say implies.

On Mon, Jan 18, 2016 at 11:44 AM, David Feuer wrote:

...
I think changing the Ord instance for Bool *may* be the way to go. Yes, the lazy one is likely a bit less efficient in some cases, but I somehow doubt many are relying on it to be fast. Moreover, people expect most Bool operations to short-circuit (I even seem to have lost that fight wrt the Data.Bits operations, which I firmly believe should be *strict*).

instance Ord Bool where False <= _ = True True <= x = x

True >= _ = True False >= x = not x

False < x = x True < _ = False

False > _ = False True > x = not x

On Mon, Jan 18, 2016 at 12:23 AM, Jon Purdy wrote:

...
+1. “<=” has the wrong strictness. In “a `implies` b”, “b” should not be evaluated if “a” is false.

As a strawman, I’d propose that the Ord instance for Bool be changed—but this is more likely to break existing code, however slightly.

On Sun, Jan 17, 2016 at 8:12 PM, David Feuer wrote:

...
-1. We already have a `<=` operator.

On Sun, Jan 17, 2016 at 9:17 PM, Niklas Hambüchen

wrote:

...
...
I propose to add to Data.Bool:

-- | Boolean implication. implies :: Bool -> Bool -> Bool implies True x = x implies False _ = True

infix 4 `implies` -- same as (==)

The request for this is quite old (see e.g.

http://neilmitchell.blogspot.de/2007/02/logical-implication-in-haskell.html ).

...
I believe that by not trying to use an operator for it, and keeping

it

...
in Data.Bool, we can avoid doing anything wrong.

A quick superficial search on Stackage Hoogle suggests that adding

On Mon, Jan 18, 2016 at 1:57 AM, Evan Laforge wrote: this

...
...
...
...
...
function should create no breakage (4 packages define their own function called `implies`, none of them import Data.Bool).

`infix` instead of `infixl` or `infixr` to force you to bracket it; for the same reason it has the same precedence as `==`. _______________________________________________ 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

_______________________________________________ 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

Henning Thielemann

6:38 p.m.

On Mon, 18 Jan 2016, Brent Yorgey wrote:

...

I disagree. The equivalence between `implies` and (<=) depends on the ordering chosen for Bool, which is completely arbitrary, and is not something people thinking about logic should be expected to know or learn. For example, the Coq standard library happens to choose the other order, with True < False.

I can confirm that the order is arbitrary. I used a Modula II implementation where True was represented as -1, because that is the bit pattern where all bits are set.

Petr Pudlák

19 Jan 19 Jan

6:38 p.m.

+1 for distinguishing <= and implies. Ordering should not be tied to logical meaning. po 18. 1. 2016 v 19:38 odesílatel Henning Thielemann < lemming@henning-thielemann.de> napsal:

...

On Mon, 18 Jan 2016, Brent Yorgey wrote:

...
I disagree. The equivalence between `implies` and (<=) depends on the ordering chosen for Bool, which is completely arbitrary, and is not something people thinking about logic should be expected to know or learn. For example, the Coq standard library happens to choose the other order, with True < False.

I can confirm that the order is arbitrary. I used a Modula II implementation where True was represented as -1, because that is the bit pattern where all bits are set._______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

Niklas Hambüchen

18 Jan 18 Jan

1:45 p.m.

On 18/01/16 05:12, David Feuer wrote:

...

-1. We already have a `<=` operator.

I would actively discourage from using that for implication - it is extremely counter-intuitive, and invites future headlines like "Self Driving Car Crushes Human Because In Haskell Logical Operators Are The Other Way Around" On 18/01/16 06:23, Jon Purdy wrote:

...

+1. “<=” has the wrong strictness. In “a `implies` b”, “b” should not be evaluated if “a” is false.

As a strawman, I’d propose that the Ord instance for Bool be changed—but this is more likely to break existing code, however slightly.

I think there's simply a difference between comparison and implication. For `<=` the existing strictness makes sense. For implication, a different strictness makes sense.

Andrew Butterfield

8:50 a.m.

HI Niklas,

...

On 18 Jan 2016, at 02:17, Niklas Hambüchen wrote:

I propose to add to Data.Bool:

-- | Boolean implication. implies :: Bool -> Bool -> Bool implies True x = x implies False _ = True

Fine by me (+1)

...

infix 4 `implies` -- same as (==)

The request for this is quite old (see e.g. http://neilmitchell.blogspot.de/2007/02/logical-implication-in-haskell.html).

I believe that by not trying to use an operator for it, and keeping it in Data.Bool, we can avoid doing anything wrong.

A quick superficial search on Stackage Hoogle suggests that adding this function should create no breakage (4 packages define their own function called `implies`, none of them import Data.Bool).

`infix` instead of `infixl` or `infixr` to force you to bracket it; for the same reason it has the same precedence as `==`.

In equational logic, it makes more sense for implication to bind tighter than equivalence, and it would usually be considered as infixr a `implies` b `implies` c same as a `implies` (b `implies` c) But if this breaks something else then plain infix is fine.... That this is the same associativity rule as for function arrows is not a coincidence, by the way.

...

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

Andrew Butterfield School of Computer Science & Statistics Trinity College Dublin 2, Ireland

Henning Thielemann

9:32 a.m.

On Mon, 18 Jan 2016, Andrew Butterfield wrote:

...

In equational logic, it makes more sense for implication to bind tighter than equivalence, and it would usually be considered as infixr

a `implies` b `implies` c same as a `implies` (b `implies` c)

But if this breaks something else then plain infix is fine....

That this is the same associativity rule as for function arrows is not a coincidence, by the way.

It is currying in logic. I assume it was the reason to make 'implies' infixr in utility-ht.

Niklas Hambüchen

1:57 p.m.

On 18/01/16 09:50, Andrew Butterfield wrote:

...

In equational logic, it makes more sense for implication to bind tighter than equivalence, and it would usually be considered as infixr

a `implies` b `implies` c same as a `implies` (b `implies` c)

This is a fair point; my reasoning was that when the variables are a bit longer, it can be more difficult for humans to do brain bracketing, that's why I proposed explicit bracketing for multiple implies with plain infix.

Herbert Valerio Riedel

9:14 a.m.

On 2016-01-18 at 03:17:44 +0100, Niklas Hambüchen wrote: [...]

...

The request for this is quite old (see e.g. http://neilmitchell.blogspot.de/2007/02/logical-implication-in-haskell.html).

I believe that by not trying to use an operator for it, and keeping it in Data.Bool, we can avoid doing anything wrong.

Just wondering, what could/would go wrong if we did use an operator `==>` (still be hidden in Data.Bool[1]), i.e. (==>) :: Bool -> Bool -> Bool True ==> x = x False ==> _ = True this would leave open the option to have an obvious flipped version (<==) :: Bool -> Bool -> Bool (<==) = flip (==>) [1]: Consequently, if `==>` is available only via explicit Data.Bool import, a conflict with QuickCheck's (==>) shouldn't be a big issue IMHO

David Feuer

9:21 a.m.

I don't think flipping it is the way to go; I expect things to short-circuit from left to right. On Jan 18, 2016 4:14 AM, "Herbert Valerio Riedel" wrote:

...

On 2016-01-18 at 03:17:44 +0100, Niklas Hambüchen wrote:

[...]

...
The request for this is quite old (see e.g.

http://neilmitchell.blogspot.de/2007/02/logical-implication-in-haskell.html ).

...
I believe that by not trying to use an operator for it, and keeping it in Data.Bool, we can avoid doing anything wrong.

Just wondering, what could/would go wrong if we did use an operator `==>` (still be hidden in Data.Bool[1]), i.e.

(==>) :: Bool -> Bool -> Bool True ==> x = x False ==> _ = True

this would leave open the option to have an obvious flipped version

(<==) :: Bool -> Bool -> Bool (<==) = flip (==>)

[1]: Consequently, if `==>` is available only via explicit Data.Bool import, a conflict with QuickCheck's (==>) shouldn't be a big issue IMHO _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

Andrew Butterfield

9:26 a.m.

...

On 18 Jan 2016, at 09:21, David Feuer wrote:

I don't think flipping it is the way to go; I expect things to short-circuit from left to right.

On Jan 18, 2016 4:14 AM, "Herbert Valerio Riedel" mailto:hvriedel@gmail.com> wrote: On 2016-01-18 at 03:17:44 +0100, Niklas Hambüchen wrote: this would leave open the option to have an obvious flipped version

(<==) :: Bool -> Bool -> Bool (<==) = flip (==>)

But you can short-circuit this on the left ! F <== p = not p T <== p = T Note quite the same as short circuiting ==> on the left... ;-) Andrew Butterfield School of Computer Science & Statistics Trinity College Dublin 2, Ireland

Henning Thielemann

9:27 a.m.

On Mon, 18 Jan 2016, Niklas Hambüchen wrote:

...

A quick superficial search on Stackage Hoogle suggests that adding this function should create no breakage (4 packages define their own function called `implies`, none of them import Data.Bool).

One of it is certainly my: https://hackage.haskell.org/package/utility-ht-0.0.11/docs/Data-Bool-HT.html... that you can simply import without altering 'base'.

Joachim Breitner

3:43 p.m.

Hi, Am Montag, den 18.01.2016, 03:17 +0100 schrieb Niklas Hambüchen:

...

I propose to add to Data.Bool:

-- | Boolean implication. implies :: Bool -> Bool -> Bool implies True x = x implies False _ = True

infix 4 `implies` -- same as (==)

I’m +1 on the grounds that although I know that one of <= or => cuts it, it causes extra mental work to find out which (and annoyance to find out that it is the “wrong” one). Using a name is explicit and gets it right the first time. -1 on changing the order for Bool, it would just break too much code that relies on that in a fairly obscure way. +1 for making it right-associative, as implications are usually written. Undecided about ==>. It would be nice, but the conflict with quickcheck would be annoying. Leaning towards -1. Greetings, Joachim -- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0xF0FBF51F Debian Developer: nomeata@debian.org

Andreas Abel

4:27 p.m.

+1 Same opinion as Joachim. --Andreas On 18.01.2016 16:43, Joachim Breitner wrote:

...

Hi,

Am Montag, den 18.01.2016, 03:17 +0100 schrieb Niklas Hambüchen:

...
I propose to add to Data.Bool:

-- | Boolean implication. implies :: Bool -> Bool -> Bool implies True x = x implies False _ = True

infix 4 `implies` -- same as (==)

I’m +1 on the grounds that although I know that one of <= or => cuts it, it causes extra mental work to find out which (and annoyance to find out that it is the “wrong” one). Using a name is explicit and gets it right the first time.

-1 on changing the order for Bool, it would just break too much code that relies on that in a fairly obscure way.

+1 for making it right-associative, as implications are usually written.

Undecided about ==>. It would be nice, but the conflict with quickcheck would be annoying. Leaning towards -1.

Greetings, Joachim

-- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden andreas.abel@gu.se http://www2.tcs.ifi.lmu.de/~abel/

Felipe Lessa

21 Jan 21 Jan

7:28 p.m.

+1 for either Data.Bool.implies or Data.Bool.(==>). +1 for right-associativity. Cheers, -- Felipe.

Iavor Diatchki

22 Jan 22 Jan

5:24 p.m.

Please don't change the ordering on Bool---it's been like that forever and it might lead to extremely subtle bugs that won't be caught by the compiler. I am ambivalent about adding an `implies` function as long as it is not automatically in scope. However, can anyone give some examples of using this in your code? All the ones I could think of would seem easier to follow when written with `if-then-else` or a guard. -Iavor On Thu, Jan 21, 2016 at 11:28 AM, Felipe Lessa wrote:

...

+1 for either Data.Bool.implies or Data.Bool.(==>).

+1 for right-associativity.

Cheers,

-- Felipe.

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

evan＠evan-borden.com

5:59 p.m.

+1 For not changing the Ord instance for Bool. It would be disastrous. As an aside, is the Order instance for Bool in the report? On Jan 22, 2016 12:24 PM, "Iavor Diatchki" wrote:

...

Please don't change the ordering on Bool---it's been like that forever and it might lead to extremely subtle bugs that won't be caught by the compiler.

I am ambivalent about adding an `implies` function as long as it is not automatically in scope. However, can anyone give some examples of using this in your code? All the ones I could think of would seem easier to follow when written with `if-then-else` or a guard.

-Iavor

On Thu, Jan 21, 2016 at 11:28 AM, Felipe Lessa wrote:

...
+1 for either Data.Bool.implies or Data.Bool.(==>).

+1 for right-associativity.

Cheers,

-- Felipe.

_______________________________________________ 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

evan＠evan-borden.com

6:11 p.m.

Answering my own question, yes it is in the report.

...

From the report:

...

6.1.1 Booleans

data Bool = False | True deriving (Read, Show, Eq, Ord, Enum, Bounded)

*11.1 Derived instances of Eq and * *Ord* ...For example, for the Bool datatype, we have that (True > False) == True .

On Fri, Jan 22, 2016 at 12:59 PM, evan@evan-borden.com < evan@evanrutledgeborden.dreamhosters.com> wrote:

...

+1 For not changing the Ord instance for Bool. It would be disastrous. As an aside, is the Order instance for Bool in the report? On Jan 22, 2016 12:24 PM, "Iavor Diatchki" wrote:

...
Please don't change the ordering on Bool---it's been like that forever and it might lead to extremely subtle bugs that won't be caught by the compiler.

I am ambivalent about adding an `implies` function as long as it is not automatically in scope. However, can anyone give some examples of using this in your code? All the ones I could think of would seem easier to follow when written with `if-then-else` or a guard.

-Iavor

On Thu, Jan 21, 2016 at 11:28 AM, Felipe Lessa wrote:

...
+1 for either Data.Bool.implies or Data.Bool.(==>).

+1 for right-associativity.

Cheers,

-- Felipe.

_______________________________________________ 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

David Feuer

8:13 p.m.

How exactly would making the Ord instance for Bool lazier be "disastrous"? On Fri, Jan 22, 2016 at 12:59 PM, evan@evan-borden.com wrote:

...

+1 For not changing the Ord instance for Bool. It would be disastrous. As an aside, is the Order instance for Bool in the report?

On Jan 22, 2016 12:24 PM, "Iavor Diatchki" wrote:

...
Please don't change the ordering on Bool---it's been like that forever and it might lead to extremely subtle bugs that won't be caught by the compiler.

I am ambivalent about adding an `implies` function as long as it is not automatically in scope. However, can anyone give some examples of using this in your code? All the ones I could think of would seem easier to follow when written with `if-then-else` or a guard.

-Iavor

On Thu, Jan 21, 2016 at 11:28 AM, Felipe Lessa wrote:

...
+1 for either Data.Bool.implies or Data.Bool.(==>).

+1 for right-associativity.

Cheers,

-- Felipe.

_______________________________________________ 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

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

Henning Thielemann

8:18 p.m.

On Fri, 22 Jan 2016, David Feuer wrote:

...

How exactly would making the Ord instance for Bool lazier be "disastrous"?

I think he talked about making fromEnum True = 0 and fromEnum False = 1.

Niklas Hambüchen

11:48 p.m.

On 22/01/16 18:24, Iavor Diatchki wrote:

...

I am ambivalent about adding an `implies` function as long as it is not automatically in scope. However, can anyone give some examples of using this in your code? All the ones I could think of would seem easier to follow when written with `if-then-else` or a guard.

I use it e.g. in assert (isProduction `implies` (iterations > 50)) $ ... other code ...

wren romano

25 Jan 25 Jan

5:27 p.m.

-1 for changing the Ord Bool instance, due to the likelihood of subtle bugs and regressions. -1 for using the name (==>) due to conflict with QuickCheck, Smallcheck, etc. Ambivalent about adding an implication operator distinct from (<=), mainly because I haven't needed it myself. IMO, the ordering on Bool should be defined so that it coincides with implication, thanks to the relationship to Boolean/Heyting algebras— which the current Ord instance already does. Though I do agree that if implication is given its own name then it ought to be lazy in the second argument, whereas it's not clear that (<=) should share that strictness/laziness. Personally, were I to add something like implication, I'd define it via a type class so that we can unify the things called (==>) in various testing frameworks. Of course, doing this appropriately would mean making a decent hierarchy of type classes for order/lattice theory. But given as we don't have one of those yet, I'd do it in a separate package so it could be played around with until everything fits together nicely, and then aim to get it blessed into HP rather than changing base. -- Live well, ~wren

Edward Kmett

26 Jan 26 Jan

3:23 p.m.

I don't care one way or the other about the creation of implies, I'm happy to bow to popular opinion either way. I do care about changing the strictness of the comparisons in Ord Bool, however, and that would require a rather massive survey of what breaks, and what gets slower -- one that we simply haven't done -- before I'd even start to be comfortable with it. -Edward On Mon, Jan 25, 2016 at 12:27 PM, wren romano wrote:

...

-1 for changing the Ord Bool instance, due to the likelihood of subtle bugs and regressions.

-1 for using the name (==>) due to conflict with QuickCheck, Smallcheck, etc.

Ambivalent about adding an implication operator distinct from (<=), mainly because I haven't needed it myself. IMO, the ordering on Bool should be defined so that it coincides with implication, thanks to the relationship to Boolean/Heyting algebras— which the current Ord instance already does. Though I do agree that if implication is given its own name then it ought to be lazy in the second argument, whereas it's not clear that (<=) should share that strictness/laziness.

Personally, were I to add something like implication, I'd define it via a type class so that we can unify the things called (==>) in various testing frameworks. Of course, doing this appropriately would mean making a decent hierarchy of type classes for order/lattice theory. But given as we don't have one of those yet, I'd do it in a separate package so it could be played around with until everything fits together nicely, and then aim to get it blessed into HP rather than changing base.

-- Live well, ~wren _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

3450

Age (days ago)

3458

Last active (days ago)

List overview

Download

29 comments

17 participants

participants (17)

Andreas Abel
Andrew Butterfield
Bardur Arantsson
Brent Yorgey
David Feuer
Edward Kmett
Evan Laforge
evan＠evan-borden.com
Felipe Lessa
Henning Thielemann
Herbert Valerio Riedel
Iavor Diatchki
Joachim Breitner
Jon Purdy
Niklas Hambüchen
Petr Pudlák
wren romano