containers: intersections for Set, along with Semigroup newtype

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
39 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

Tom Ellis-5
On Mon, Dec 21, 2020 at 07:19:49PM +0100, Ben Franksen wrote:
> 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
[...]

> 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

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.

Tom
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

Oleg Grenrus
In reply to this post by Ben Franksen
lattice package has 'not':
https://hackage.haskell.org/package/lattices-2.0.2/docs/Algebra-Heyting.html#v:neg

- 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 <
>> [hidden email]> 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 <
>>> [hidden email]> 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
>>>> [hidden email]
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>
>>
>> _______________________________________________
>> Libraries mailing list
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

David Casperson
In reply to this post by Carter Schonwald
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.,                  |  [hidden email]
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 <[hidden email]>
> To: Tom Ellis <[hidden email]>,
>     Haskell Libraries <[hidden email]>
> Date: Mon, 21 Dec 2020 08:12:27
> Subject: Re: containers: intersections for Set, along with Semigroup newtype
> Message-ID:
>     <CAHYVw0zhxPAF1fOK=[hidden email]>
>
>
> 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 <[hidden email]> 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
>       [hidden email]
>       http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>
>
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Viktor Dukhovni
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.

--
    Viktor.
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

Ben Franksen
In reply to this post by Tom Ellis-5
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

David Casperson
In reply to this post by Viktor Dukhovni
Hi Viktor.  On 2020-12-21, you wrote:

> From: Viktor Dukhovni <[hidden email]>
> To: [hidden email]
> Reply-To: [hidden email]
> Date: Mon, 21 Dec 2020 14:25:40
> Subject: Re: containers: intersections for Set, along with Semigroup newtype
> Message-ID: <X+Eg5G7LDyy2OT/[hidden email]>
>
> 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

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

Oliver Charles-3
In reply to this post by Tom Ellis-5
I've wanted it when writing DSLs. For example, when doing SQL query generation, if you have some Expr a type to represent database expressions of type 'a', it'd be nice to be able to have && "just work" on them, much like how we can add a Num (Expr a) instance. If other functions were written in terms of Bool, these are trivially useful on Expr now, but without that they have to be re-implemented.

On Mon, 21 Dec 2020, at 6:54 PM, Tom Ellis wrote:
On Mon, Dec 21, 2020 at 07:19:49PM +0100, Ben Franksen wrote:
> 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
[...]
> 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

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.

Tom
_______________________________________________
Libraries mailing list



_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

Ben Franksen
In reply to this post by Oleg Grenrus
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#v:neg

Oh, nice! (Though 'neg' is not quite as suggestive as 'not'.)

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

Tikhon Jelvis
In reply to this post by Ben Franksen
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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

David Feuer
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 <[hidden email]> 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 <[hidden email]> 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
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

David Casperson
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
--
David Casperson
Computer Science

David Feuer, on 2020-12-21, you wrote:

> From: David Feuer <[hidden email]>
> To: Tikhon Jelvis <[hidden email]>
> Date: Mon, 21 Dec 2020 15:49:18
> Cc: Ben Franksen <[hidden email]>,
>     Haskell Libraries <[hidden email]>
> Subject: Re: type class Boolean
> Message-ID:
>     <CAMgWh9s1V7=[hidden email]>
>
> CAUTION: This email is not from UNBC. Avoid links and attachments. Don't buy gift cards.
>
>
> 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 <[hidden email]> 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 <[hidden email]> 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
>>> [hidden email]
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>> _______________________________________________
>> Libraries mailing list
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

Oleg Grenrus
In reply to this post by Ben Franksen
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#v:neg
> Oh, nice! (Though 'neg' is not quite as suggestive as 'not'.)
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

Oleg Grenrus
In reply to this post by David Casperson
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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

Johannes Waldmann-2
In reply to this post by Ben Franksen
[I sent this to -cafe by mistake]

> most useful kind of instance would be symbolic booleans

Yes. Ersatz has this:

https://hackage.haskell.org/package/ersatz-0.4.8/docs/Ersatz-Bit.html#t:Boolean

I also use this class (re-exported) in
https://hackage.haskell.org/package/obdd

Then modules typically start with

import Prelude hiding ( not, and, or, (&&), (||) ) -- possibly more
import Ersatz

slightly annoying but you get used to it ...

- J.
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

Ben Franksen
In reply to this post by Oleg Grenrus
Am 22.12.20 um 11:40 schrieb Oleg Grenrus:
> I didn't want to clash with Prelude names. Also in Heyting-generality
> "not" is not correct either. (In general, neg is not involutive).

Yes, obviously. I still think a class Boolean for boolean algebras (with
the usual operators now limited to Bool) would be nice. I don't care too
much whether it has HeytingAlgebra as super class or not, since I have
never had any use for the more general classes. I think I mentioned in
the beginning that my main motivation is convenience. Predicates are
ubiquitous in programming and the desire to combine them using
generalized boolean operators crops up almost everywhere.

It amazes me how the designers of Haskell included this elaborate
hierarchy of types and classes for all sorts of numbers in the standard
libraries, but apparently never thought of generalizing booleans to
predicates (and other boolean algebras).

Cheers
Ben

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

Jon Purdy
In reply to this post by Ben Franksen
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.



On Mon, Dec 21, 2020 at 10:20 AM Ben Franksen <[hidden email]> 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 <
> [hidden email]> 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 <
>> [hidden email]> 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
>>> [hidden email]
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>
>>
>
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

Ben Franksen
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

Oleg Grenrus
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.HTM
[5]
https://web.archive.org/web/20090604210339/http://home.ccil.org/~remlaps/www.bobbemer.com/BRACES.HTM

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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: type class Boolean

Ben Franksen
Thanks!

Am 27.12.20 um 22:05 schrieb Oleg Grenrus:

> 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.HTM
> [5]
> https://web.archive.org/web/20090604210339/http://home.ccil.org/~remlaps/www.bobbemer.com/BRACES.HTM
>
> 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
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
12