Intervals form a semilattice with respect to `isSuperintervalOf` — add an instance to show this?

[kindaro]

Namely, given two intervals, we can construct an interval that has all the lowest coördinates as its infimum and all the highest as its supremum. This operation is called «convex hull» elsewhere. The type of coördinates should itself be a lattice for this to work. If, further, the type of coördinates has bounds, then the type of intervals has an upper bound — the whole space. An example would be something like a vector space over the extended real number system — a formal completion of floating point numbers with positive and negative infinities.

With the above in mind, we may concisely characterize intervals as a profunctor in the category of partial orders.

[robrix]

If I’m not mistaken, that’s currently expressed via our Union semigroup, tho using Ord on coordinates instead of a lattice. What sort of instance(s) do you propose adding?

a profunctor in the category of partial orders

Interesting!

[kindaro]

@robrix  There are a few things to say.

• I was remembering that lattices have type classes for both semi-lattices and lattices, but turns out it is not the case since version 2. Possibly we can depend on the version 1.7 and keep it on life support.

  Then there is your own package semilattices, but, as far as I see, it does not define a notion of a lattice where join and meet are required to be compatible, which is what we need our coördinates to satisfy in order for the induced ordering on intervals to work. So possibly we can add some features to semilattices.

• I find it that Ord and Semigroup do not express the connexion I propose we have here as clearly and precisely as Lattice and Semilattice would.

  • In the current setting we have no way to define the «universe» — the upper bound, largest possible interval, formed coördinate-wise by the lower and the upper bounds of the underlying bounded lattice. There is no lower bound for intervals with respect to inclusion, so Bounded is not suitable.
  • The order of intervals under inclusion is not compatible with the usual ordering by the «rightness» of the constituent coördinates. The order of inclusion is not even total, so the Ord instance would not fit anyway.

To be honest, the situation with lattice libraries is worse than I thought and now I suppose my proposal has to be shelved until a more featureful lattice library appears.

[robrix]

Then there is your own package semilattices, but, as far as I see, it does not define a notion of a lattice where join and meet are required to be compatible, which is what we need our coördinates to satisfy in order for the induced ordering on intervals to work. So possibly we can add some features to semilattices.

I handle that case, when it arises, by adding Join and Meet constraints and documenting that they are required to be compatible. That is, I don’t think we would necessarily need to extend semilattices for this, tho clearly it’s possible.

• I find it that Ord and Semigroup do not express the connexion I propose we have here as clearly and precisely as Lattice and Semilattice would.

  • In the current setting we have no way to define the «universe» — the upper bound, largest possible interval, formed coördinate-wise by the lower and the upper bounds of the underlying bounded lattice. There is no lower bound for intervals with respect to inclusion, so Bounded is not suitable.
  • The order of intervals under inclusion is not compatible with the usual ordering by the «rightness» of the constituent coördinates. The order of inclusion is not even total, so the Ord instance would not fit anyway.

I accept both of these points, but I don’t follow what they mean for the usage of the library. In what way do we calculate the wrong results for what you have in mind? What do the results you want look like instead?