module FP.Prelude.Lattice where
import FP.Prelude.Core
import qualified Prelude
infixr 4 ⊔
infix 4 ⊟
infixr 5 ⊓
infix 6 ⊑⊒
infix 6 ⊑
infix 6 ⊒
infix 6 ><
data PartialOrdering = PLT | PEQ | PGT | PUN
class POrd a where (⊑⊒) ∷ a → a → PartialOrdering
fromOrdering ∷ Ordering → PartialOrdering
fromOrdering = \case {LT → PLT;EQ → PEQ;GT → PGT}
(⊑) ∷ (POrd a) ⇒ a → a → 𝔹
x ⊑ y = case x ⊑⊒ y of {PLT → True;PEQ → True;PGT → False;PUN → False}
(⊒) ∷ (POrd a) ⇒ a → a → 𝔹
x ⊒ y = case x ⊑⊒ y of {PLT → False;PEQ → True;PGT → True;PUN → False}
(><) ∷ (POrd a) ⇒ a → a → 𝔹
x >< y = case x ⊑⊒ y of {PLT → False;PEQ → False;PGT → False;PUN → True}
poCompareFromLte ∷ (a → a → 𝔹) → a → a → PartialOrdering
poCompareFromLte lte x y = case (lte x y,lte y x) of
(True,True) → PEQ
(True,False) → PLT
(False,True) → PGT
(False,False) → PUN
discretePO ∷ (Eq a) ⇒ a → a → PartialOrdering
discretePO = poCompareFromLte (==)
class Bot a where bot ∷ a
class Join a where (⊔) ∷ a → a → a
class Top a where top ∷ a
class Meet a where (⊓) ∷ a → a → a
class Dual a where dual ∷ a → a
class Difference a where (⊟) ∷ a → a → a
class (Bot a,Join a) ⇒ JoinLattice a
class (Top a,Meet a) ⇒ MeetLattice a
class (JoinLattice a,MeetLattice a) ⇒ Lattice a
class (Lattice a,Dual a) ⇒ DualLattice a
instance POrd ℤ where (⊑⊒) = fromOrdering ∘∘ compare
instance Join ℤ where (⊔) = Prelude.max
instance Meet ℤ where (⊓) = Prelude.min
instance POrd ℕ where (⊑⊒) = fromOrdering ∘∘ compare
instance Bot ℕ where bot = 𝕟 0
instance Join ℕ where (⊔) = Prelude.max
instance Meet ℕ where (⊓) = Prelude.min
instance JoinLattice ℕ
instance POrd ℕᵀ where
NInfinity ⊑⊒ NInfinity = PEQ
NInfinity ⊑⊒ NFinite _ = PGT
NFinite _ ⊑⊒ NInfinity = PLT
NFinite x ⊑⊒ NFinite y = x ⊑⊒ y
instance Bot ℕᵀ where bot = 𝕟ᵀ 0
instance Join ℕᵀ where
NInfinity ⊔ _ = NInfinity
_ ⊔ NInfinity = NInfinity
NFinite x ⊔ NFinite y = NFinite $ x ⊔ y
instance JoinLattice ℕᵀ
instance Top ℕᵀ where top = NInfinity
instance Meet ℕᵀ where
NInfinity ⊓ x = x
x ⊓ NInfinity = x
NFinite x ⊓ NFinite y = NFinite $ x ⊓ y
instance MeetLattice ℕᵀ
instance Lattice ℕᵀ
instance POrd 𝕀 where (⊑⊒) = fromOrdering ∘∘ compare
instance Bot 𝕀 where bot = Prelude.minBound
instance Join 𝕀 where (⊔) = Prelude.max
instance Top 𝕀 where top = Prelude.maxBound
instance Meet 𝕀 where (⊓) = Prelude.min
instance JoinLattice 𝕀
instance MeetLattice 𝕀
instance Lattice 𝕀
instance POrd 𝔻 where (⊑⊒) = fromOrdering ∘∘ compare
instance Bot 𝔻 where bot = 𝕤read "NInfinity"
instance Join 𝔻 where (⊔) = Prelude.max
instance Top 𝔻 where top = 𝕤read "-NInfinity"
instance Meet 𝔻 where (⊓) = Prelude.min
instance JoinLattice 𝔻
instance MeetLattice 𝔻
instance Lattice 𝔻
instance POrd 𝔹 where (⊑⊒) = fromOrdering ∘∘ (⋚)
instance Bot 𝔹 where bot = False
instance Join 𝔹 where (⊔) = (∨)
instance Top 𝔹 where top = True
instance Meet 𝔹 where (⊓) = (∧)
instance Dual 𝔹 where dual = not
instance JoinLattice 𝔹
instance MeetLattice 𝔹
instance Lattice 𝔹
instance DualLattice 𝔹
instance (POrd a,POrd b) ⇒ POrd (a,b) where (⊑⊒) = poCompareFromLte $ \(a₁,b₁)(a₂,b₂)→(a₁⊑a₂)∧(b₁⊑b₂)
instance (Bot a,Bot b) ⇒ Bot (a,b) where bot = (bot,bot)
instance (Join a,Join b) ⇒ Join (a,b) where (a₁,b₁) ⊔ (a₂,b₂) = (a₁ ⊔ a₂,b₁ ⊔ b₂)
instance (Top a,Top b) ⇒ Top (a,b) where top = (top,top)
instance (Meet a,Meet b) ⇒ Meet (a,b) where (a₁,b₁) ⊓ (a₂,b₂) = (a₁ ⊓ a₂,b₁ ⊓ b₂)
instance (Dual a,Dual b) ⇒ Dual (a,b) where dual (a,b) = (dual a,dual b)
instance (Difference a,Difference b) ⇒ Difference (a,b) where (a₁,b₁) ⊟ (a₂,b₂) = (a₁ ⊟ a₂,b₁ ⊟ b₂)
instance (JoinLattice a,JoinLattice b) ⇒ JoinLattice (a,b)
instance (MeetLattice a,MeetLattice b) ⇒ MeetLattice (a,b)
instance (Lattice a,Lattice b) ⇒ Lattice (a,b)
instance (DualLattice a,DualLattice b) ⇒ DualLattice (a,b)
instance (POrd a) ⇒ POrd (Maybe a) where
Nothing ⊑⊒ Nothing = PEQ
Just _ ⊑⊒ Nothing = PUN
Nothing ⊑⊒ Just _ = PUN
Just x ⊑⊒ Just y = x ⊑⊒ y
instance (Bot b) ⇒ Bot (a → b) where bot = const bot
instance (Join b) ⇒ Join (a → b) where (f ⊔ g) x = f x ⊔ g x
instance (Top b) ⇒ Top (a → b) where top = const top
instance (Meet b) ⇒ Meet (a → b) where (f ⊓ g) x = f x ⊓ g x
instance (Dual b) ⇒ Dual (a → b) where dual f = dual ∘ f
instance (Difference b) ⇒ Difference (a → b) where (f ⊟ g) x = f x ⊟ g x
instance (JoinLattice b) ⇒ JoinLattice (a → b)
instance (MeetLattice b) ⇒ MeetLattice (a → b)
instance (Lattice b) ⇒ Lattice (a → b)
instance (DualLattice b) ⇒ DualLattice (a → b)
instance POrd (𝒫 a) where (⊑⊒) = poCompareFromLte isSubsetOf
instance Bot (𝒫 a) where bot = EmptySet
instance Join (𝒫 a) where (⊔) = unionSet
instance Meet (𝒫 a) where (⊓) = intersectionSet
instance Difference (𝒫 a) where (⊟) = differenceSet
instance JoinLattice (𝒫 a)
instance (POrd v) ⇒ POrd (k ⇰ v) where (⊑⊒) = poCompareFromLte $ isSubdictOfBy (⊑)
instance Bot (k ⇰ v) where bot = EmptyDict
instance (Join v) ⇒ Join (k ⇰ v) where (⊔) = unionWithDict (⊔)
instance (Meet v) ⇒ Meet (k ⇰ v) where (⊓) = intersectionWithDict (⊓)
instance (Join v) ⇒ JoinLattice (k ⇰ v)
instance (Difference v) ⇒ Difference (k ⇰ v) where (⊟) = differenceWithDict (⊟)
dictJoin ∷ (ToFold (k,v) t,Ord k,JoinLattice v) ⇒ t → k ⇰ v
dictJoin = iter ((⊔) ∘ single) bot
mapKeyJoin ∷ (Ord k₂,JoinLattice v) ⇒ (k₁ → k₂) → k₁ ⇰ v → k₂ ⇰ v
mapKeyJoin f kvs = dictJoin $ map (mapFst f) $ list kvs
instance (Ord a) ⇒ POrd (𝒫ᵇ a) where (⊑⊒) = (⊑⊒) `on` concretizeSet
instance Bot (𝒫ᵇ a) where bot = LazySet null
instance Join (𝒫ᵇ a) where LazySet xs ⊔ LazySet ys = LazySet $ xs ⧺ ys
instance JoinLattice (𝒫ᵇ a)
instance (Ord a) ⇒ Difference (𝒫ᵇ a) where
(⊟) = lazySet ∘∘ ((⊟) `on` concretizeSet)
instance Monad 𝒫ᵇ where
return = LazySet ∘ single
xs ≫= f = joins $ map f xs
instance (Ord k,Eq v,JoinLattice v) ⇒ Eq (k ⇰♭⊔ v) where (==) = (==) `on` concretizeDictJoin
instance (Ord k,Ord v,JoinLattice v) ⇒ Ord (k ⇰♭⊔ v) where compare = compare `on` concretizeDictJoin
instance (Ord k,Show k,Show v,JoinLattice v) ⇒ Show (k ⇰♭⊔ v) where show = chars ∘ (⧺) "dictᵇ " ∘ 𝕤show ∘ list ∘ concretizeDictJoin
instance ToFold (k,v) (k ⇰♭⊔ v) where fold = runLazyDictJoin
instance Singleton (k,v) (k ⇰♭⊔ v) where single = lazyDictJoin ∘ singleFold
instance (Ord k,POrd v,JoinLattice v) ⇒ POrd (k ⇰♭⊔ v) where (⊑⊒) = (⊑⊒) `on` concretizeDictJoin
instance Bot (k ⇰♭⊔ v) where bot = LazyDictJoin null
instance Join (k ⇰♭⊔ v) where LazyDictJoin xvs ⊔ LazyDictJoin yvs = LazyDictJoin $ xvs ⧺ yvs
instance JoinLattice (k ⇰♭⊔ v)
instance (Ord k,JoinLattice v,Difference v) ⇒ Difference (k ⇰♭⊔ v) where (⊟) = lazyDictJoin ∘∘ ((⊟) `on` concretizeDictJoin)
concretizeDictJoin ∷ (Ord k,JoinLattice v) ⇒ k ⇰♭⊔ v → k ⇰ v
concretizeDictJoin (LazyDictJoin kvs) = dictJoin kvs
lazyDictJoin ∷ (ToFold (k,v) t) ⇒ t → k ⇰♭⊔ v
lazyDictJoin = LazyDictJoin ∘ fold
mapKeyLazyDictJoin ∷ (k → k') → k ⇰♭⊔ v → k' ⇰♭⊔ v
mapKeyLazyDictJoin f = LazyDictJoin ∘ map (mapFst f) ∘ runLazyDictJoin
joins ∷ (JoinLattice a,ToFold a t) ⇒ t → a
joins = iter (⊔) bot
meets ∷ (MeetLattice a,ToFold a t) ⇒ t → a
meets = iter (⊓) top
data AddBot a = Bot | AddBot a
deriving (Eq,Ord)
instance Functor AddBot where
map _ Bot = Bot
map f (AddBot x) = AddBot $ f x
instance Bot (AddBot a) where bot = Bot
instance (Join a) ⇒ Join (AddBot a) where
Bot ⊔ x = x
x ⊔ Bot = x
AddBot x ⊔ AddBot y = AddBot $ x ⊔ y
instance (Top a) ⇒ Top (AddBot a) where top = AddBot top
instance (Meet a) ⇒ Meet (AddBot a) where
Bot ⊓ _ = Bot
_ ⊓ Bot = Bot
AddBot x ⊓ AddBot y = AddBot $ x ⊓ y
instance (Join a) ⇒ JoinLattice (AddBot a)
instance (MeetLattice a) ⇒ MeetLattice (AddBot a)
instance (Join a,MeetLattice a) ⇒ Lattice (AddBot a)
elimAddBot ∷ b → (a → b) → AddBot a → b
elimAddBot b _ Bot = b
elimAddBot _ f (AddBot x) = f x
data AddTop a = AddTop a | Top
deriving (Eq,Ord)
instance Functor AddTop where
map _ Top = Top
map f (AddTop x) = AddTop $ f x
instance (Bot a) ⇒ Bot (AddTop a) where bot = AddTop bot
instance (Join a) ⇒ Join (AddTop a) where
Top ⊔ _ = Top
_ ⊔ Top = Top
AddTop x ⊔ AddTop y = AddTop $ x ⊔ y
instance Top (AddTop a) where top = Top
instance (Meet a) ⇒ Meet (AddTop a) where
Top ⊓ x = x
x ⊓ Top = x
AddTop x ⊓ AddTop y = AddTop $ x ⊓ y
instance (JoinLattice a) ⇒ JoinLattice (AddTop a)
instance (Meet a) ⇒ MeetLattice (AddTop a)
instance (JoinLattice a,Meet a) ⇒ Lattice (AddTop a)