haskellari / lattices

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

Interface provided by `PartialOrd` isn't practical/efficient #117

Open andreasabel opened 2 years ago

andreasabel commented 2 years ago

The interface for PartialOrd a has two methods:

  comparable :: a -> a -> Bool
  leq :: a -> a -> Bool

https://hackage.haskell.org/package/lattices-2.0.3/docs/Algebra-PartialOrd.html#t:PartialOrd

I think an interface as chosen in package partial-order allows for more efficient implementations:

  compare :: a -> a -> Maybe Ordering

https://hackage.haskell.org/package/partial-order-0.2.0.0/docs/Data-PartialOrd.html#v:compare

From the latter, we easily define:

   comparable a b = isJust (compare a b)
   leq a b = case compare a b of { Just LT -> True; Just EQ -> True; _ -> False }

However, defining compare involves two calls to the interface:

   compare a b =
     case (leq a b, leq b a) of 
          (True, True) -> Just EQ
          (True, False) -> Just LT
          (False, True) -> Just GT
          (False, False) -> Nothing

This may be problematic if there is common work to be done for leq a b and leq b a. The pure interface does not allow sharing of this joint work.

For example, consider sets implemented by sorted lists. A call to leq a b = isPrefixOf a b would have worst-time complexity O(min(n,m)); but compare would just run in the same time. So, the interface with just leq gives a slow-down of factor 2 in the worst case.

phadej commented 2 years ago

compare is a bad name as it clashes with Ord definition. I agree, it would be good to add such method to PartialOrd.

Can we have efficient implementations for Set and Maps?

andreasabel commented 2 years ago

compare is a bad name as it clashes with Ord definition. I agree, it would be good to add such method to PartialOrd.

compareMaybe would be a canonical name.

Can we have efficient implementations for Set and Maps?

I suppose symmetric difference would be the canonical avenue for Set. However, it hasn't materialized yet:

Maybe a stand-in via Set.toAscList wouldn't be too awful.

Also one can lift compareMaybe from v to k -> v for a finite k using minimum on the four point lattice (Hasse diagram):

              Just EQ
Just LT                     Just GT
              Nothing

This gives a general recipe for products of all kinds.