valuations-0.0.3: src/Data/Valuation/DomainLattice.hs

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# OPTIONS_GHC -Wall -Werror #-}

-- | A lattice structure on domains, as required by the presheaf formulation
-- of valuation algebras (Shenoy & Shafer, Kohlas, Abramsky & Carù).
--
-- A domain lattice provides:
--
-- * Join (\/) — combining domains (supremum)
-- * Meet (/\) — intersecting domains (infimum)
-- * Partial order — domain inclusion, with incomparable elements
module Data.Valuation.DomainLattice
  ( DomainLattice (..),
    DomainLattice',
    HasDomainLattice (..),
    AsDomainLattice (..),
    runDomainJoin,
    runDomainMeet,
    runDomainCompare,
    runDomainLeq,
    setDomainLattice,

    -- * laws
    lawJoinAssociative,
    lawMeetAssociative,
    lawJoinCommutative,
    lawMeetCommutative,
    lawAbsorption1,
    lawAbsorption2,
    lawJoinIdempotent,
    lawMeetIdempotent,
    lawLeqFromJoin,
  )
where

import Control.Lens (Lens', Prism', review, view)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Valuation.PartialOrder
  ( HasPartialOrder (..),
    PartialOrder,
    fromLeq,
    partialOrderLeq,
    runPartialOrder,
  )
import Data.Valuation.Semigroup
  ( Semigroup,
    applySemigroup,
    runSemigroup,
  )
import Prelude hiding (Semigroup)

-- $setup
-- >>> :set -Wno-name-shadowing -Wno-type-defaults

-- |
-- >>> import qualified Data.Set as Set
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)
-- >>> runDomainJoin lat (Set.fromList [1,2]) (Set.fromList [2,3])
-- fromList [1,2,3]
-- >>> runDomainMeet lat (Set.fromList [1,2]) (Set.fromList [2,3])
-- fromList [2]
-- >>> runDomainLeq lat (Set.fromList [1]) (Set.fromList [1,2])
-- True
-- >>> runDomainLeq lat (Set.fromList [1,3]) (Set.fromList [1,2])
-- False
-- >>> runDomainCompare lat (Set.fromList [1,2]) (Set.fromList [2,3])
-- Nothing
data DomainLattice p sg o
  = DomainLattice
      -- | join (\/ / supremum)
      (Semigroup p sg)
      -- | meet (/\ / infimum)
      (Semigroup p sg)
      -- | partial order
      (PartialOrder o)

type DomainLattice' x =
  DomainLattice (->) x x

-- | Classy lens for types that contain a 'DomainLattice'.
class HasDomainLattice c p sg o | c -> p sg o where
  domainLattice :: Lens' c (DomainLattice p sg o)
  domainLatticeJoin :: Lens' c (Semigroup p sg)
  domainLatticeJoin = domainLattice . domainLatticeJoin
  domainLatticeMeet :: Lens' c (Semigroup p sg)
  domainLatticeMeet = domainLattice . domainLatticeMeet

instance HasDomainLattice (DomainLattice p sg o) p sg o where
  domainLattice = id
  domainLatticeJoin f (DomainLattice j m o) = fmap (\j' -> DomainLattice j' m o) (f j)
  domainLatticeMeet f (DomainLattice j m o) = fmap (\m' -> DomainLattice j m' o) (f m)

-- | Classy prism for types that can be constructed from a 'DomainLattice'.
class AsDomainLattice c p sg o | c -> p sg o where
  _DomainLattice :: Prism' c (DomainLattice p sg o)

instance AsDomainLattice (DomainLattice p sg o) p sg o where
  _DomainLattice = id

instance HasPartialOrder (DomainLattice p sg o) o where
  partialOrder f (DomainLattice j m o) = fmap (DomainLattice j m) (f o)

-- | Apply the domain join (\/): the supremum of two domains.
{-# SPECIALIZE runDomainJoin ::
  DomainLattice (->) sg o -> sg -> sg -> sg
  #-}
runDomainJoin :: (HasDomainLattice lat (->) sg o) => lat -> sg -> sg -> sg
runDomainJoin = runSemigroup . view domainLatticeJoin

-- | Apply the domain meet (/\): the infimum of two domains.
{-# SPECIALIZE runDomainMeet ::
  DomainLattice (->) sg o -> sg -> sg -> sg
  #-}
runDomainMeet :: (HasDomainLattice lat (->) sg o) => lat -> sg -> sg -> sg
runDomainMeet = runSemigroup . view domainLatticeMeet

-- | Compare two domains using the partial order.
-- Returns 'Nothing' for incomparable elements.
--
-- >>> import qualified Data.Set as Set
-- >>> runDomainCompare (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1]) (Set.fromList [1,2])
-- Just LT
-- >>> runDomainCompare (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [1,2])
-- Just EQ
-- >>> runDomainCompare (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3])
-- Nothing
{-# SPECIALIZE runDomainCompare ::
  DomainLattice p sg o -> o -> o -> Maybe Ordering
  #-}
runDomainCompare :: (HasPartialOrder lat p) => lat -> p -> p -> Maybe Ordering
runDomainCompare = runPartialOrder . view partialOrder

-- | Test the domain partial order: @runDomainLeq lat d1 d2@ is 'True' iff @d1 <= d2@.
-- Returns 'False' for incomparable elements.
--
-- >>> import qualified Data.Set as Set
-- >>> runDomainLeq (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1]) (Set.fromList [1,2])
-- True
-- >>> runDomainLeq (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3])
-- False
{-# SPECIALIZE runDomainLeq ::
  DomainLattice p sg o -> o -> o -> Bool
  #-}
runDomainLeq :: (HasPartialOrder lat p) => lat -> p -> p -> Bool
runDomainLeq = partialOrderLeq . view partialOrder

-- | The canonical 'DomainLattice' for 'Set', with union as join,
-- intersection as meet, and subset as the partial order.
--
-- >>> import qualified Data.Set as Set
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set String) (Set String)
-- >>> runDomainJoin lat (Set.fromList ["x","y"]) (Set.fromList ["y","z"])
-- fromList ["x","y","z"]
-- >>> runDomainMeet lat (Set.fromList ["x","y"]) (Set.fromList ["y","z"])
-- fromList ["y"]
-- >>> runDomainLeq lat (Set.fromList ["x"]) (Set.fromList ["x","y"])
-- True
-- >>> runDomainCompare lat (Set.fromList ["x","y"]) (Set.fromList ["y","z"])
-- Nothing
setDomainLattice :: (Ord a) => DomainLattice' (Set a)
setDomainLattice =
  DomainLattice
    (review applySemigroup Set.union)
    (review applySemigroup Set.intersection)
    (fromLeq Set.isSubsetOf)

-- |
-- >>> import qualified Data.Set as Set
-- >>> lawJoinAssociative (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3]) (Set.fromList [3,4])
-- True
lawJoinAssociative :: (Eq sg) => DomainLattice (->) sg o -> sg -> sg -> sg -> Bool
lawJoinAssociative lat a b c =
  let j = runDomainJoin lat
   in j (j a b) c == j a (j b c)

-- |
-- >>> import qualified Data.Set as Set
-- >>> lawMeetAssociative (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3]) (Set.fromList [3,4])
-- True
lawMeetAssociative :: (Eq sg) => DomainLattice (->) sg o -> sg -> sg -> sg -> Bool
lawMeetAssociative lat a b c =
  let m = runDomainMeet lat
   in m (m a b) c == m a (m b c)

-- |
-- >>> import qualified Data.Set as Set
-- >>> lawJoinCommutative (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3])
-- True
lawJoinCommutative :: (Eq sg) => DomainLattice (->) sg o -> sg -> sg -> Bool
lawJoinCommutative lat a b =
  runDomainJoin lat a b == runDomainJoin lat b a

-- |
-- >>> import qualified Data.Set as Set
-- >>> lawMeetCommutative (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3])
-- True
lawMeetCommutative :: (Eq sg) => DomainLattice (->) sg o -> sg -> sg -> Bool
lawMeetCommutative lat a b =
  runDomainMeet lat a b == runDomainMeet lat b a

-- | Absorption law 1: @a \/ (a /\ b) = a@.
--
-- >>> import qualified Data.Set as Set
-- >>> lawAbsorption1 (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3])
-- True
lawAbsorption1 :: (Eq sg) => DomainLattice (->) sg o -> sg -> sg -> Bool
lawAbsorption1 lat a b =
  runDomainJoin lat a (runDomainMeet lat a b) == a

-- | Absorption law 2: @a /\ (a \/ b) = a@.
--
-- >>> import qualified Data.Set as Set
-- >>> lawAbsorption2 (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3])
-- True
lawAbsorption2 :: (Eq sg) => DomainLattice (->) sg o -> sg -> sg -> Bool
lawAbsorption2 lat a b =
  runDomainMeet lat a (runDomainJoin lat a b) == a

-- | Join idempotence: @a \/ a = a@.
--
-- >>> import qualified Data.Set as Set
-- >>> lawJoinIdempotent (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2])
-- True
lawJoinIdempotent :: (Eq sg) => DomainLattice (->) sg o -> sg -> Bool
lawJoinIdempotent lat a =
  runDomainJoin lat a a == a

-- | Meet idempotence: @a /\ a = a@.
--
-- >>> import qualified Data.Set as Set
-- >>> lawMeetIdempotent (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,2])
-- True
lawMeetIdempotent :: (Eq sg) => DomainLattice (->) sg o -> sg -> Bool
lawMeetIdempotent lat a =
  runDomainMeet lat a a == a

-- | Consistency of partial order with join: @a <= b@ iff @a \/ b = b@.
--
-- >>> import qualified Data.Set as Set
-- >>> lawLeqFromJoin (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1]) (Set.fromList [1,2])
-- True
-- >>> lawLeqFromJoin (setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)) (Set.fromList [1,3]) (Set.fromList [1,2])
-- True
lawLeqFromJoin :: (Eq d) => DomainLattice' d -> d -> d -> Bool
lawLeqFromJoin lat a b =
  runDomainLeq lat a b == (runDomainJoin lat a b == b)