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