Break up BooleanAlgebra

[paf31]

cc @freebroccolo

We discussed modifying the BooleanAlgebra hierarchy on IRC.

I'd like to support some simple overloading of the boolean operations, while not splitting things into a full hierarchy of Lattices, which I think would be fine in another library.

I propose:

• Split out HeytingAlgebra
• Make Bounded a subclass of Ord
• Copy the Bounded members into HeytingAlgebra

as follows:

-- See https://en.wikipedia.org/wiki/Heyting_algebra#Bounded_lattice_with_an_implication_operation
--
-- a ==> a = tr
-- a && (a ==> b) = a ==> b
-- b && (a ==> b) = b
-- a ==> (b && c) = (a ==>b) && (a ==> c)
--
-- plus the laws for a bounded lattice
--
-- plus `not a = a ==> fa`
class HeytingAlgebra h where
  tr :: h
  fa :: h
  implies :: h -> h -> h
  conj :: h -> h -> h
  disj :: h -> h -> h
  not :: h -> h

infix ==> as implies -- for the purposes of writing out the laws above

infix && as conj
infix || as disj

-- adds the law of the excluded middle
class (HeytingAlgebra b) <= BooleanAlgebra b

This allows us to interpret the operations of Boolean algebra in a variety of settings:

• Boolean itself
• Tuples
• Power sets of Finite types
• The interval [0, 1] with min and max operations (Heyting but not Boolean)
• Three-valued logic (Heyting but not Boolean)
• In general, we can create a HeytingAlgebra from any Bounded type with an order-reversing involution.

etc.

The tricky bit is that there is obviously an interaction with the Ord hierarchy here, but I'm trying to hide it in order to get something useable without refining the hierarchy too much, hence the formulation of HeytingAlgebra in terms of implication and conjugation, instead of the underlying order.

[garyb]

I'm not crazy about the names tr and fa, fa in particular is almost certainly going to be shadowed... but then I don't have any suggestions of alternatives either really.

Is there a counterexample of why we shouldn't use Ord or Bounded as a superclass here? We could use top and bottom for tr and fa perhaps then.

[paf31]

Is there a counterexample of why we shouldn't use Ord or Bounded as a superclass here?

There's no guarantee that you have a totally-ordered lattice, in general.

[garyb]

Ah right, and I assume we don't really want to go with Poset <= Ord after all?

[paf31]

I think that's going to be tricky, since we'd have to either change the type of compare or add another function to deal with incomparable values.

I don't think we need to be that fine-grained, honestly, at least not in Prelude.

[garyb]

largest and smallest? 😉

[garyb]

👍 for the proposal in general though. The implication operator is interesting, is that something that is generally useful, or is it mainly (for us anyway) for the laws?

[paf31]

I think we need names which suggest truth and falsehood, but I can't think of good ones.

I can see implies being potentially useful in some scenarios, but it's mainly there for the laws.

Also 👍 from me on this. In particular, I think introducing HeytingAlgebra but not much extra stuff is a good balance for the prelude.

As for naming, I agree with @garyb. Some potential alternatives:

• ff, tt (these names are often used in the type theory community but may be too short)
• hbot, htop (or ibot, itop for "intuitionistic")
• falsum, verum (at least I've seen the former used for \bot before)

As far as the implication operator goes, it feels a little weird coming at this from the boolean algebra side but in intuitionistic logic it is the more primitive notion and not A is defined as A ==> fa. Obviously with some sort of operational interpretation (e.g., lambda calculus) it feels more natural.

There is another way to look at the role of implication from a categorical rather than order theoretic perspective in terms of a special kind of symmetric monoidal category called a dialogue category. See here (page 79) where ⊗ corresponds to conjunction and ⊸ to implication.

The dialogue categories Melliès describes are like *-autonomous categories where the negation is not required to be involutive up to isomorphism (i.e., from our perspective here it is not required to be boolean). See the "fourth definition" (page 81) and then the explanation (page 82) of the relationship between ⊸/ ⊥ and ¬/⊗.

A key issue which is sort of hidden here but would probably show up in some instances is the role that variance plays, i.e., categorically ⊗ is a bifunctor but ⊸ is a profunctor. The definition section of closed category has more about this.

[LiamGoodacre]

btw
a && (a ==> b) = a ==> b
is supposed to be
a && (a ==> b) = a && b

[garyb]

#64