haskellari / lattices

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

instance PartialOrd (M.Map k v) #33

Closed mhecker closed 7 years ago

mhecker commented 8 years ago

I am confused about the PartialOrd instance of Map:

instance (Ord k, PartialOrd v) => PartialOrd (M.Map k v) where
  m1 `leq` m2 = m1 `M.isSubmapOf` m2 && M.fold (\(x1, x2) b -> b && x1 `leq` x2) True (M.intersectionWith (,) m1 m2)

This results in:

> Data.Map.fromList [ (0, Data.Set.fromList [0]) ] `leq`
  Data.Map.fromList [ (0, Data.Set.fromList [0,1]) ]
False 

Compare this with the JoinSemiLattice instance of Map , which gives:

> Data.Map.fromList [ (0, Data.Set.fromList [0]) ] `joinLeq` 
  Data.Map.fromList [ (0, Data.Set.fromList [0,1]) ]
True

The documentation of isSubmapOf says:

This function is defined as (isSubmapOf = isSubmapOfBy (==)). and The expression (isSubmapOfBy f t1 t2) returns True if all keys in t1 are in tree t2, and when f returns True when applied to their respective values.

so use of isSubmapOf is strange to me, anyway, since then the test && M.fold (\(x1, x2) b -> b && x1leqx2) True (M.intersectionWith (,) m1 m2) appears to be redundant.