<div dir="ltr">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.<br><div><br></div><div>-Brent<br></div><div><br><div class="gmail_quote"><div dir="ltr">On Mon, Jan 18, 2016 at 1:04 AM David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I agree with you that    not a || b   says something a bit different<br>
from  a `implies` b in a more general logical context. However, I<br>
believe that  a <= b  says exactly the same thing. It's true that it<br>
may not be quite obvious to everyone, but anyone thinking enough about<br>
logic to *want* an implies function should probably be willing to<br>
learn such things.<br>
<br>
On Mon, Jan 18, 2016 at 1:57 AM, Evan Laforge <<a href="mailto:qdunkan@gmail.com" target="_blank">qdunkan@gmail.com</a>> wrote:<br>
> I have only very rarely needed 'implies' and when I do I'm happy with<br>
> 'if a then b else False'.  But if I needed to do that a lot, I would<br>
> write my own function and certainly never use (<=), because I wouldn't<br>
> guess that (<=) has the same logic as implies.  And even if it does,<br>
> isn't the means more important than the end?  For the same reason I<br>
> wouldn't write 'not a || b' because when I want to say implies I'll<br>
> just directly say implies.<br>
><br>
> On Mon, Jan 18, 2016 at 11:44 AM, David Feuer <<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>> wrote:<br>
>> I think changing the Ord instance for Bool *may* be the way to go.<br>
>> Yes, the lazy one is likely a bit less efficient in some cases, but I<br>
>> somehow doubt many are relying on it to be fast. Moreover, people<br>
>> expect most Bool operations to short-circuit (I even seem to have lost<br>
>> that fight wrt the Data.Bits operations, which I firmly believe should<br>
>> be *strict*).<br>
>><br>
>> instance Ord Bool where<br>
>>   False <= _ = True<br>
>>   True <= x = x<br>
>><br>
>>   True >= _ = True<br>
>>   False >= x = not x<br>
>><br>
>>   False < x = x<br>
>>   True < _ = False<br>
>><br>
>>   False > _ = False<br>
>>   True > x = not x<br>
>><br>
>><br>
>> On Mon, Jan 18, 2016 at 12:23 AM, Jon Purdy <<a href="mailto:evincarofautumn@gmail.com" target="_blank">evincarofautumn@gmail.com</a>> wrote:<br>
>>> +1. “<=” has the wrong strictness. In “a `implies` b”, “b” should not be<br>
>>> evaluated if “a” is false.<br>
>>><br>
>>> As a strawman, I’d propose that the Ord instance for Bool be changed—but<br>
>>> this is more likely to break existing code, however slightly.<br>
>>><br>
>>> On Sun, Jan 17, 2016 at 8:12 PM, David Feuer <<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>> wrote:<br>
>>>><br>
>>>> -1. We already have a `<=` operator.<br>
>>>><br>
>>>> On Sun, Jan 17, 2016 at 9:17 PM, Niklas Hambüchen <<a href="mailto:mail@nh2.me" target="_blank">mail@nh2.me</a>> wrote:<br>
>>>> > I propose to add to Data.Bool:<br>
>>>> ><br>
>>>> >     -- | Boolean implication.<br>
>>>> >     implies :: Bool -> Bool -> Bool<br>
>>>> >     implies True  x = x<br>
>>>> >     implies False _ = True<br>
>>>> ><br>
>>>> >     infix 4 `implies` -- same as (==)<br>
>>>> ><br>
>>>> > The request for this is quite old (see e.g.<br>
>>>> ><br>
>>>> > <a href="http://neilmitchell.blogspot.de/2007/02/logical-implication-in-haskell.html" rel="noreferrer" target="_blank">http://neilmitchell.blogspot.de/2007/02/logical-implication-in-haskell.html</a>).<br>
>>>> ><br>
>>>> > I believe that by not trying to use an operator for it, and keeping it<br>
>>>> > in Data.Bool, we can avoid doing anything wrong.<br>
>>>> ><br>
>>>> > A quick superficial search on Stackage Hoogle suggests that adding this<br>
>>>> > function should create no breakage (4 packages define their own function<br>
>>>> > called `implies`, none of them import Data.Bool).<br>
>>>> ><br>
>>>> > `infix` instead of `infixl` or `infixr` to force you to bracket it; for<br>
>>>> > the same reason it has the same precedence as `==`.<br>
>>>> > _______________________________________________<br>
>>>> > Libraries mailing list<br>
>>>> > <a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
>>>> > <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
>>>> _______________________________________________<br>
>>>> Libraries mailing list<br>
>>>> <a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
>>>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
>>><br>
>>><br>
>> _______________________________________________<br>
>> Libraries mailing list<br>
>> <a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div></div></div>