<div dir="ltr"><div>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.</div><div><br></div><div>class HeytingAlgebra a where<br></div><div> ff :: a<br></div><div> tt :: a<br></div><div> implies :: a -> a -> a<br></div><div> conj :: a -> a -> a -- aliased to (&&)<br></div><div> disj :: a -> a -> a -- aliased to (||)<br></div><div> not :: a -> a<br></div><div><br></div><div>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:<br></div><div><br></div><div> a && (a `implies` b) = a && b<br></div><div>b && (a `implies` b) = b<br></div><div>not a = a `implies` ff</div><div><br></div><div>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.<br></div><div><br></div><div>[1] <a href="https://pursuit.purescript.org/packages/purescript-prelude/4.1.1/docs/Data.HeytingAlgebra">https://pursuit.purescript.org/packages/purescript-prelude/4.1.1/docs/Data.HeytingAlgebra</a></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Dec 21, 2020 at 10:20 AM Ben Franksen <<a href="mailto:ben.franksen@online.de">ben.franksen@online.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">All this talk about lattices reminds me of one of my pet gripes I have<br>
with the standard libraries (base), namely that the boolean operators<br>
aren't overloaded. I don't want to open endless discussions about the<br>
perfect generalization, because there are lots of valid generalizations<br>
and the lattice package is fine for those.<br>
<br>
But most generalizations don't have a 'not' (complement) operator. So, a<br>
simple type class Boolean with instances for Bool and functions<br>
returning Booleans should cover the majority of use cases; more<br>
instances could be added of course. Something like<br>
<br>
{-# LANGUAGE NoImplicitPrelude #-}<br>
module Data.Boolean where<br>
<br>
import Prelude hiding ((&&),(||),not)<br>
import qualified Prelude<br>
<br>
infixr 3 &&<br>
infixr 2 ||<br>
<br>
class Boolean a where<br>
-- laws: that of a boolean algebra, i.e.<br>
-- complemented distributive lattice, see<br>
-- <a href="https://en.wikipedia.org/wiki/Boolean_algebra#Laws" rel="noreferrer" target="_blank">https://en.wikipedia.org/wiki/Boolean_algebra#Laws</a><br>
(&&) :: a -> a -> a<br>
(||) :: a -> a -> a<br>
not :: a -> a<br>
top :: a<br>
bottom :: a<br>
<br>
instance Boolean Bool where<br>
(&&) = (Prelude.&&)<br>
(||) = (Prelude.||)<br>
not = Prelude.not<br>
top = True<br>
bottom = False<br>
<br>
instance Boolean b => Boolean (a->b) where<br>
(f && g) x = f x && g x<br>
(f || g) x = f x || g x<br>
(not f) x = not (f x)<br>
top = const top<br>
bottom = const bottom<br>
<br>
IMHO this would be absolutely benign, no problems with type inference,<br>
fully Haskell98, no breakage of existing code I can think of. (I didn't<br>
check that last point but I would be very surprised if there were.)<br>
<br>
Cheers<br>
Ben<br>
<br>
Am 21.12.20 um 17:14 schrieb Carter Schonwald:<br>
> edit: neglected to mention that choosing which lattice (and or dual) to use<br>
> only really matters when considering products/sums of lattices to form new<br>
> lattices<br>
> <br>
> On Mon, Dec 21, 2020 at 11:12 AM Carter Schonwald <<br>
> <a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>> wrote:<br>
> <br>
>> why are we equating the lattice operators for True and false with the<br>
>> lattice operators for set? (for both structures, we have the dual partial<br>
>> order is also a lattice, so unless we have )<br>
>> (i'm going to get the names of these equations wrong, but )<br>
>><br>
>> the "identity" law is going to be max `intersect` y == y , min `union` y<br>
>> === y<br>
>><br>
>> the "absorbing" law is going to be min `intersect` y == min , max<br>
>> `union` y == max<br>
>><br>
>> these rules work the same for (min = emptyset, max == full set, union ==<br>
>> set union, intersect == set intersecct)<br>
>> OR for its dual lattice (min == full set, max == emtpy set, union = set<br>
>> intersection, intersect == set union)<br>
>><br>
>> at some level arguing about the empty list case turns into artifacts of<br>
>> "simple" definitions<br>
>><br>
>> that said, i suppose a case could be made that for intersect :: [a] -> a ,<br>
>> that as the list argument gets larger the result should be getting<br>
>> *smaller*, so list intersect of lattice elements should be "anti-monotone",<br>
>> and list union should be monotone (the result gets bigger). I dont usually<br>
>> see tht<br>
>><br>
>> either way, I do strongly feel that either way, arguing by how we choose<br>
>> to relate the boolean lattice and seet lattices is perhaps the wrong<br>
>> choice... because both lattices are equivalent to theeir dual lattice<br>
>><br>
>> On Mon, Dec 21, 2020 at 5:12 AM Tom Ellis <<br>
>> <a href="mailto:tom-lists-haskell-cafe-2017@jaguarpaw.co.uk" target="_blank">tom-lists-haskell-cafe-2017@jaguarpaw.co.uk</a>> wrote:<br>
>><br>
>>> On Sun, Dec 20, 2020 at 11:05:39PM +0100, Ben Franksen wrote:<br>
>>>> Am 06.12.20 um 19:58 schrieb Sven Panne:<br>
>>>>> To me it's just the other way around: It violates aesthetics if it<br>
>>> doesn't<br>
>>>>> follow the mathematical definition in all cases, which is why I don't<br>
>>> like<br>
>>>>> NonEmpty here.<br>
>>>><br>
>>>> I think you've got that wrong.<br>
>>>><br>
>>>> x `elem` intersections []<br>
>>>> = {definition}<br>
>>>> forall xs in []. x `elem` xs<br>
>>>> = {vacuous forall}<br>
>>>> true<br>
>>>><br>
>>>> Any proposition P(x) is true for all x in []. So the mathematical<br>
>>>> definition of intersections::[Set a]-> Set a would not be the empty set<br>
>>>> but the set of all x:a, which in general we have no way to construct.<br>
>>><br>
>>> Yes, and to bring this back to Sven's original claim<br>
>>><br>
>>> | Why NonEmpty? I would expect "intersections [] = Set.empty", because<br>
>>> | the result contains all the elements which are in all sets,<br>
>>> | i.e. none. That's at least my intuition, is there some law which<br>
>>> | this would violate?<br>
>>><br>
>>> the correct definition of "intersections []" should be "all elements<br>
>>> which are in all of no sets" i.e. _every_ value of the given type!<br>
>>><br>
>>> Tom<br>
>>> _______________________________________________<br>
>>> Libraries mailing list<br>
>>> <a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
>>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
>>><br>
>><br>
> <br>
> <br>
> _______________________________________________<br>
> Libraries mailing list<br>
> <a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
> <br>
<br>
<br>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div>