Top of finite join-semilattice

[cartazio]

One way or another, a project of mine at work using lattice / partial ordered structures in a pretty fundamental way, and before i commit to having my own mini lattices in tree, I figured i'd ask what roadmap you have in mind for this code base and/or how might I be able to help out?

cheers!

[phadej]

@cartazio Currently the lattices api is quite stable, and I don't have any major development plans, other than adding more instances.

I'm open to ideas though.

One idea of mine is to figure out on how to develop boolean-normal-forms (github) further. There are free-ish structures (tree with meet and join nodes, dnf and cnf like representations), which might be useful. If it's something you need, just say. I'd probably make a lattices-extras package for that though, as then I can e.g. depend on recursion-schemes.

[cartazio]

Cool! I'll have to mull those. One question that came up at work yesterday is whether or not the constraint structure for when top and bottom are defined actually make sense.

Design question about the current type classes , which I should move its own ticket perhaps :) At work we have a join semi lattice where then elements of the partial order correspond to {1}, {2}, and {1,2},

This means top is definable, but bottom and or meet are not , for this particular partial order. Thus the formulation of the bounded semi lattice classes precludes defining the top type class im stance for this lattice using thst class. Because at least for now we don't want to consider the completion that includes the empty set

On Tuesday, February 23, 2016, Oleg Grenrus notifications@github.com wrote:

@cartazio https://github.com/cartazio Currently the lattices api is quite stable, and I don't have any major development plans, other than adding more instances.

I'm open to ideas though.

One idea of mine is to figure out on how to develop boolean-normal-forms http://hackage.haskell.org/package/boolean-normal-forms (github) https://github.com/phadej/boolean-normal-forms further. There are free-ish structures (tree with meet and join nodes, dnf and cnf like representations), which might be useful. If it's something you need, just say. I'd probably make a lattices-extras package for that though, as then I can e.g. depend on recursion-schemes.

— Reply to this email directly or view it on GitHub https://github.com/phadej/lattices/issues/27#issuecomment-187577637.

[phadej]

Let me see, you have

data T = T1 | T2 | T12
    deriving (Eq)

instance JoinSemiLattice T where
    T1  \/ T1   = T1
    T1  \/ T2   = T12
    T1  \/ T12  = T12
    T2  \/ T1   = T12
    T2  \/ T2   = T2
    T2  \/ T12  = T12
    T12 \/ T1   = T12
    T12 \/ T2   = T12
    T12 \/ T12  = T12

instance PartialOrd T where
    leq = joinLeq

I see, there is natural top = T12 element, because

forall x. top \/ x = top
forall x. x \/ top = top

But we cannot define top because of class MeetSemiLattice a => BoundedMeetSemiLattice a constraint.

It's some time since my algebra classes, but there could be

class JoinSemiLattice l => FiniteJoinSemiLattice l where
    finiteTop :: l
    default finiteTop :: Finite l => l
    finiteTop = joins universeF

Yet would it be enough to have finiteTop (and correspondingly finiteBottom) for your application?

[cartazio]

I think this would work for us, though as the application evolves my understanding may change :)

[cartazio]

(though of course i'm not sure if this need be done unless its something that actually improves abstrations generally :) )

[phadej]

I'll leave this open. I'm not 100% sure, whether having the FiniteJoinSemiLattice class would be useful. Having finiteTop in a class is justified, as it can be "precomputed" (e.g. for very large, though still finite semilattices); OTOH when you have only join operation, you have only finiteTop \/ x = finiteTop law, which doesn't really give you anything interesting to work with?

I might be wrong though, if you have some interesting application, I'll reconsider this again.

[phadej]

I decided to remove MeetSemiLattice and JoinSemiLattice classes. So this issue is non applicable anymore.