Reintroduce Join/MeetSemiLattice

[dbeacham]

Why were Join/MeetSemiLattice dropped from the API?

I have some algebras that can only implement meet (or join) but do not have the other, e.g. they form a partial ordering but can only define lub or glb.

It's a bit of a shame to have the missing step from partial ord to lattice.

[phadej]

I'd recommend to use https://hackage.haskell.org/package/semilattices if you need that.

I have to write down my reasoning though for an API change

[dbeacham]

It'd be good to see the reasoning.

Having to use a separate package is a bit annoying as I have code that works over some types that are lattices and some that are just semi lattices and I'd like to have them use the same operator rather than switching between differently qualified /\ and \/.

[sgraf812]

Also there is no PartialOrd in semilattices. In general, its API seems inferior.

I have a pomaps package that depends on PartialOrd and datafix which strengthens these requirements to BoundedJoinSemiLattice in a few places, and of course there are BJSLs in practice that just aren't bounded lattices. I'd just use v1.7 forever, but that won't work without --allow-newer anymore with GHC 8.8.1.

Would you consider also maintaining v1.*, if only for bumping upper bounds?

[phadej]

@sgraf812 I did revision for 1.7.1.1 https://hackage.haskell.org/package/lattices-1.7.1.1/revisions/ (looks like GHC-8.10 is fine too). I'll do revision for 2.x versions when I do bigger larger scan of libraries I maintain (after GHC-8.10 is released).

About BoundedJoinSemiLattice. I don't think I'll add it back. For the datafix case you are actually interested in CPOs, not lattices. I'm thinking that class PartialOrd a => CPO a where ??? would be reasonable to have, and maybe make lfpFrom to use that class (as that what the fixpoint theorem requires).

In short Lattice and PartialOrd are unrelated as far as type-checker is concerned, for reasons like (#54), so I might need to "duplicate" classes.

Yet, I'm not sure how CPO class should look like. Its math definition says that big \/ exists in directed subset (or there is least upper element in ascending chain), which is not arbitrary subset (i.e. not [a]). Thus e.g. binary strings ordered by isPrefixOf are CPO (but they are not lattice). I'm trying to wrap my head around it, and come up with something satisfactory, yet not oversimplifying too much.

I even borrowed a book to wrap my head around these issues properly
yet I have been lazy studying it.

[sgraf812]

Yes, BoundedJoinSemiLattice is just an approximation to a CPO, but a very close one. Close enough for the program analyses I had in mind, at least.

Also, being able to compute the join of two incomparable elements is quite useful at times. In terms of a monotone function f as in datafix this means that we can start fixed-point iteration when computing f c, where c is an upper bound to both a and b (so c >= a \/ b), from f a \/ f b (which is lower bound to f (a \/ b), which is lower bound to f c). In a CPO, you would have to start from ⊥.

TLDR; I like BoundedJoinSemiLattice for datafix, and redefining it probably wouldn't be that hard. It's just that I like to build on a separate library that defines this language rather than embedding it into a library with a very narrow use case.

Edit: Reading https://en.wikipedia.org/wiki/Complete_partial_order it seems I had the definition of a chain-complete partial order in mind when writing this. I find that wikipedia page quite confusing everytime I hit it. Anyway, thanks for the version bump!

[phadej]

Another solution for datafix, which you probably won't like. Is to use Monoid instead of BoundedSemiJoinLattice. You'd need to have a disclaimer that only commutative and idempotent monoids work; yet there are no connection between PartialOrd and BoundedSemiJoinLattice (though this library has the same underlying order). I'm not sure whether user have to write some monotonic function for things to work, but that's not enforced by type-system either.

I tried, and needed to do just two changes in the library (examples define instances, so there is more work). joins to mconcat was the other one.

[sgraf812]

Thanks for the suggestion! I'd probably define a IdempotentCommutativeMonoid class for that. And then I can just define BoundedSemiJoinLattice directly, to get the connection with PartialOrd.

Anyway, the current state of things works for me, so no need to change it just yet :)

I'm a little worried about potential users (well, in case there will ever be any user of datafix other than myself) in the future that like to use some new lattices v2 feature that conflicts with my <2 upper bound.

[dbeacham]

I can also use lattices-1.7.1 (thanks for providing that) and heyting-algebras-0.2.0.0 but it's not ideal as we'll definitely be missing future updates/additions. Using 2.0 introduces partial functions as I can't define (\/) on all of my lattice types.

I still don't understand the need or benefit to combining join/meet lattices while you keep a separation of bounded meet and join lattices. They're two perfectly lawful parts of the hierarchy.

[phadej]

If you want separate type hierarchy, use https://hackage.haskell.org/package/semilattices.

We (lattices and semilattices) explore the design space of "how to encode mathematical structures in Haskell", and chose different ways.

I wont reintroduce Join/MeetSemiLattice class(es).

[kindaro]

@phadej  Please help me understand why semi-lattices have been removed. Who benefits from having separate packages for lattices and semi-lattices, with separate class hierarchies and subtly distinct interfaces? Surely if a type is a lattice, it is automatically both a join and a meet semilattice. Can there ever be a technical reason for breaking things apart like this?

[sgraf812]

Note that I accepted in #95 (comment) that I just have to define my own type class. I can't switch to https://hackage.haskell.org/package/semilattices, because it has no analog of PartialOrd. So there are use cases in which you can't replace lattices-1.* by lattices-2.* or semilattices.

[davean]

I to would be interested in the reasoning for this change. I can't see the reason for this reordering of the type classes (and it breaks my usages of this package).

Above you said you needed to write up the logic, I can't find it yet though. Would you mind explaining please?

[phadej]

I don't like when there are laws assigned to

• memberless type-classes (or synonyms)
• laws refer to members of type-classes which are not super-classes

class Pointed f where
  pure :: a - f a

class Ap f where
  (<*>) :: f (a -> b) -> f a -> f b

type Applicative f = (Functor f, Pointed f, Ap f)

That's however how hierarchy is modelled in semilattices, and you are free to use it if you like.

Current (lattices-2) design is such that:

• there is no memberless type-classes (with extra laws). Note BoundedLattice doesn't add any laws.
• there is no laws referencing members not in class itself or its superclasses.
  /\ and \/ are introduced in the same class Lattice, so their interaction, e.g. absorption is a natural looking class.

I'm aware that new hierachy might not fit all the previous use-cases,
trade-offs have to be made. I made this one.

[sgraf812]

You're of course free to refactor your library as you please, but

I don't like when there are laws assigned to

• memberless type-classes (or synonyms)

I understand the issue about synonyms, but not so much about type classes. What's wrong with a memberless sub class? If Haskell actually had theorem proving capabilities, the proof for the law would surely be part of the type class, so the type class wouldn't even be empty anymore. Declaring the instance in Haskell basically declares a "trust me" proof.

I'm not a huge fan if the instance for a memberless sub class is directly implied, though, because that makes it effectively a synonym.

Maybe I'm misunderstanding, but the example you gave is just one for the synonym issue, not for the memberless type class issue.

[phadej]

However, Haskell does not have theorem proving capabilities. In Agda lattices look different, and that is fine.

And even if Haskell had:

class (Functor f, Pointed f, Ap f) => Applicative f where
   ...four law members..

then what would be the inferred type of:

liftA2 f x y = f <$> x <*> y

It won't be Applicative f =>.

In theorem provers, types are rarely inferred. In Haskell they are, because it's not a theorem prover and laws are not used formally (so we won't overconstraint the type if we don't need to).

[sgraf812]

Inference is a convincing example. Thanks!

[emilypi]

Note BoundedLattice doesn't add any laws.

But Lattice does - it has absorption laws which are codified into the typeclass. One can have a type which has both a Join and Meet semilattice instance which does not have a Lattice instance because absorption fails. In this case, a memberless typeclass gives an indicator towards the reasoning principles you can use for join and meet, which is not implied if you just have (Join a, Meet a) => ! The latter introduces ambiguity at the cost of source code cleanliness, and the former introduces improved reasoning at the cost of a typeclass. I'm inclined to believe that the typeclass is the lesser of the two evils here.

One of the other knock-on effects this has is that, while the "more principled class is the superclass" approach may work in some cases like Monoid a => Semigroup a, it doesn't in the case of Lattices. You can view a semigroup as a degenerate Monoid, vis. Semicategory as a deficient category, depending on your worldview, but a Lattice is more akin to a Ring, which is a composite structure built from more principled components: namely, join/meet-semilattices and their bounded variants. So to me and to others, that direction for implication is actually surprising and in the case of the first point, wrong in some cases.

I'm not going to say "change it back", because obviously competition is great, but it's something to think about.

[davean]

That is the problem I'm running into, this arrangement seems to contradict the theory behind lattices.

[dbeacham]

One can have a type which has both a Join and Meet semilattice instance which does not have a Lattice instance because absorption fails

But in this case the join and meet instances can't be with respect to the same partial order?

But I might be misunderstanding and you're making exactly this point!

I think I'd expect

class (JoinSemiLattice a, MeetSemiLattice a) => Lattice a
instance (JoinSemiLattice a, MeetSemiLattice a) => Lattice a

?

Not arguing for a change just trying to understand what other interfaces could make sense.

[davean]

Not every (JoinSemiLattice a, MeetSemiLattice a) => a is Lattice a, correct. Lattice a comes with extra requirements. If you need those theorems you need to take Lattice.

[dbeacham]

Yes - but that is only in the case when the induced partial orders are different? - which I'd argue makes for poor instances.

I think that would be fixed by making PartialOrd be a superclass of JoinSemiLattice and MeetSemiLattice?

[phadej]

Yes - but that is only in the case when the induced partial orders are different? - which I'd argue makes for poor instances.

I think that would be fixed by making PartialOrd be a superclass of JoinSemiLattice and MeetSemiLattice?

#54

[dbeacham]

Sorry @phadej - I'd seen this and it wasn't a request to make any changes. Just trying to clear up the discussion I'd been having above.

I do feel that breaking the hierarchy apart to admit the JoinSemiLattice v => JoinSemiLattice (k -> v) is a bit of a misstep. It feels coincidental that the (->) join- and meet-semilattices are pointwise compared to domain-wise for equality, ordering etc. and so living without them as we do for Eq, Ord etc doesn't feel that problematic. There may of course be other instances I'm not aware of that don't admit PartialOrd instances but they must similarly fail to supply Eq instances otherwise you could define the PartialOrd via

(<=?) x y | x /\ y == x = True
          | otherwise = False

That said - thanks for creating/maintaining the library! I understand how much time it can take and underappreciated it can be.

[emilypi]

Yes - but that is only in the case when the induced partial orders are different? - which I'd argue makes for poor instances.

I think that would be fixed by making PartialOrd be a superclass of JoinSemiLattice and MeetSemiLattice?

Yes, precisely. This problem comes from the fact that the purely algebraic take (lattices are composed of a pair of commutative, idempotent monoids that agree as a duoid) and the order-theoretic take (lattices are posets with all finite joins/meets) make slightly different assumptions at different points. In the former case, you need the typeclass due to the pair (Join a, Meet a) having possibly conflicting operations (they don't form a duoid/fail absorption), where the instances can concretize those absorption laws. The latter case works only if you accept partial ord as your superclass. That's the tradeoff. I still think having the typeclass in either case helps with reasoning because I don't want to keep that all in my head implicitly. And i would still say that lattices should not superclass their component algebras!

[phadej]

I do feel that breaking the hierarchy apart to admit the JoinSemiLattice v => JoinSemiLattice (k -> v) is a bit of a misstep.

(predicate1 /\ predicate2) \/ anotherPredicate is however very neat and practical.

[dbeacham]

Ah yes - that is very nice and something I hadn't considered.

You can - albeit with an extra couple of operators - recover that behaviour (and more?) with

(</\>) :: Applicative f => MeetSemiLattice a => f a -> f a -> f a
(</\>) = liftA2 (/\)

but I guess that's just one of the trade-offs.