Proposal: Data.Bool.implies

[Brent Yorgey]

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 <david.feuer at gmail.com> 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.
>
> On Mon, Jan 18, 2016 at 1:57 AM, Evan Laforge <qdunkan at gmail.com> 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 <david.feuer at gmail.com>
> 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 <evincarofautumn at gmail.com>
> 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 <david.feuer at gmail.com>
> wrote:
> >>>>
> >>>> -1. We already have a `<=` operator.
> >>>>
> >>>> On Sun, Jan 17, 2016 at 9:17 PM, Niklas Hambüchen <mail at nh2.me>
> 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 at haskell.org
> >>>> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> >>>> _______________________________________________
> >>>> Libraries mailing list
> >>>> Libraries at haskell.org
> >>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> >>>
> >>>
> >> _______________________________________________
> >> Libraries mailing list
> >> Libraries at haskell.org
> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20160118/ac390b5f/attachment.html>