Skip to content

Instantly share code, notes, and snippets.

@non
Last active August 29, 2015 14:08
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save non/f458b74533e1506e2736 to your computer and use it in GitHub Desktop.
Save non/f458b74533e1506e2736 to your computer and use it in GitHub Desktop.
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