type class Boolean

David Casperson casper at unbc.ca
Tue Dec 22 01:17:24 UTC 2020


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 <david.feuer at gmail.com>
> To: Tikhon Jelvis <tikhon at jelv.is>
> Date: Mon, 21 Dec 2020 15:49:18
> Cc: Ben Franksen <ben.franksen at online.de>,
>     Haskell Libraries <libraries at haskell.org>
> Subject: Re: type class Boolean
> Message-ID:
>     <CAMgWh9s1V7=7KGku0KnVF0FV_zFANm6K6pxCwLdpPxxyQDXShQ at mail.gmail.com>
> 
> 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 <tikhon at jelv.is> 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 <ben.franksen at online.de> 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 at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>


More information about the Libraries mailing list