Turn `joinLeq` and `meetLeq` into class methods

[yairchu]

In implementing a library for type inference, I stumbled upon a situation regarding type constraints.

I want to be able to:

• Accumulate (\/) constraints together
• Efficiently check if constraints were already propagated into a unification term (leq)

With the existing hierarchy, this requires to use both JoinSemilattice and PartialOrd, and to require that leq = joinLeq for all types used as type constraints..

If joinLeq was a class method of JoinSemiLattice (with its current implementation becoming the default/fallback implementation) I could had just required JoinSemilattice and not need additional requirements.

[phadej]

What about JoinSemiLattice (k -> v) or Test.QuickCheck.Property?

https://github.com/phadej/lattices/issues/54 is related issue, IIRC.

[yairchu]

So, iiuc - the problem is that JoinSemiLattice doesn't necessarily imply Eq which is another constraint for joinLeq.

Would you consider

• A ComparableJoinSemiLattice class and other Comparable classes?
• Adding an Eq constraint, which reduces possible instances (I'll admit I'm ignorant to the various use-cases of lattices therefore I don't know if this is a ridiculous suggestions)

Also are there rules regarding to which leq is the right one in case of lattice instances?

[phadej]

ComparableJoinSemiLattice would be (by default) memberless class (as JoinSemiLattice and PartialOrd) would be its superclasses. That's a (somewhat well known) problem in a class hierarchy design in Haskell:

• two classes combined is "less" than new class (i.e. additional laws, coherence conditions)
• but memberless class makes it difficult (impossible?) to write code which would infer the new "bigger" class.
• i.e. something added are additional compatibility conditions, laws.

As an example, if you write a code using leq and /\ over some l; then the inferred constraints would be (JoinSemiLattice l, PartialOrd l) => ..., not ComparableJoinSemiLattice.

So I'd rather do nothing, and not require any compatibility conditions (maybe I should advice that it's s good idea anyway) between PartialOrd and JoinSemiLattices, but be careful not to introduce non-compatibile instances in the library itself.

(Similarly, I'll really advice to make PartialOrd and Ord compatible, when possible - but as other issue https://github.com/phadej/lattices/pull/79 shows, it's not possible even in the lib itself).

---

As for your use-case, you can make

type ComparableJoinSemiLattice l = (JoinSemiLattice l, PartialOrd l )

and require your users to make instances compatible for your library to work correctly as preconditions to your library functions. (IMHO it's not muh different then requiring some things when calling lens in lens to construct well-behaved Lens).

---

Another example of this design problem is to require Default's def to be mempty when a type is both Default and Monoid - it's tricky. Or the Pointed story...

---

This issue seems be worth a blog post. I'll make a note to myself.

[yairchu]

Since there's two SemiLattice classes, with different partial orders, I think that PartialOrd shouldn't be a superclass of ComparableJoinSemiLattice. The hypothetical ComparableLattice is both a comparable join and comparable meet and the two methods joinLeq and meetLeq allow one to use both orderings. Or am I wrong because one ordering is redundant once the other exists?

[phadej]

Err.. yes. SemiLattice and MeetLattice could be different (e.g. (/\) = (\/)), but that's plain stupid. And indeed Lattice class is memberless, but it adds laws that meet and join distribute etc. So it's not consistent, that we have Lattice but not ComparableLattice; but that's a design choice which I can stand behind (more instances, Lattice is way more useful than ComparableLattice, ..., decidable equality ruling out instances).

Note that lattices as package doesn't capture all the lattice theory stuff. E.g. we cannot have BoundedMeetSemiLattice i.e. meet and top (in your case, top "no constraints"). But even your case has bottom i.e. some unsatisfiable constraint (if you consider them all "equal"). But for Haskell like language you cannot have join of constraints... TL;DR there are bounded semilattices with annihilation element, but even there are all meets and top and bottom, there aren't joins etc. All that variety is difficult to capture in Haskell type-classes.

---

I'll write the blogpost in 2019 :)

[yairchu]

I probably misunderstood something, I assumed that for sane lattices (that follow the rules and all) joinLeq and meetLeq are not equivalent. Are they interchangeable for types that support both?

[phadej]

they should give the same result, yes.

[phadej]

If i recall right

joinLeq x y = (x \/ y) == y

==> meet with x

((x \/ y) /\ x) == y /\ x

==> absorption law

x == y /\ x = meetLeq x y

[yairchu]

Alright, so I'll close the issue I guess :)

[yairchu]

Thanks for the explanations!