Split out ComplementedLattice from Heyting typeclass?

[benhutchison]

(Ok I'm being slightly tongue in cheek, but..) IMO it's an unfortunate accident of history that the lattice algebra hierarchy ended up in a ecosystem-anchor library like Cats.

On one hand, it begs to become the butt of jokes. A workmate used to ask if anyone had "designed any lattices lately?".

OTOH it means that evolving the lattice typeclasses becomes a more heavyweight change than in Spire or another more obscure location.

The Heyting typeclass introduced two new, independent abstract methods, complement and imp (implication).

https://github.com/typelevel/cats/blob/main/algebra-core/src/main/scala/algebra/lattice/Heyting.scala#L64-L65

Introducing two distinct abstract operations in a single TC may be a design smell. Is there a weaker form with just one?

Yes, an algebra that has just complement without imp is called a Complemented Lattice.

Why does it matter? Well, a datatype for proper fraction, a value between [0, 1], could implement ComplementedLattice and complement is useful. But I can't see a sensible implementation for imp that would get used; that operator seems to belong in discrete logics.