containers: intersections for Set, along with Semigroup newtype

[David Casperson]

Hi Viktor.  On 2020-12-21, you wrote:

> From: Viktor Dukhovni <ietf-dane at dukhovni.org>
> To: libraries at haskell.org
> Reply-To: libraries at haskell.org
> Date: Mon, 21 Dec 2020 14:25:40
> Subject: Re: containers: intersections for Set, along with Semigroup newtype
> Message-ID: <X+Eg5G7LDyy2OT/5 at straasha.imrryr.org>
> 
> On Mon, Dec 21, 2020 at 02:06:33PM -0800, David Casperson wrote:
>
>> 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])
>
> But the non-negative integers with gcd and lcm are surely not a bounded
> lattice.  If we introduce an upper bound by restricting attention to
> numbers that are factors of some number n > 1, then surely co-atoms
> reappear in the form of n/p for each prime factor of n.

If we define a partial order by x≤y iff x divides y (x|y in the
sequel, meaning for clarity ∃k kx=y) there is a lattice structure
giving by meet being gcd, and join by lcm, and there are bounds:
∀x 1|x, and ∀x x|0, so 1 is ⊥, and 0 is ⊤.  Regardless of whether
one likes having 0|0, this is a perfectly well-defined lattice,
and there are no co-atoms; there is no largest (w.r.t. |)
non-negative integer not divisible by 3.

Some people want to insist that x|y ifF y/x exists, that is,
∃!k kx=y, in which case all of the preceding paragraph is true,
except for the fact that we no longer have a lattice because we
are refusing to define 0∨0 and 0∧0, notwithstanding the existence
of a consistent possible extension.

Alternatively, take your favourite lower-bounded, upper-unbounded
lattice, and add an element ∞, and extend meet and join so that
x∧∞=x, x∨∞=∞.  You can check that the result also satisfies the
lattice laws.

Happy Solstice!
stay safe!


David
-- 
David Casperson
Computer Science