type class Boolean

Wed Dec 23 21:40:31 UTC 2020

Just as a point of reference in the design space, some of which has already
been brought up, PureScript does this with its ‘HeytingAlgebra’ class[1],
which also includes implication. Booleans and predicates are both instances.

class HeytingAlgebra a where
  ff :: a
  tt :: a
  implies :: a -> a -> a
  conj :: a -> a -> a  -- aliased to (&&)
  disj :: a -> a -> a  -- aliased to (||)
  not :: a -> a

This has the standard laws for a Heyting algebra: AND and OR are
associative, commutative, and idempotent; implication is also idempotent;
true and false are identities for AND and OR, respectively; AND and OR are
related by absorption; implication distributes over AND, and the following
whose names (if they are named) I don’t actually know:

a && (a `implies` b) = a && b
b && (a `implies` b) = b
not a = a `implies` ff

As bikesheds go, I prefer your names ‘top’ and ‘bottom’ over ‘tt’ and ‘ff’;
generalising ‘(&&)’ and ‘(||)’ is fine if it doesn’t cause ambiguity
issues, otherwise I like ‘(/\)’ and ‘(\/)’—which, after all, are the very
reason the backslash was added to ASCII in the first place.

[1]
https://pursuit.purescript.org/packages/purescript-prelude/4.1.1/docs/Data.HeytingAlgebra

On Mon, Dec 21, 2020 at 10:20 AM Ben Franksen <ben.franksen at online.de>
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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20201223/a4e9ddc4/attachment.html>