induced JoinSemiLattice from PartialOrd

[carlostome]

Hi, I'm interesed in lattices induced by a partial order relation and some extra element that serves as top

We could implement such using the already existing datatype Algebra.Lattice.Dropped but it already has instances for JoinSemiLattice, BoundedSemiLattice ... that would overlap.

I propose to augment the library with something like the following:

module Algebra.PartialOrd.Drop where

import Algebra.Lattice
import Algebra.PartialOrd

data Drop a = Topped
            | Dropped a

instance PartialOrd a => JoinSemiLattice (Drop a) where
  Topped    \/ _      = Topped
  _      \/ Topped    = Topped
  Dropped x \/ Dropped y
    | leq x y   = Dropped y
    | leq y x   = Dropped x
    | otherwise = Topped

instance BoundedJoinSemiLattice (Drop a) where
   top = Topped

Of course this can be generalized for Lifted, Levitated and maybe something else.

[phadej]

Is this correct? Take sets with union as a join, subset as partord. {1, 2} and {2,3} aren't in relation, yet their union is {1, 2, 3}; not a "all numbers".

[carlostome]

My use case was to have Int + Top so the partial order between Int is just equality and Top serves to make a JoinSemiLattice out of it.

In the case of sets I would think of Top as the join of any two sets that are not related but not as the "all numbers" set.

[phadej]

I'm unease to add that to the library. Your use case has quite strong condition of

not (a ≤ b) and not (b ≤ a) imply (a ∨ b) = ⊤.

I'd rather implement instance Eq a => JoinSemiLattice (Something a) in your executable/library, as I'm not sure it has an established name or/and is generally useful.

[carlostome]

Ok, then I'll close the issue, thanks for answering so quickly.

[phadej]

sorry for unable to help more.