type class Boolean

[Ben Franksen]

All this talk about lattices reminds me of one of my pet gripes I have
with the standard libraries (base), namely that the boolean operators
aren't overloaded. I don't want to open endless discussions about the
perfect generalization, because there are lots of valid generalizations
and the lattice package is fine for those.

But most generalizations don't have a 'not' (complement) operator. So, a
simple type class Boolean with instances for Bool and functions
returning Booleans should cover the majority of use cases; more
instances could be added of course. Something like

{-# LANGUAGE NoImplicitPrelude #-}
module Data.Boolean where

import Prelude hiding ((&&),(||),not)
import qualified Prelude

infixr 3 &&
infixr 2 ||

class Boolean a where
  -- laws: that of a boolean algebra, i.e.
  -- complemented distributive lattice, see
  -- https://en.wikipedia.org/wiki/Boolean_algebra#Laws
  (&&) :: a -> a -> a
  (||) :: a -> a -> a
  not :: a -> a
  top :: a
  bottom :: a

instance Boolean Bool where
  (&&) = (Prelude.&&)
  (||) = (Prelude.||)
  not = Prelude.not
  top = True
  bottom = False

instance Boolean b => Boolean (a->b) where
  (f && g) x = f x && g x
  (f || g) x = f x || g x
  (not f) x = not (f x)
  top = const top
  bottom = const bottom

IMHO this would be absolutely benign, no problems with type inference,
fully Haskell98, no breakage of existing code I can think of. (I didn't
check that last point but I would be very surprised if there were.)

Cheers
Ben

Am 21.12.20 um 17:14 schrieb Carter Schonwald:
> edit: neglected to mention that choosing which lattice (and or dual) to use
> only really matters when considering products/sums of lattices to form new
> lattices
> 
> On Mon, Dec 21, 2020 at 11:12 AM Carter Schonwald <
> carter.schonwald at gmail.com> wrote:
> 
>> why are we equating the lattice operators for True and false with the
>> lattice operators for set? (for both structures, we have the dual partial
>> order is also a lattice, so unless we have )
>> (i'm going to get the names of these equations wrong, but )
>>
>> the "identity" law is going to be  max `intersect` y == y ,  min `union` y
>> === y
>>
>> the "absorbing" law is going to be   min `intersect` y == min , max
>> `union` y == max
>>
>> these rules work the same for (min = emptyset, max == full set, union ==
>> set union, intersect == set intersecct)
>> OR for its dual lattice (min == full set, max == emtpy set, union = set
>> intersection, intersect == set union)
>>
>> at some level arguing about the empty list case turns into artifacts of
>> "simple" definitions
>>
>> that said, i suppose a case could be made that for intersect :: [a] -> a ,
>> that as the list argument gets larger the result should be getting
>> *smaller*, so list intersect of lattice elements should be "anti-monotone",
>> and list union should be monotone (the result gets bigger). I dont usually
>> see tht
>>
>> either way, I do strongly feel that either way, arguing by how we choose
>> to relate the boolean lattice and seet lattices is perhaps the wrong
>> choice... because both lattices are equivalent to theeir dual lattice
>>
>> On Mon, Dec 21, 2020 at 5:12 AM Tom Ellis <
>> tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk> wrote:
>>
>>> On Sun, Dec 20, 2020 at 11:05:39PM +0100, Ben Franksen wrote:
>>>> Am 06.12.20 um 19:58 schrieb Sven Panne:
>>>>> To me it's just the other way around: It violates aesthetics if it
>>> doesn't
>>>>> follow the mathematical definition in all cases, which is why I don't
>>> like
>>>>> NonEmpty here.
>>>>
>>>> I think you've got that wrong.
>>>>
>>>>   x `elem` intersections []
>>>> = {definition}
>>>>   forall xs in []. x `elem` xs
>>>> = {vacuous forall}
>>>>   true
>>>>
>>>> Any proposition P(x) is true for all x in []. So the mathematical
>>>> definition of intersections::[Set a]-> Set a would not be the empty set
>>>> but the set of all x:a, which in general we have no way to construct.
>>>
>>> Yes, and to bring this back to Sven's original claim
>>>
>>> | Why NonEmpty? I would expect "intersections [] = Set.empty", because
>>> | the result contains all the elements which are in all sets,
>>> | i.e. none. That's at least my intuition, is there some law which
>>> | this would violate?
>>>
>>> the correct definition of "intersections []" should be "all elements
>>> which are in all of no sets" i.e. _every_ value of the given type!
>>>
>>> Tom
>>> _______________________________________________
>>> 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
>