type class Boolean

[Oleg Grenrus]

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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries