Add DistributiveLattice, update Readme

[non]

Great! Looks good to me. :+1:

I'll leave this open for a bit in case @TomasMikula or anyone else wants to comment, but it seems ready to go.

[johnynek]

Question that came up here: math.max(NaN, x) == math.min(NaN, x) == NaN, and same with java.lang.Math.min/max, which means that Order[Double] is not lawful (NaN is biggest by compare, but is the top and bottom according to min/max). So, this must mean our Order tests are not exercising min/max testing (or we aren't running them for double. Sorry I didn't check that yet).

Not sure what we should do here. NaN being bigger than PositiveInfinity is a bit weird. But being more precise and using PartialOrder here may be overkill. On the other hand, a PartialOrder is exactly what we have here.

There could be unsafeToOrder on PartialOrder that throws an exception when we get NaN, which might be useful in cases where we expect to use a subset of the inputs that will always compare well. Or we could fix the Order to make min(x, NaN) == x, which seems a bit dangerous. Or we could just say that basically everything on Float/Double is not lawful (which is kind of what we do now).

[johnynek]

Also, each Lattice has a dual, right? But for some reason we only have this notion on Bool. So, Lattice dual could return a Lattice. I think Heyting doesn't always have a dual which is a Heyting (some seem to, maybe all and I misunderstood). If they did then we could have a f-bound on Lattice and then dual returns the self-type there. Alternatively, we could override in each subclass the subclass of Lattice that dual returns.

[non]

@johnynek The situation with Double gets worse:

java.lang.Double.compare(3.0, Double.NaN) // -1
java.lang.Double.min(3.0, Double.NaN) // NaN

So NaN is greater than 3.0 (according to .compare) but less according to .min.

I think the way forward is to say:

• Order[Double] is not lawful.
• Order[Double] (excluding NaN) is lawful.
• Folks who need specific semantics (i.e. a total order including NaN) must define their own.

Our guiding principle in Spire is to preserve the direct semantics for Double. In other words, we wire compare, less-than, min, max, etc. up to the relevant direct methods. I don't see another approach that won't increase the already signficant inconsistencies between IEEE-754 and the JVM.

[non]

My vote would be to add .dual to Lattice and to refine the return value in its various subtypes. This is a bit ugly but will keep things simple for users and has less chance of going wrong than exposing F-bounded polymorphism.

[TomasMikula]

The dual of Heyting is not Heyting in general. A counterexample that you cannot just swap ∧ and ∨ is that a ∨ ¬a = 1, which is not generally true for Heyting, would be a ∧ ¬a = 0 in the dual, which is true for every Heyting. That means we just turned a false statement into a true statement, thus a contradiction.

Wikipedia says that the dual of Heyting is sometimes called a Brouwer lattice:

Heyting algebras are less often called pseudo-Boolean algebras, or even Brouwer lattices,[2] although the latter term may denote the dual definition,[3] or have a slightly more general meaning.

[TomasMikula]

As far as I'm concerned, this looks good to go.

[non]

Excellent. :+1: