On Sun, 6 Dec 2020, Reed Mullanix wrote:

In a perfect world we would use something like Foldable1 from semigroupoids, but sadly that is not in base.

Is it necessary to have it in base for your use? For me, 'NonEmpty.foldl1 Set.intersection' is perfect.

Am So., 6. Dez. 2020 um 19:56 Uhr schrieb Reed Mullanix < reedmullanix@gmail.com>:

It doesn't violate any laws per say, due to the general lawlessness of Foldable, but violates aesthetics. [...]

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.

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

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

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 Am 21.12.20 um 17:14 schrieb Carter Schonwald:

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

Am 21.12.20 um 19:54 schrieb Tom Ellis:

I think it's worth seeing more instances. As it is I don't understand in what situations one would use these polymorphically and therefore why `liftA2 (&&)`, `fmap not`, `pure True` and friends wouldn't suffice.

As with all overloading it's partly a matter of convenience. For instance you can't use 'liftA2 (&&)' as an operator. And your list of alternatives above demonstrates that one has to remember which lifting operator (pure, fmap, liftA2) to use, depending on arity.

I imagine you'd want (&&) and (||) to live in a Lattice class, `bottom` and `top` in `BoundedBelow` and `BoundedAbove`, respectively, and `not` in a `Boolean` one. The relationship between Lattice, JoinSemilattice, and MeetSemilattice is unfortunately awkward (much like that between Ring, AbelianGroup, and Monoid), but mumble mumble something. On Mon, Dec 21, 2020 at 6:32 PM Tikhon Jelvis wrote:

For me, the most useful kind of instance would be symbolic booleans like SBV's SBool type.

A real bonus would be making if-then-else polymorphic as well—although that doesn't really fit with the lattice abstraction. I know we can do that with RebindableSyntax, but that is a *heavyweight* extension to enable!

Breaking boolean behavior up into a few different classes would work for this application. Boolean algebras for and/not/etc, Conditional for ifThenElse and maybe even Boolish or something for True and False pattern synonyms (or just true and false constants).

I don't think all of this belongs in base, but making booleans and boolean operators more polymorphic would definitely be useful.

On Mon, Dec 21, 2020 at 3:21 PM Ben Franksen wrote:

...

Am 21.12.20 um 19:54 schrieb Tom Ellis:

...

I think it's worth seeing more instances. As it is I don't understand in what situations one would use these polymorphically and therefore why `liftA2 (&&)`, `fmap not`, `pure True` and friends wouldn't suffice.

As with all overloading it's partly a matter of convenience. For instance you can't use 'liftA2 (&&)' as an operator. And your list of alternatives above demonstrates that one has to remember which lifting operator (pure, fmap, liftA2) to use, depending on arity.

_______________________________________________ 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

You describe the lattices package. [1] - There is Lattice class with /\ and \/ - BoundedJoinSemiLattice and BoundedMeetSemiLattice with bottom and top - Heyting with ==> and neg I don't think that functionality should be part of base. The design is not clear and hard to agree on. There is also semilattices [2] package which takes different route There are no intermediate, additional Modular or Distributive or Boolean in lattices package, because these would be classes without members. I consider such a bad design in Haskell, so I omitted them. (Some people argue that there should be class Monoid m => CommutativeMonoid m, and there are plenty discussion why this is good or bad, or can be made ok). - Oleg [1] https://hackage.haskell.org/package/lattices [2] https://hackage.haskell.org/package/semilattices On 22.12.2020 3.17, David Casperson wrote:

Hi all,

let's start at lattices, a set with ∨ and ∧, where a∧(a∨b) ≈ a, a∨(a∧b) ≈ a, and ∨ and ∧ are commutative, associative, and idempotent.  To get to Boolean algebras, we need to add

a. bounds, b. distributivity, and c. complements.

Given any lattice, you can always add a +∞ and a -∞ to get a bounded lattice (there is a functor ...).  So I think that from the point of view of class structure Lattice and Bounded can exist independently.  At least for lattices, upper and lower bounds are independent, so ??maybe?? a OneSidedBounded class.

Not all lattices are distributive [i.e., they don't autmoatically satisfy a∧(c∨b) ≈ (a∧c)∨(a∧b), a∨(c∧b) ≈ (a∨c)∧(a∨b) ].  A class between lattice and DistributiveLattice that might be useful is ModularLattice (lattices with a notion of "height").  There are also meet semi-distributive ... (I'm not an expert on lattice theory, but I know several).  Most people are most familiar with distributive lattices.

Similarly, not all bounded distributive lattices have a complement operation.  A bounded distributive lattice with a complement operation that satisfies De Morgan's laws and a′′≈a (alternatively a′∨a≈⊤) is a Boolean algebra.  There is a strictly weaker notion of a Heyting algebra, which might be useful as a class, because it uses implication (→) as a fundamental operation in place of not (′).  Usually in a Heyting algebra a′ is defined to mean a→⊥.  There are Heyting algebras where a′∨a≈⊤ doesn't hold.

As a programmer, I haven't seen a non-Boolean Heyting algebra in "the wild", or at least not recognized them, but it doesn't mean they wouldn't be useful.

At any rate, these are some of the things that I would think about while simultaneously trying to avoid to much bikeshedding on the one hand, and suddenly forcefully retro-fitting Applicative (or Semigroup) on the other.

hth,

stay safe! Happy Solstice!

David

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

lattice package has 'not': https://hackage.haskell.org/package/lattices-2.0.2/docs/Algebra-Heyting.html... - Oleg On 21.12.2020 20.19, Ben Franksen wrote:

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

Am 21.12.20 um 17:14 schrieb Carter Schonwald:

...

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

I didn't want to clash with Prelude names. Also in Heyting-generality "not" is not correct either. (In general, neg is not involutive). - Oleg On 22.12.2020 1.28, Ben Franksen wrote:

Am 21.12.20 um 21:04 schrieb Oleg Grenrus:

...

lattice package has 'not': https://hackage.haskell.org/package/lattices-2.0.2/docs/Algebra-Heyting.html... Oh, nice! (Though 'neg' is not quite as suggestive as 'not'.)

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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 wrote:

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

Wikipedia [1] has references

Bob Bemer added the \ character to the ASCII character set on September 18, 1961,[3][4] as the result of character frequency studies. In particular, the \ was introduced so that the ALGOL boolean operators ∧ (and) and ∨ (or) could be composed in ASCII as /\ and \/ respectively.[4][5]

- Oleg [1] https://en.wikipedia.org/wiki/Backslash [3] http://www.thocp.net/biographies/bemer_bob.htm [4] https://web.archive.org/web/20130119163809/http://www.bobbemer.com/BACSLASH.... [5] https://web.archive.org/web/20090604210339/http://home.ccil.org/~remlaps/www... On 27.12.2020 12.03, Ben Franksen wrote:

Am 23.12.20 um 22:40 schrieb Jon Purdy:

...

otherwise I like ‘(/\)’ and ‘(\/)’—which, after all, are the very reason the backslash was added to ASCII in the first place. Interesting. Out of curiosity: do you have a reference for this?

Cheers Ben

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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

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

From: Viktor Dukhovni To: libraries@haskell.org Reply-To: libraries@haskell.org Date: Mon, 21 Dec 2020 14:25:40 Subject: Re: containers: intersections for Set, along with Semigroup newtype Message-ID:

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

I would be opposed to intersections [] = [] as it is true that *all* things have the property of being a member of every element of []. In set theory without classes I've usually seen this worked around by never using intersections on an empty set (ie using NonEmpty) ======= Georgi

Intersection is a lattice operation, whose identity element is the "whole universe" not the empty set. Imagine if we had an intersections :: [Set a] -> Set a we would expect it have the law intersections (a ++ b) = (intersections a) `intersect` (intersections b) now let b be [] and aa == intersections a, and we get aa == aa `intersect` (intersections []) and this must hold for all aa, which is impossible unless we have some kind of universe set. 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 Sven Panne, on 2020-12-06, you wrote:

From: Sven Panne To: Reed Mullanix Date: Sun, 6 Dec 2020 10:50:13 Cc: Haskell Libraries 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.

Am So., 6. Dez. 2020 um 07:20 Uhr schrieb Reed Mullanix : [...]   intersections :: Ord a => NonEmpty (Set a) -> Set a   intersections (s :| ss) = Foldable.foldl' intersection s ss [...]

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?

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries