Re: containers: intersections for Set, along with Semigroup newtype

21 Dec 2020

      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@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 
To: Tom Ellis ,
    Haskell Libraries 
Date: Mon, 21 Dec 2020 08:12:27
Subject: Re: containers: intersections for Set, along with Semigroup newtype
Message-ID:

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  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@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