containers: intersections for Set, along with Semigroup newtype
Locked
12
12
 
|
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 |
|
|
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 |
Re: containers: intersections for Set, along with Semigroup newtype
|
|
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 |
Re: containers: intersections for Set, along with Semigroup newtype
|
|
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 |
|
|
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 |
Re: containers: intersections for Set, along with Semigroup newtype
|
|
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. 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 |
|
|
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:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
|
|
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 |
|
|
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: _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
|
|
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 |
|
|
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 |
|
|
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 |
|
|
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 |
|
|
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 |
|
|
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 |
|
|
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 _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
|
|
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 |
|
|
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 |
|
|
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 |
«
Return to Haskell - Libraries
|
1 view|%1 views
| Free forum by Nabble | Edit this page |