containers: intersections for Set, along with Semigroup newtype

[David Casperson]

Hi Carter,

not sure if I understand exactly what you are getting at here,
but there IS a strong connection, via membership, between
lattices on True/False and set lattices:

     x ∈ A ∪ B   iff x ∈ A ∨ x ∈ B
     x ∈ A ∩ B   iff x ∈ A ∧ x ∈ B
     x ∈ A'      iff ¬ (x ∈ A)

and, in particular,

     x ∈ ∩(A ∈ P)   iff ∀(A∈P) [x ∈ A]

Lattices aren't necessarily isomorphic to their duals, even with
bounded lattices. (Take, for instance, lcm and gcd on the
non-negative integers.  The primes are atoms, there are no
co-atoms. [1])

WITH COMPLEMENT, sets form a boolean algebra which is self-dual
via De Morgan's lawas, but you need to have a universe against
which to compute complements.  Without complementation there
isn't necessarily duality.  Take for instance, finite subsets of
the integers.

Am I missing your point?

cheers,
David
-- 
David Casperson, PhD, R.P.,                  |  David.Casperson at unbc.ca
Associate Professor and Chair,               |  (250)   960-6672 Fax 960-5544
Computer Science                             |  3333 University Way
University of Northern British Columbia      |  Prince George, BC   V2N 4Z9
                                              |  CANADA

[1] several decades ago it took me an embarrasingly long time to
convince the Maple community that lcm(0,0)=0 was the sensible
lattice-theoretic definition.

Carter Schonwald, on 2020-12-21, you wrote:

> From: Carter Schonwald <carter.schonwald at gmail.com>
> To: Tom Ellis <tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk>,
>     Haskell Libraries <libraries at haskell.org>
> Date: Mon, 21 Dec 2020 08:12:27
> Subject: Re: containers: intersections for Set, along with Semigroup newtype
> Message-ID:
>     <CAHYVw0zhxPAF1fOK=Ow1ikdHETn+6pDEvWNV6UsNrygxvZMiXA at mail.gmail.com>
> 
> 
> CAUTION: This email is not from UNBC. Avoid links and attachments. Don't buy gift cards.
> 
> 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
> 
> 
>
-------------- next part --------------
_______________________________________________
Libraries mailing list
Libraries at haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries