type class Boolean

[Oleg Grenrus]

lattice package has 'not':
https://hackage.haskell.org/package/lattices-2.0.2/docs/Algebra-Heyting.html#v:neg

- Oleg

On 21.12.2020 20.19, Ben Franksen wrote:
> 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
>>
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries