Skip to content

Instantly share code, notes, and snippets.

Last active Aug 29, 2015
What would you like to do?
Heyting[A] versus Bool[A]

So I promised an explanation around the changes to BooleanAlgebra[A] since 0.8.2.

The basic idea here is that we wanted to add support for lattices (and semi-lattices, and heyting algebras). These are structures which generalize boolean algebras but which are much more general. For example, the spire.math.Trilean type almost seems like it could be a boolean algebra, but it violates the law of the excluded middle.

Heyting[A] was introduced to support these types, and "algebra" was dropped from the name since it seemed redundant; Bool[A] was chosen to avoid a name conflict with Boolean[A].

In addition to their use in logic (where the operators are things like and and or) lattices are often used in other situations where their operators are defined as meet and join. Heyting algebras sort of span this gap -- it probably doesn't make sense for MeetSemilattice[A] to be defined in terms of an and method, nor does it make sense for Bool[A] to be defined in terms of meet and join.

The compromise here is that Heyting[A] defines meet and join in terms of and and or, meaning that users of Bool[A] only need to deal with the familiar methods but will still be able to use instances of Bool[A] in code that requires a lattice.

The lattice type classes and Heyting[A] were put in spire.alegbra.lattice since they are probably less commonly used than many of the other type classes. Bool[A] was left out since boolean algebras are much more familiar.

I'm happy to revisit any of these decisions before the 0.9.0 release. The current design was arrived at after informal discussion between @tixxit, myself, and others.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment