haskellari / lattices

Fine-grained lattice primitives for Haskell
BSD 3-Clause "New" or "Revised" License
35 stars 15 forks source link

Set union not necessarily commutative #84

Open rightfold opened 5 years ago

rightfold commented 5 years ago

JoinSemiLattice requires that join is commutative, but this is not necessarily true for the instance JoinSemiLattice (Set a) where join = union.

Consider this valid total order:

data X = X Int String
instance Eq X where (X a _) (X b _) = a == b
instance Ord X where (X a _) (X b _) = a `compare` b

Now with:

a = fromList [X 1 "A"]
b = fromList [X 1 "B"]

The following do not give the same result:

union a b
union b a
phadej commented 5 years ago
λ Data.Set> data X = X Int String deriving (Show)
λ Data.Set> instance Eq X where (X a _) == (X b _) = a == b
λ Data.Set> instance Ord X where compare (X a _) (X b _) = a `compare` b
λ Data.Set> a = fromList [X 1 "A"]
λ Data.Set> b = fromList [X 1 "B"]
λ Data.Set> union a b
fromList [X 1 "A"]
λ Data.Set> union b a
fromList [X 1 "B"]
λ Data.Set> union a b == union b a
True

I don't see a problem. Your Eq / Ord says they are EQual.

rightfold commented 5 years ago

They are equivalent according to the equivalence relation Eq (Set X), but they are not the same value. One is fromList [X 1 "A"] whereas the other one is fromList [X 1 "B"].

If you want the semilattice laws to hold with respect to Eq, rather than extensional equality, how would you describe them for the instance JoinSemiLattice (a -> b)?