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.H...
On Mon, Dec 21, 2020 at 10:20 AM 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
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@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
Am 21.12.20 um 17:14 schrieb Carter Schonwald: 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@jaguarpaw.co.uk> 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
On Sun, Dec 20, 2020 at 11:05:39PM +0100, Ben Franksen wrote: 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries