diff --git a/Algebra/Enumerable.hs b/Algebra/Enumerable.hs deleted file mode 100644 --- a/Algebra/Enumerable.hs +++ /dev/null @@ -1,50 +0,0 @@ -{-# LANGUAGE Safe #-} ----------------------------------------------------------------------------- --- | --- Module : Algebra.Enumerable --- Copyright : (C) 2010-2015 Maximilian Bolingbroke --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- -module Algebra.Enumerable {-# DEPRECATED "Use Data.Universe.Class" #-} ( - Enumerable(..), universeBounded, - Enumerated(..) - ) where - --- | Finitely enumerable things -class Enumerable a where - universe :: [a] - -universeBounded :: (Enum a, Bounded a) => [a] -universeBounded = enumFromTo minBound maxBound - - --- | Wrapper used to mark where we expect to use the fact that something is Enumerable -newtype Enumerated a = Enumerated { unEnumerated :: a } - deriving (Eq, Ord) - -instance Enumerable a => Enumerable (Enumerated a) where - universe = map Enumerated universe - - --- TODO: add to this rather sorry little set of instances. Can we exploit commonality with lazy-smallcheck? - -instance Enumerable Bool where - universe = universeBounded - -instance Enumerable Int where - universe = universeBounded - -instance Enumerable a => Enumerable (Maybe a) where - universe = Nothing : map Just universe - -instance (Enumerable a, Enumerable b) => Enumerable (Either a b) where - universe = map Left universe ++ map Right universe - -instance Enumerable () where - universe = [()] - -instance (Enumerable a, Enumerable b) => Enumerable (a, b) where - universe = [(a, b) | a <- universe, b <- universe] diff --git a/Algebra/Lattice.hs b/Algebra/Lattice.hs deleted file mode 100644 --- a/Algebra/Lattice.hs +++ /dev/null @@ -1,566 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE FlexibleInstances #-} -#if __GLASGOW_HASKELL__ >=710 && MIN_VERSION_unordered_containers(0,2,6) -{-# LANGUAGE Safe #-} -#else -{-# LANGUAGE Trustworthy #-} -#endif -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} -#if __GLASGOW_HASKELL__ >= 707 && __GLASGOW_HASKELL__ < 709 -{-# OPTIONS_GHC -fno-warn-amp #-} -#endif ----------------------------------------------------------------------------- --- | --- Module : Algebra.Lattice --- Copyright : (C) 2010-2015 Maximilian Bolingbroke --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- --- In mathematics, a lattice is a partially ordered set in which every --- two elements have a unique supremum (also called a least upper bound --- or @join@) and a unique infimum (also called a greatest lower bound or --- @meet@). --- --- In this module lattices are defined using 'meet' and 'join' operators, --- as it's constructive one. --- ----------------------------------------------------------------------------- -module Algebra.Lattice ( - -- * Unbounded lattices - JoinSemiLattice(..), MeetSemiLattice(..), Lattice, - joinLeq, joins1, meetLeq, meets1, - - -- * Bounded lattices - BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..), BoundedLattice, - joins, meets, - fromBool, - - -- * Monoid wrappers - Meet(..), Join(..), - - -- * Fixed points of chains in lattices - lfp, lfpFrom, unsafeLfp, - gfp, gfpFrom, unsafeGfp, - ) where - -import Prelude () -import Prelude.Compat - -import qualified Algebra.PartialOrd as PO - -import Data.Universe.Class (Universe(..), Finite(..)) - -import Control.Monad.Zip (MonadZip(..)) -import Data.Data (Data, Typeable) -import Data.Hashable (Hashable(..)) -import Data.Proxy (Proxy(..)) -import Data.Semigroup (Semigroup(..), Endo(..), Any(..), All(..)) -import Data.Tagged (Tagged(..)) -import Data.Void (Void) -import GHC.Generics (Generic) - -import qualified Data.IntMap as IM -import qualified Data.IntSet as IS -import qualified Data.Map as M -import qualified Data.Set as S - -import qualified Data.HashSet as HS -import qualified Data.HashMap.Lazy as HM - -import Control.Applicative (Const(..)) -import Data.Functor.Identity (Identity(..)) -import Data.Semigroup.Foldable (Foldable1 (..)) - -infixr 6 /\ -- This comment needed because of CPP -infixr 5 \/ - --- | A algebraic structure with element joins: --- --- > Associativity: x \/ (y \/ z) == (x \/ y) \/ z --- > Commutativity: x \/ y == y \/ x --- > Idempotency: x \/ x == x -class JoinSemiLattice a where - (\/) :: a -> a -> a - (\/) = join - - join :: a -> a -> a - join = (\/) - -#if __GLASGOW_HASKELL__ >= 707 - {-# MINIMAL (\/) | join #-} -#endif -{-# DEPRECATED join "Use '\\/' infix operator" #-} - --- | The partial ordering induced by the join-semilattice structure -joinLeq :: (Eq a, JoinSemiLattice a) => a -> a -> Bool -joinLeq x y = (x \/ y) == y - --- | A algebraic structure with element meets: --- --- > Associativity: x /\ (y /\ z) == (x /\ y) /\ z --- > Commutativity: x /\ y == y /\ x --- > Idempotency: x /\ x == x -class MeetSemiLattice a where - (/\) :: a -> a -> a - (/\) = meet - - meet :: a -> a -> a - meet = (/\) - -#if __GLASGOW_HASKELL__ >= 707 - {-# MINIMAL (/\) | meet #-} -#endif -{-# DEPRECATED meet "Use '/\\' infix operator" #-} - --- | The partial ordering induced by the meet-semilattice structure -meetLeq :: (Eq a, MeetSemiLattice a) => a -> a -> Bool -meetLeq x y = (x /\ y) == x - - - --- | The combination of two semi lattices makes a lattice if the absorption law holds: --- see and --- --- > Absorption: a \/ (a /\ b) == a /\ (a \/ b) == a -class (JoinSemiLattice a, MeetSemiLattice a) => Lattice a where - --- | A join-semilattice with some element |bottom| that \/ approaches. --- --- > Identity: x \/ bottom == x -class JoinSemiLattice a => BoundedJoinSemiLattice a where - bottom :: a - --- | The join of a list of join-semilattice elements -joins :: (BoundedJoinSemiLattice a, Foldable f) => f a -> a -joins = getJoin . foldMap Join - --- | The join of at a list of join-semilattice elements (of length at least one) -joins1 :: (JoinSemiLattice a, Foldable1 f) => f a -> a -joins1 = getJoin . foldMap1 Join - --- | A meet-semilattice with some element |top| that /\ approaches. --- --- > Identity: x /\ top == x -class MeetSemiLattice a => BoundedMeetSemiLattice a where - top :: a - --- | The meet of a list of meet-semilattice elements -meets :: (BoundedMeetSemiLattice a, Foldable f) => f a -> a -meets = getMeet . foldMap Meet --- --- | The meet of at a list of meet-semilattice elements (of length at least one) -meets1 :: (MeetSemiLattice a, Foldable1 f) => f a -> a -meets1 = getMeet . foldMap1 Meet - --- | Lattices with both bounds -class (Lattice a, BoundedJoinSemiLattice a, BoundedMeetSemiLattice a) => BoundedLattice a where - --- | 'True' to 'top' and 'False' to 'bottom' -fromBool :: BoundedLattice a => Bool -> a -fromBool True = top -fromBool False = bottom - --- --- Sets --- - -instance Ord a => JoinSemiLattice (S.Set a) where - (\/) = S.union - -instance Ord a => MeetSemiLattice (S.Set a) where - (/\) = S.intersection - -instance Ord a => Lattice (S.Set a) where - -instance Ord a => BoundedJoinSemiLattice (S.Set a) where - bottom = S.empty - -instance (Ord a, Finite a) => BoundedMeetSemiLattice (S.Set a) where - top = S.fromList universeF - -instance (Ord a, Finite a) => BoundedLattice (S.Set a) where - --- --- IntSets --- - -instance JoinSemiLattice IS.IntSet where - (\/) = IS.union - -instance MeetSemiLattice IS.IntSet where - (/\) = IS.intersection - -instance Lattice IS.IntSet - -instance BoundedJoinSemiLattice IS.IntSet where - bottom = IS.empty - --- --- HashSet --- - -instance (Eq a, Hashable a) => JoinSemiLattice (HS.HashSet a) where - (\/) = HS.union - -instance (Eq a, Hashable a) => MeetSemiLattice (HS.HashSet a) where - (/\) = HS.intersection - -instance (Eq a, Hashable a) => Lattice (HS.HashSet a) - -instance (Eq a, Hashable a) => BoundedJoinSemiLattice (HS.HashSet a) where - bottom = HS.empty - --- --- Maps --- - -instance (Ord k, JoinSemiLattice v) => JoinSemiLattice (M.Map k v) where - (\/) = M.unionWith (\/) - -instance (Ord k, MeetSemiLattice v) => MeetSemiLattice (M.Map k v) where - (/\) = M.intersectionWith (/\) - -instance (Ord k, Lattice v) => Lattice (M.Map k v) where - -instance (Ord k, JoinSemiLattice v) => BoundedJoinSemiLattice (M.Map k v) where - bottom = M.empty - -instance (Ord k, Finite k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (M.Map k v) where - top = M.fromList (universeF `zip` repeat top) - -instance (Ord k, Finite k, BoundedLattice v) => BoundedLattice (M.Map k v) where - --- --- IntMaps --- - -instance JoinSemiLattice v => JoinSemiLattice (IM.IntMap v) where - (\/) = IM.unionWith (\/) - -instance JoinSemiLattice v => BoundedJoinSemiLattice (IM.IntMap v) where - bottom = IM.empty - -instance MeetSemiLattice v => MeetSemiLattice (IM.IntMap v) where - (/\) = IM.intersectionWith (/\) - -instance Lattice v => Lattice (IM.IntMap v) - - --- --- HashMaps --- - -instance (Eq k, Hashable k) => JoinSemiLattice (HM.HashMap k v) where - (\/) = HM.union - -instance (Eq k, Hashable k) => MeetSemiLattice (HM.HashMap k v) where - (/\) = HM.intersection - -instance (Eq k, Hashable k) => BoundedJoinSemiLattice (HM.HashMap k v) where - bottom = HM.empty - --- --- Functions --- - -instance JoinSemiLattice v => JoinSemiLattice (k -> v) where - f \/ g = \x -> f x \/ g x - -instance MeetSemiLattice v => MeetSemiLattice (k -> v) where - f /\ g = \x -> f x /\ g x - -instance Lattice v => Lattice (k -> v) where - -instance BoundedJoinSemiLattice v => BoundedJoinSemiLattice (k -> v) where - bottom = const bottom - -instance BoundedMeetSemiLattice v => BoundedMeetSemiLattice (k -> v) where - top = const top - -instance BoundedLattice v => BoundedLattice (k -> v) where - --- Unit -instance JoinSemiLattice () where - _ \/ _ = () - -instance BoundedJoinSemiLattice () where - bottom = () - -instance MeetSemiLattice () where - _ /\ _ = () - -instance BoundedMeetSemiLattice () where - top = () - -instance Lattice () where -instance BoundedLattice () where - --- --- Tuples --- - -instance (JoinSemiLattice a, JoinSemiLattice b) => JoinSemiLattice (a, b) where - (x1, y1) \/ (x2, y2) = (x1 \/ x2, y1 \/ y2) - -instance (MeetSemiLattice a, MeetSemiLattice b) => MeetSemiLattice (a, b) where - (x1, y1) /\ (x2, y2) = (x1 /\ x2, y1 /\ y2) - -instance (Lattice a, Lattice b) => Lattice (a, b) where - -instance (BoundedJoinSemiLattice a, BoundedJoinSemiLattice b) => BoundedJoinSemiLattice (a, b) where - bottom = (bottom, bottom) - -instance (BoundedMeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (a, b) where - top = (top, top) - -instance (BoundedLattice a, BoundedLattice b) => BoundedLattice (a, b) where - --- --- Bools --- - -instance JoinSemiLattice Bool where - (\/) = (||) - -instance MeetSemiLattice Bool where - (/\) = (&&) - -instance Lattice Bool where - -instance BoundedJoinSemiLattice Bool where - bottom = False - -instance BoundedMeetSemiLattice Bool where - top = True - -instance BoundedLattice Bool where - ---- Monoids - --- | Monoid wrapper for JoinSemiLattice -newtype Join a = Join { getJoin :: a } - deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic) - -instance JoinSemiLattice a => Semigroup (Join a) where - Join a <> Join b = Join (a \/ b) - -instance BoundedJoinSemiLattice a => Monoid (Join a) where - mempty = Join bottom - Join a `mappend` Join b = Join (a \/ b) - -instance Functor Join where - fmap f (Join x) = Join (f x) - -instance Applicative Join where - pure = Join - Join f <*> Join x = Join (f x) - _ *> x = x - -instance Monad Join where - return = pure - Join m >>= f = f m - (>>) = (*>) - -instance MonadZip Join where - mzip (Join x) (Join y) = Join (x, y) - -instance Universe a => Universe (Join a) where - universe = fmap Join universe - -instance Finite a => Finite (Join a) where - universeF = fmap Join universeF - --- | Monoid wrapper for MeetSemiLattice -newtype Meet a = Meet { getMeet :: a } - deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic) - -instance MeetSemiLattice a => Semigroup (Meet a) where - Meet a <> Meet b = Meet (a /\ b) - -instance BoundedMeetSemiLattice a => Monoid (Meet a) where - mempty = Meet top - Meet a `mappend` Meet b = Meet (a /\ b) - -instance Functor Meet where - fmap f (Meet x) = Meet (f x) - -instance Applicative Meet where - pure = Meet - Meet f <*> Meet x = Meet (f x) - _ *> x = x - -instance Monad Meet where - return = pure - Meet m >>= f = f m - (>>) = (*>) - -instance MonadZip Meet where - mzip (Meet x) (Meet y) = Meet (x, y) - -instance Universe a => Universe (Meet a) where - universe = fmap Meet universe - -instance Finite a => Finite (Meet a) where - universeF = fmap Meet universeF - --- All -instance JoinSemiLattice All where - All a \/ All b = All $ a \/ b - -instance BoundedJoinSemiLattice All where - bottom = All False - -instance MeetSemiLattice All where - All a /\ All b = All $ a /\ b - -instance BoundedMeetSemiLattice All where - top = All True - -instance Lattice All where -instance BoundedLattice All where - --- Any -instance JoinSemiLattice Any where - Any a \/ Any b = Any $ a \/ b - -instance BoundedJoinSemiLattice Any where - bottom = Any False - -instance MeetSemiLattice Any where - Any a /\ Any b = Any $ a /\ b - -instance BoundedMeetSemiLattice Any where - top = Any True - -instance Lattice Any where -instance BoundedLattice Any where - --- Endo -instance JoinSemiLattice a => JoinSemiLattice (Endo a) where - Endo a \/ Endo b = Endo $ a \/ b - -instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Endo a) where - bottom = Endo bottom - -instance MeetSemiLattice a => MeetSemiLattice (Endo a) where - Endo a /\ Endo b = Endo $ a /\ b - -instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Endo a) where - top = Endo top - -instance Lattice a => Lattice (Endo a) where -instance BoundedLattice a => BoundedLattice (Endo a) where - --- Tagged -instance JoinSemiLattice a => JoinSemiLattice (Tagged t a) where - Tagged a \/ Tagged b = Tagged $ a \/ b - -instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Tagged t a) where - bottom = Tagged bottom - -instance MeetSemiLattice a => MeetSemiLattice (Tagged t a) where - Tagged a /\ Tagged b = Tagged $ a /\ b - -instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Tagged t a) where - top = Tagged top - -instance Lattice a => Lattice (Tagged t a) where -instance BoundedLattice a => BoundedLattice (Tagged t a) where - --- Proxy -instance JoinSemiLattice (Proxy a) where - _ \/ _ = Proxy - -instance BoundedJoinSemiLattice (Proxy a) where - bottom = Proxy - -instance MeetSemiLattice (Proxy a) where - _ /\ _ = Proxy - -instance BoundedMeetSemiLattice (Proxy a) where - top = Proxy - -instance Lattice (Proxy a) where -instance BoundedLattice (Proxy a) where - -#if MIN_VERSION_base(4,8,0) --- Identity -instance JoinSemiLattice a => JoinSemiLattice (Identity a) where - Identity a \/ Identity b = Identity (a \/ b) - -instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Identity a) where - bottom = Identity bottom - -instance MeetSemiLattice a => MeetSemiLattice (Identity a) where - Identity a /\ Identity b = Identity (a /\ b) - -instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Identity a) where - top = Identity top - -instance Lattice a => Lattice (Identity a) where -instance BoundedLattice a => BoundedLattice (Identity a) where -#endif - --- Const -instance JoinSemiLattice a => JoinSemiLattice (Const a b) where - Const a \/ Const b = Const (a \/ b) - -instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Const a b) where - bottom = Const bottom - -instance MeetSemiLattice a => MeetSemiLattice (Const a b) where - Const a /\ Const b = Const (a /\ b) - -instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Const a b) where - top = Const top - -instance Lattice a => Lattice (Const a b) where -instance BoundedLattice a => BoundedLattice (Const a b) where - --- Void -instance JoinSemiLattice Void where - a \/ _ = a - -instance MeetSemiLattice Void where - a /\ _ = a - -instance Lattice Void where - --- | Implementation of Kleene fixed-point theorem . --- Assumes that the function is monotone and does not check if that is correct. -{-# INLINE unsafeLfp #-} -unsafeLfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a -unsafeLfp = PO.unsafeLfpFrom bottom - --- | Implementation of Kleene fixed-point theorem . --- Forces the function to be monotone. -{-# INLINE lfp #-} -lfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a -lfp = lfpFrom bottom - --- | Implementation of Kleene fixed-point theorem . --- Forces the function to be monotone. -{-# INLINE lfpFrom #-} -lfpFrom :: (Eq a, BoundedJoinSemiLattice a) => a -> (a -> a) -> a -lfpFrom init_x f = PO.unsafeLfpFrom init_x (\x -> f x \/ x) - - --- | Implementation of Kleene fixed-point theorem . --- Assumes that the function is antinone and does not check if that is correct. -{-# INLINE unsafeGfp #-} -unsafeGfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a -unsafeGfp = PO.unsafeGfpFrom top - --- | Implementation of Kleene fixed-point theorem . --- Forces the function to be antinone. -{-# INLINE gfp #-} -gfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a -gfp = gfpFrom top - --- | Implementation of Kleene fixed-point theorem . --- Forces the function to be antinone. -{-# INLINE gfpFrom #-} -gfpFrom :: (Eq a, BoundedMeetSemiLattice a) => a -> (a -> a) -> a -gfpFrom init_x f = PO.unsafeGfpFrom init_x (\x -> f x /\ x) diff --git a/Algebra/Lattice/Divisibility.hs b/Algebra/Lattice/Divisibility.hs deleted file mode 100644 --- a/Algebra/Lattice/Divisibility.hs +++ /dev/null @@ -1,77 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE DeriveDataTypeable #-} -#if __GLASGOW_HASKELL__ < 709 -{-# LANGUAGE Trustworthy #-} -#else -{-# LANGUAGE Safe #-} -#endif ----------------------------------------------------------------------------- --- | --- Module : Algebra.Lattice.Divisibility --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- -module Algebra.Lattice.Divisibility ( - Divisibility(..) - ) where - -import Prelude () -import Prelude.Compat - -import Algebra.Lattice -import Algebra.PartialOrd - -import Control.DeepSeq -import Control.Monad -import Data.Data -import Data.Hashable -import GHC.Generics - --- --- Divisibility --- - --- | A divisibility lattice. @'join' = 'lcm'@, @'meet' = 'gcd'@. -newtype Divisibility a = Divisibility { getDivisibility :: a } - deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable -#if __GLASGOW_HASKELL__ >= 706 - , Generic1 -#endif - ) - -instance Applicative Divisibility where - pure = return - (<*>) = ap - -instance Monad Divisibility where - return = Divisibility - Divisibility x >>= f = f x - -instance NFData a => NFData (Divisibility a) where - rnf (Divisibility a) = rnf a - -instance Hashable a => Hashable (Divisibility a) - -instance Integral a => JoinSemiLattice (Divisibility a) where - Divisibility x \/ Divisibility y = Divisibility (lcm x y) - -instance Integral a => MeetSemiLattice (Divisibility a) where - Divisibility x /\ Divisibility y = Divisibility (gcd x y) - -instance Integral a => Lattice (Divisibility a) where - -instance Integral a => BoundedJoinSemiLattice (Divisibility a) where - bottom = Divisibility 1 - -instance (Eq a, Integral a) => PartialOrd (Divisibility a) where - leq (Divisibility a) (Divisibility b) = b `mod` a == 0 diff --git a/Algebra/Lattice/Dropped.hs b/Algebra/Lattice/Dropped.hs deleted file mode 100644 --- a/Algebra/Lattice/Dropped.hs +++ /dev/null @@ -1,92 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE DeriveDataTypeable #-} -#if __GLASGOW_HASKELL__ < 709 -{-# LANGUAGE Trustworthy #-} -#else -{-# LANGUAGE Safe #-} -#endif ----------------------------------------------------------------------------- --- | --- Module : Algebra.Lattice.Dropped --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- -module Algebra.Lattice.Dropped ( - Dropped(..) - , retractDropped - ) where - -import Prelude () -import Prelude.Compat - -import Algebra.Lattice - -import Control.DeepSeq -import Control.Monad -import Data.Data -import Data.Hashable -import GHC.Generics - --- --- Dropped --- - --- | Graft a distinct top onto an otherwise unbounded lattice. --- As a bonus, the top will be an absorbing element for the join. -data Dropped a = Top - | Drop a - deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable -#if __GLASGOW_HASKELL__ >= 706 - , Generic1 -#endif - ) - -instance Applicative Dropped where - pure = return - (<*>) = ap - -instance Monad Dropped where - return = Drop - Top >>= _ = Top - Drop x >>= f = f x - -instance NFData a => NFData (Dropped a) where - rnf Top = () - rnf (Drop a) = rnf a - -instance Hashable a => Hashable (Dropped a) - -instance JoinSemiLattice a => JoinSemiLattice (Dropped a) where - Top \/ _ = Top - _ \/ Top = Top - Drop x \/ Drop y = Drop (x \/ y) - -instance MeetSemiLattice a => MeetSemiLattice (Dropped a) where - Top /\ drop_y = drop_y - drop_x /\ Top = drop_x - Drop x /\ Drop y = Drop (x /\ y) - -instance Lattice a => Lattice (Dropped a) where - -instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Dropped a) where - bottom = Drop bottom - -instance MeetSemiLattice a => BoundedMeetSemiLattice (Dropped a) where - top = Top - -instance BoundedLattice a => BoundedLattice (Dropped a) where - --- | Interpret @'Dropped' a@ using the 'BoundedMeetSemiLattice' of @a@. -retractDropped :: BoundedMeetSemiLattice a => Dropped a -> a -retractDropped Top = top -retractDropped (Drop x) = x diff --git a/Algebra/Lattice/Free.hs b/Algebra/Lattice/Free.hs deleted file mode 100644 --- a/Algebra/Lattice/Free.hs +++ /dev/null @@ -1,148 +0,0 @@ -{-# LANGUAGE RankNTypes #-} - ----------------------------------------------------------------------------- --- | --- Module : Algebra.Lattice.Free --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- - -module Algebra.Lattice.Free - ( -- * Free join-semilattices - FreeJoinSemiLattice - , liftFreeJoinSemiLattice - , lowerFreeJoinSemiLattice - , retractFreeJoinSemiLattice - - -- * Free meet-semilattices - , FreeMeetSemiLattice - , liftFreeMeetSemiLattice - , lowerFreeMeetSemiLattice - , retractFreeMeetSemiLattice - - -- * Free lattices - , FreeLattice - , liftFreeLattice - , lowerFreeLattice - , retractFreeLattice - ) where - -import Prelude () -import Prelude.Compat - -import Algebra.Lattice -import Data.Universe.Class - --- --- Free join-semilattices --- - -newtype FreeJoinSemiLattice a = FreeJoinSemiLattice - { lowerFreeJoinSemiLattice :: forall b. JoinSemiLattice b => - (a -> b) -> b - } - -liftFreeJoinSemiLattice :: a -> FreeJoinSemiLattice a -liftFreeJoinSemiLattice a = FreeJoinSemiLattice (\inj -> inj a) - -retractFreeJoinSemiLattice :: JoinSemiLattice a => FreeJoinSemiLattice a -> a -retractFreeJoinSemiLattice a = lowerFreeJoinSemiLattice a id - -instance Functor FreeJoinSemiLattice where - fmap f (FreeJoinSemiLattice g) = FreeJoinSemiLattice (\inj -> g (inj . f)) - a <$ FreeJoinSemiLattice f = FreeJoinSemiLattice (\inj -> f (const (inj a))) - -instance JoinSemiLattice (FreeJoinSemiLattice a) where - FreeJoinSemiLattice f \/ FreeJoinSemiLattice g = - FreeJoinSemiLattice (\inj -> f inj \/ g inj) - -instance BoundedJoinSemiLattice a => - BoundedJoinSemiLattice (FreeJoinSemiLattice a) where - bottom = FreeJoinSemiLattice (\inj -> inj bottom) - -instance Universe a => Universe (FreeJoinSemiLattice a) where - universe = fmap liftFreeJoinSemiLattice universe - -instance Finite a => Finite (FreeJoinSemiLattice a) where - universeF = fmap liftFreeJoinSemiLattice universeF - - --- --- Free meet-semilattices --- - -newtype FreeMeetSemiLattice a = FreeMeetSemiLattice - { lowerFreeMeetSemiLattice :: forall b. MeetSemiLattice b => - (a -> b) -> b - } - -instance Functor FreeMeetSemiLattice where - fmap f (FreeMeetSemiLattice g) = FreeMeetSemiLattice (\inj -> g (inj . f)) - a <$ FreeMeetSemiLattice f = FreeMeetSemiLattice (\inj -> f (const (inj a))) - -liftFreeMeetSemiLattice :: a -> FreeMeetSemiLattice a -liftFreeMeetSemiLattice a = FreeMeetSemiLattice (\inj -> inj a) - -retractFreeMeetSemiLattice :: MeetSemiLattice a => FreeMeetSemiLattice a -> a -retractFreeMeetSemiLattice a = lowerFreeMeetSemiLattice a id - -instance MeetSemiLattice (FreeMeetSemiLattice a) where - FreeMeetSemiLattice f /\ FreeMeetSemiLattice g = - FreeMeetSemiLattice (\inj -> f inj /\ g inj) - -instance BoundedMeetSemiLattice a => - BoundedMeetSemiLattice (FreeMeetSemiLattice a) where - top = FreeMeetSemiLattice (\inj -> inj top) - -instance Universe a => Universe (FreeMeetSemiLattice a) where - universe = fmap liftFreeMeetSemiLattice universe - -instance Finite a => Finite (FreeMeetSemiLattice a) where - universeF = fmap liftFreeMeetSemiLattice universeF - - --- --- Free lattices --- - -newtype FreeLattice a = FreeLattice - { lowerFreeLattice :: forall b. Lattice b => - (a -> b) -> b - } - -instance Functor FreeLattice where - fmap f (FreeLattice g) = FreeLattice (\inj -> g (inj . f)) - a <$ FreeLattice f = FreeLattice (\inj -> f (const (inj a))) - -liftFreeLattice :: a -> FreeLattice a -liftFreeLattice a = FreeLattice (\inj -> inj a) - -retractFreeLattice :: Lattice a => FreeLattice a -> a -retractFreeLattice a = lowerFreeLattice a id - -instance JoinSemiLattice (FreeLattice a) where - FreeLattice f \/ FreeLattice g = FreeLattice (\inj -> f inj \/ g inj) - -instance MeetSemiLattice (FreeLattice a) where - FreeLattice f /\ FreeLattice g = FreeLattice (\inj -> f inj /\ g inj) - -instance Lattice (FreeLattice a) - -instance BoundedJoinSemiLattice a => - BoundedJoinSemiLattice (FreeLattice a) where - bottom = FreeLattice (\inj -> inj bottom) - -instance BoundedMeetSemiLattice a => - BoundedMeetSemiLattice (FreeLattice a) where - top = FreeLattice (\inj -> inj top) - -instance BoundedLattice a => - BoundedLattice (FreeLattice a) - -instance Universe a => Universe (FreeLattice a) where - universe = fmap liftFreeLattice universe - -instance Finite a => Finite (FreeLattice a) where - universeF = fmap liftFreeLattice universeF diff --git a/Algebra/Lattice/Levitated.hs b/Algebra/Lattice/Levitated.hs deleted file mode 100644 --- a/Algebra/Lattice/Levitated.hs +++ /dev/null @@ -1,101 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE DeriveDataTypeable #-} -#if __GLASGOW_HASKELL__ < 709 -{-# LANGUAGE Trustworthy #-} -#else -{-# LANGUAGE Safe #-} -#endif ----------------------------------------------------------------------------- --- | --- Module : Algebra.Lattice.Levitated --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- -module Algebra.Lattice.Levitated ( - Levitated(..) - , retractLevitated - ) where - -import Prelude () -import Prelude.Compat - -import Algebra.Lattice - -import Control.DeepSeq -import Control.Monad -import Data.Data -import Data.Hashable -import GHC.Generics - --- --- Levitated --- - --- | Graft a distinct top and bottom onto an otherwise unbounded lattice. --- The top is the absorbing element for the join, and the bottom is the absorbing --- element for the meet. -data Levitated a = Top - | Levitate a - | Bottom - deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable -#if __GLASGOW_HASKELL__ >= 706 - , Generic1 -#endif - ) - -instance Applicative Levitated where - pure = return - (<*>) = ap - -instance Monad Levitated where - return = Levitate - Top >>= _ = Top - Bottom >>= _ = Bottom - Levitate x >>= f = f x - -instance NFData a => NFData (Levitated a) where - rnf Top = () - rnf Bottom = () - rnf (Levitate a) = rnf a - -instance Hashable a => Hashable (Levitated a) - -instance JoinSemiLattice a => JoinSemiLattice (Levitated a) where - Top \/ _ = Top - _ \/ Top = Top - Levitate x \/ Levitate y = Levitate (x \/ y) - Bottom \/ lev_y = lev_y - lev_x \/ Bottom = lev_x - -instance MeetSemiLattice a => MeetSemiLattice (Levitated a) where - Top /\ lev_y = lev_y - lev_x /\ Top = lev_x - Levitate x /\ Levitate y = Levitate (x /\ y) - Bottom /\ _ = Bottom - _ /\ Bottom = Bottom - -instance Lattice a => Lattice (Levitated a) where - -instance JoinSemiLattice a => BoundedJoinSemiLattice (Levitated a) where - bottom = Bottom - -instance MeetSemiLattice a => BoundedMeetSemiLattice (Levitated a) where - top = Top - -instance Lattice a => BoundedLattice (Levitated a) where - --- | Interpret @'Levitated' a@ using the 'BoundedLattice' of @a@. -retractLevitated :: BoundedLattice a => Levitated a -> a -retractLevitated Top = top -retractLevitated Bottom = bottom -retractLevitated (Levitate x) = x diff --git a/Algebra/Lattice/Lexicographic.hs b/Algebra/Lattice/Lexicographic.hs deleted file mode 100644 --- a/Algebra/Lattice/Lexicographic.hs +++ /dev/null @@ -1,130 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE DeriveDataTypeable #-} -#if __GLASGOW_HASKELL__ < 709 -{-# LANGUAGE Trustworthy #-} -#else -{-# LANGUAGE Safe #-} -#endif ----------------------------------------------------------------------------- --- | --- Module : Algebra.Lattice.Lexicographic --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- -module Algebra.Lattice.Lexicographic ( - Lexicographic(..) - ) where - -import Prelude () -import Prelude.Compat - -import Algebra.Lattice -import Algebra.PartialOrd - -import Control.DeepSeq -import Control.Monad -import Data.Data -import Data.Hashable -import GHC.Generics - --- --- Lexicographic --- - --- | A pair lattice with a lexicographic ordering. This means in --- a join the second component of the resulting pair is the second --- component of the pair with the larger first component. If the --- first components are equal, then the second components will be --- joined. The meet is similar only it prefers the smaller first --- component. --- --- An application of this type is versioning. For example, a --- Last-Writer-Wins register would look like --- 'Lexicographc (Ordered Timestamp) v' where the lattice --- structure handles the, presumably rare, case of matching --- 'Timestamps'. Typically this is done in an arbitary, but --- deterministic manner. -data Lexicographic k v = Lexicographic !k !v - deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable -#if __GLASGOW_HASKELL__ >= 706 - , Generic1 -#endif - ) - -instance BoundedJoinSemiLattice k => Applicative (Lexicographic k) where - pure = return - (<*>) = ap - --- Essentially the Writer monad. -instance BoundedJoinSemiLattice k => Monad (Lexicographic k) where - return = Lexicographic bottom - Lexicographic k v >>= f = - case f v of - Lexicographic k' v' -> Lexicographic (k \/ k') v' - -instance (NFData k, NFData v) => NFData (Lexicographic k v) where - rnf (Lexicographic k v) = rnf k `seq` rnf v - -instance (Hashable k, Hashable v) => Hashable (Lexicographic k v) - --- Why we have 'bottom', and not @v1 \\/ v2@ in the @otherwise@ clause? --- --- For example what is the join of @(2, 1)@ and @(3, 2)@ --- in lexicographic divisibility divisibility lattice. --- --- With @v1 \\/ v2@, we get the upper bound, but not least! --- --- @ --- (2, 1) `leq` (6, 2) --- (3, 2) `leq` (6, 2) --- @ --- --- But @(6, 1) `leq` (6, 2)@, and --- --- @ --- (2, 1) `leq` (6, 1) --- (3, 2) `leq` (6, 1) --- @ --- -instance (PartialOrd k, JoinSemiLattice k, BoundedJoinSemiLattice v) => JoinSemiLattice (Lexicographic k v) where - l@(Lexicographic k1 v1) \/ r@(Lexicographic k2 v2) - | k1 == k2 = Lexicographic k1 (v1 \/ v2) - | k1 `leq` k2 = r - | k2 `leq` k1 = l - | otherwise = Lexicographic (k1 \/ k2) bottom - -instance (PartialOrd k, MeetSemiLattice k, BoundedMeetSemiLattice v) => MeetSemiLattice (Lexicographic k v) where - l@(Lexicographic k1 v1) /\ r@(Lexicographic k2 v2) - | k1 == k2 = Lexicographic k1 (v1 /\ v2) - | k1 `leq` k2 = l - | k2 `leq` k1 = r - | otherwise = Lexicographic (k1 /\ k2) top - -instance (PartialOrd k, Lattice k, BoundedLattice v) => Lattice (Lexicographic k v) where - -instance (PartialOrd k, BoundedJoinSemiLattice k, BoundedJoinSemiLattice v) => BoundedJoinSemiLattice (Lexicographic k v) where - bottom = Lexicographic bottom bottom - -instance (PartialOrd k, BoundedMeetSemiLattice k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (Lexicographic k v) where - top = Lexicographic top top - -instance (PartialOrd k, BoundedLattice k, BoundedLattice v) => BoundedLattice (Lexicographic k v) where - -instance (PartialOrd k, PartialOrd v) => PartialOrd (Lexicographic k v) where - Lexicographic k1 v1 `leq` Lexicographic k2 v2 - | k1 == k2 = v1 `leq` v2 - | k1 `leq` k2 = True - | otherwise = False -- Incomparable or k2 `leq` k1 - comparable (Lexicographic k1 v1) (Lexicographic k2 v2) - | k1 == k2 = comparable v1 v2 - | otherwise = comparable k1 k2 diff --git a/Algebra/Lattice/Lifted.hs b/Algebra/Lattice/Lifted.hs deleted file mode 100644 --- a/Algebra/Lattice/Lifted.hs +++ /dev/null @@ -1,91 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -#if __GLASGOW_HASKELL__ < 709 -{-# LANGUAGE Trustworthy #-} -#else -{-# LANGUAGE Safe #-} -#endif ----------------------------------------------------------------------------- --- | --- Module : Algebra.Lattice.Lifted --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- -module Algebra.Lattice.Lifted ( - Lifted(..) - , retractLifted - ) where - -import Prelude () -import Prelude.Compat - -import Algebra.Lattice - -import Control.DeepSeq -import Control.Monad -import Data.Data -import Data.Hashable -import GHC.Generics - --- --- Lifted --- - --- | Graft a distinct bottom onto an otherwise unbounded lattice. --- As a bonus, the bottom will be an absorbing element for the meet. -data Lifted a = Lift a - | Bottom - deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable -#if __GLASGOW_HASKELL__ >= 706 - , Generic1 -#endif - ) - -instance Applicative Lifted where - pure = return - (<*>) = ap - -instance Monad Lifted where - return = Lift - Bottom >>= _ = Bottom - Lift x >>= f = f x - -instance NFData a => NFData (Lifted a) where - rnf Bottom = () - rnf (Lift a) = rnf a - -instance Hashable a => Hashable (Lifted a) - -instance JoinSemiLattice a => JoinSemiLattice (Lifted a) where - Lift x \/ Lift y = Lift (x \/ y) - Bottom \/ lift_y = lift_y - lift_x \/ Bottom = lift_x - -instance MeetSemiLattice a => MeetSemiLattice (Lifted a) where - Lift x /\ Lift y = Lift (x /\ y) - Bottom /\ _ = Bottom - _ /\ Bottom = Bottom - -instance Lattice a => Lattice (Lifted a) where - -instance JoinSemiLattice a => BoundedJoinSemiLattice (Lifted a) where - bottom = Bottom - -instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Lifted a) where - top = Lift top - -instance BoundedLattice a => BoundedLattice (Lifted a) where - --- | Interpret @'Lifted' a@ using the 'BoundedJoinSemiLattice' of @a@. -retractLifted :: BoundedJoinSemiLattice a => Lifted a -> a -retractLifted Bottom = bottom -retractLifted (Lift x) = x diff --git a/Algebra/Lattice/Op.hs b/Algebra/Lattice/Op.hs deleted file mode 100644 --- a/Algebra/Lattice/Op.hs +++ /dev/null @@ -1,84 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE DeriveDataTypeable #-} -#if __GLASGOW_HASKELL__ < 709 -{-# LANGUAGE Trustworthy #-} -#else -{-# LANGUAGE Safe #-} -#endif ----------------------------------------------------------------------------- --- | --- Module : Algebra.Lattice.Op --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- -module Algebra.Lattice.Op ( - Op(..) - ) where - -import Prelude () -import Prelude.Compat - -import Algebra.Lattice -import Algebra.PartialOrd - -import Control.DeepSeq -import Control.Monad -import Data.Data -import Data.Hashable -import GHC.Generics - --- --- Op --- - --- | The opposite lattice of a given lattice. That is, switch --- meets and joins. -newtype Op a = Op { getOp :: a } - deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable -#if __GLASGOW_HASKELL__ >= 706 - , Generic1 -#endif - ) - -instance Applicative Op where - pure = return - (<*>) = ap - -instance Monad Op where - return = Op - Op x >>= f = f x - -instance NFData a => NFData (Op a) where - rnf (Op a) = rnf a - -instance Hashable a => Hashable (Op a) - -instance MeetSemiLattice a => JoinSemiLattice (Op a) where - Op x \/ Op y = Op (x /\ y) - -instance JoinSemiLattice a => MeetSemiLattice (Op a) where - Op x /\ Op y = Op (x \/ y) - -instance Lattice a => Lattice (Op a) where - -instance BoundedMeetSemiLattice a => BoundedJoinSemiLattice (Op a) where - bottom = Op top - -instance BoundedJoinSemiLattice a => BoundedMeetSemiLattice (Op a) where - top = Op bottom - -instance BoundedLattice a => BoundedLattice (Op a) where - -instance PartialOrd a => PartialOrd (Op a) where - Op a `leq` Op b = b `leq` a -- Note swap. - comparable (Op a) (Op b) = comparable a b diff --git a/Algebra/Lattice/Ordered.hs b/Algebra/Lattice/Ordered.hs deleted file mode 100644 --- a/Algebra/Lattice/Ordered.hs +++ /dev/null @@ -1,84 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE DeriveDataTypeable #-} -#if __GLASGOW_HASKELL__ < 709 -{-# LANGUAGE Trustworthy #-} -#else -{-# LANGUAGE Safe #-} -#endif ----------------------------------------------------------------------------- --- | --- Module : Algebra.Lattice.Ordered --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- -module Algebra.Lattice.Ordered ( - Ordered(..) - ) where - -import Prelude () -import Prelude.Compat - -import Algebra.Lattice -import Algebra.PartialOrd - -import Control.DeepSeq -import Control.Monad -import Data.Data -import Data.Hashable -import GHC.Generics - --- --- Ordered --- - --- | A total order gives rise to a lattice. Join is --- max, meet is min. -newtype Ordered a = Ordered { getOrdered :: a } - deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable -#if __GLASGOW_HASKELL__ >= 706 - , Generic1 -#endif - ) - -instance Applicative Ordered where - pure = return - (<*>) = ap - -instance Monad Ordered where - return = Ordered - Ordered x >>= f = f x - -instance NFData a => NFData (Ordered a) where - rnf (Ordered a) = rnf a - -instance Hashable a => Hashable (Ordered a) - -instance Ord a => JoinSemiLattice (Ordered a) where - Ordered x \/ Ordered y = Ordered (max x y) - -instance Ord a => MeetSemiLattice (Ordered a) where - Ordered x /\ Ordered y = Ordered (min x y) - -instance Ord a => Lattice (Ordered a) where - -instance (Ord a, Bounded a) => BoundedJoinSemiLattice (Ordered a) where - bottom = Ordered minBound - -instance (Ord a, Bounded a) => BoundedMeetSemiLattice (Ordered a) where - top = Ordered maxBound - -instance (Ord a, Bounded a) => BoundedLattice (Ordered a) where - -instance Ord a => PartialOrd (Ordered a) where - leq = (<=) - comparable _ _ = True diff --git a/Algebra/PartialOrd.hs b/Algebra/PartialOrd.hs deleted file mode 100644 --- a/Algebra/PartialOrd.hs +++ /dev/null @@ -1,147 +0,0 @@ -{-# LANGUAGE Safe #-} ----------------------------------------------------------------------------- --- | --- Module : Algebra.PartialOrd --- Copyright : (C) 2010-2015 Maximilian Bolingbroke --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- -module Algebra.PartialOrd ( - -- * Partial orderings - PartialOrd(..), - partialOrdEq, - - -- * Fixed points of chains in partial orders - lfpFrom, unsafeLfpFrom, - gfpFrom, unsafeGfpFrom - ) where - -import qualified Data.IntMap as IM -import qualified Data.IntSet as IS -import qualified Data.Map as M -import qualified Data.Set as S - --- | A partial ordering on sets --- () is a set equipped --- with a binary relation, `leq`, that obeys the following laws --- --- @ --- Reflexive: a ``leq`` a --- Antisymmetric: a ``leq`` b && b ``leq`` a ==> a == b --- Transitive: a ``leq`` b && b ``leq`` c ==> a ``leq`` c --- @ --- --- Two elements of the set are said to be `comparable` when they are are --- ordered with respect to the `leq` relation. So --- --- @ --- `comparable` a b ==> a ``leq`` b || b ``leq`` a --- @ --- --- If `comparable` always returns true then the relation `leq` defines a --- total ordering (and an `Ord` instance may be defined). Any `Ord` instance is --- trivially an instance of `PartialOrd`. 'Algebra.Lattice.Ordered' provides a --- convenient wrapper to satisfy 'PartialOrd' given 'Ord'. --- --- As an example consider the partial ordering on sets induced by set --- inclusion. Then for sets `a` and `b`, --- --- @ --- a ``leq`` b --- @ --- --- is true when `a` is a subset of `b`. Two sets are `comparable` if one is a --- subset of the other. Concretely --- --- @ --- a = {1, 2, 3} --- b = {1, 3, 4} --- c = {1, 2} --- --- a ``leq`` a = `True` --- a ``leq`` b = `False` --- a ``leq`` c = `False` --- b ``leq`` a = `False` --- b ``leq`` b = `True` --- b ``leq`` c = `False` --- c ``leq`` a = `True` --- c ``leq`` b = `False` --- c ``leq`` c = `True` --- --- `comparable` a b = `False` --- `comparable` a c = `True` --- `comparable` b c = `False` --- @ -class Eq a => PartialOrd a where - -- | The relation that induces the partial ordering - leq :: a -> a -> Bool - - -- | Whether two elements are ordered with respect to the relation. A - -- default implementation is given by - -- - -- > comparable x y = leq x y || leq y x - comparable :: a -> a -> Bool - comparable x y = leq x y || leq y x - --- | The equality relation induced by the partial-order structure. It must obey --- the laws --- @ --- Reflexive: a == a --- Transitive: a == b && b == c ==> a == c --- @ -partialOrdEq :: PartialOrd a => a -> a -> Bool -partialOrdEq x y = leq x y && leq y x - -instance Ord a => PartialOrd (S.Set a) where - leq = S.isSubsetOf - -instance PartialOrd IS.IntSet where - leq = IS.isSubsetOf - -instance (Ord k, PartialOrd v) => PartialOrd (M.Map k v) where - leq = M.isSubmapOfBy leq - -instance PartialOrd v => PartialOrd (IM.IntMap v) where - leq = IM.isSubmapOfBy leq - -instance (PartialOrd a, PartialOrd b) => PartialOrd (a, b) where - -- NB: *not* a lexical ordering. This is because for some component partial orders, lexical - -- ordering is incompatible with the transitivity axiom we require for the derived partial order - (x1, y1) `leq` (x2, y2) = x1 `leq` x2 && y1 `leq` y2 - --- | Least point of a partially ordered monotone function. Checks that the function is monotone. -lfpFrom :: PartialOrd a => a -> (a -> a) -> a -lfpFrom = lfpFrom' leq - --- | Least point of a partially ordered monotone function. Does not checks that the function is monotone. -unsafeLfpFrom :: Eq a => a -> (a -> a) -> a -unsafeLfpFrom = lfpFrom' (\_ _ -> True) - -{-# INLINE lfpFrom' #-} -lfpFrom' :: Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a -lfpFrom' check init_x f = go init_x - where go x | x' == x = x - | x `check` x' = go x' - | otherwise = error "lfpFrom: non-monotone function" - where x' = f x - - --- | Greatest fixed point of a partially ordered antinone function. Checks that the function is antinone. -{-# INLINE gfpFrom #-} -gfpFrom :: PartialOrd a => a -> (a -> a) -> a -gfpFrom = gfpFrom' leq - --- | Greatest fixed point of a partially ordered antinone function. Does not check that the function is antinone. -{-# INLINE unsafeGfpFrom #-} -unsafeGfpFrom :: Eq a => a -> (a -> a) -> a -unsafeGfpFrom = gfpFrom' (\_ _ -> True) - -{-# INLINE gfpFrom' #-} -gfpFrom' :: Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a -gfpFrom' check init_x f = go init_x - where go x | x' == x = x - | x' `check` x = go x' - | otherwise = error "gfpFrom: non-antinone function" - where x' = f x diff --git a/Algebra/PartialOrd/Instances.hs b/Algebra/PartialOrd/Instances.hs deleted file mode 100644 --- a/Algebra/PartialOrd/Instances.hs +++ /dev/null @@ -1,22 +0,0 @@ -{-# LANGUAGE Safe #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} ----------------------------------------------------------------------------- --- | --- Module : Algebra.PartialOrd.Instances --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- --- This module re-exports orphan instances from 'Data.Universe.Instances.Eq' --- module, and @(PartialOrd v, Finite k) => PartialOrd (k -> v)@ instance. ----------------------------------------------------------------------------- -module Algebra.PartialOrd.Instances () where - -import Algebra.PartialOrd (PartialOrd(..)) -import Data.Universe.Class (Finite(..)) -import Data.Universe.Instances.Eq () - --- | @Eq (k -> v)@ is from 'Data.Universe.Instances.Eq' -instance (PartialOrd v, Finite k) => PartialOrd (k -> v) where - f `leq` g = all (\k -> f k `leq` g k) universeF diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,11 @@ +# 1.7 (2017-10-01) + +- `HashMap` instances changed +- `PartialOrd Meet` and `Join` +- `PartialOrd ()` and `Void` +- `BoundedLattice (HashSet a)` +- `PartialOrd [a]` (`leq = isInfixOf`) + # 1.6.0 (2017-06-26) - Correct PartialOrd Map and IntMap instances diff --git a/lattices.cabal b/lattices.cabal --- a/lattices.cabal +++ b/lattices.cabal @@ -1,5 +1,5 @@ name: lattices -version: 1.6.0 +version: 1.7 cabal-version: >= 1.10 category: Math license: BSD3 @@ -49,6 +49,7 @@ semigroupoids >= 5.2 && < 5.3, universe-base >= 1.0 && < 1.1, universe-reverse-instances >= 1.0 && < 1.1 + hs-source-dirs: src ghc-options: -Wall default-language: Haskell2010 diff --git a/src/Algebra/Enumerable.hs b/src/Algebra/Enumerable.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Enumerable.hs @@ -0,0 +1,50 @@ +{-# LANGUAGE Safe #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Enumerable +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Enumerable {-# DEPRECATED "Use Data.Universe.Class" #-} ( + Enumerable(..), universeBounded, + Enumerated(..) + ) where + +-- | Finitely enumerable things +class Enumerable a where + universe :: [a] + +universeBounded :: (Enum a, Bounded a) => [a] +universeBounded = enumFromTo minBound maxBound + + +-- | Wrapper used to mark where we expect to use the fact that something is Enumerable +newtype Enumerated a = Enumerated { unEnumerated :: a } + deriving (Eq, Ord) + +instance Enumerable a => Enumerable (Enumerated a) where + universe = map Enumerated universe + + +-- TODO: add to this rather sorry little set of instances. Can we exploit commonality with lazy-smallcheck? + +instance Enumerable Bool where + universe = universeBounded + +instance Enumerable Int where + universe = universeBounded + +instance Enumerable a => Enumerable (Maybe a) where + universe = Nothing : map Just universe + +instance (Enumerable a, Enumerable b) => Enumerable (Either a b) where + universe = map Left universe ++ map Right universe + +instance Enumerable () where + universe = [()] + +instance (Enumerable a, Enumerable b) => Enumerable (a, b) where + universe = [(a, b) | a <- universe, b <- universe] diff --git a/src/Algebra/Lattice.hs b/src/Algebra/Lattice.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice.hs @@ -0,0 +1,584 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleInstances #-} +#if __GLASGOW_HASKELL__ >=710 && MIN_VERSION_unordered_containers(0,2,6) +{-# LANGUAGE Safe #-} +#else +{-# LANGUAGE Trustworthy #-} +#endif +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} +#if __GLASGOW_HASKELL__ >= 707 && __GLASGOW_HASKELL__ < 709 +{-# OPTIONS_GHC -fno-warn-amp #-} +#endif +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +-- In mathematics, a lattice is a partially ordered set in which every +-- two elements have a unique supremum (also called a least upper bound +-- or @join@) and a unique infimum (also called a greatest lower bound or +-- @meet@). +-- +-- In this module lattices are defined using 'meet' and 'join' operators, +-- as it's constructive one. +-- +---------------------------------------------------------------------------- +module Algebra.Lattice ( + -- * Unbounded lattices + JoinSemiLattice(..), MeetSemiLattice(..), Lattice, + joinLeq, joins1, meetLeq, meets1, + + -- * Bounded lattices + BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..), BoundedLattice, + joins, meets, + fromBool, + + -- * Monoid wrappers + Meet(..), Join(..), + + -- * Fixed points of chains in lattices + lfp, lfpFrom, unsafeLfp, + gfp, gfpFrom, unsafeGfp, + ) where + +import Prelude () +import Prelude.Compat + +import qualified Algebra.PartialOrd as PO + +import Data.Universe.Class (Finite (..), Universe (..)) + +import Control.Monad.Zip (MonadZip (..)) +import Data.Data (Data, Typeable) +import Data.Hashable (Hashable (..)) +import Data.Proxy (Proxy (..)) +import Data.Semigroup (All (..), Any (..), Endo (..), Semigroup (..)) +import Data.Tagged (Tagged (..)) +import Data.Void (Void) +import GHC.Generics (Generic) + +import qualified Data.IntMap as IM +import qualified Data.IntSet as IS +import qualified Data.Map as M +import qualified Data.Set as S + +import qualified Data.HashMap.Lazy as HM +import qualified Data.HashSet as HS + +import Control.Applicative (Const (..)) +import Data.Functor.Identity (Identity (..)) +import Data.Semigroup.Foldable (Foldable1 (..)) + +infixr 6 /\ -- This comment needed because of CPP +infixr 5 \/ + +-- | A algebraic structure with element joins: +-- +-- > Associativity: x \/ (y \/ z) == (x \/ y) \/ z +-- > Commutativity: x \/ y == y \/ x +-- > Idempotency: x \/ x == x +class JoinSemiLattice a where + (\/) :: a -> a -> a + (\/) = join + + join :: a -> a -> a + join = (\/) + +#if __GLASGOW_HASKELL__ >= 707 + {-# MINIMAL (\/) | join #-} +#endif +{-# DEPRECATED join "Use '\\/' infix operator" #-} + +-- | The partial ordering induced by the join-semilattice structure +joinLeq :: (Eq a, JoinSemiLattice a) => a -> a -> Bool +joinLeq x y = (x \/ y) == y + +-- | A algebraic structure with element meets: +-- +-- > Associativity: x /\ (y /\ z) == (x /\ y) /\ z +-- > Commutativity: x /\ y == y /\ x +-- > Idempotency: x /\ x == x +class MeetSemiLattice a where + (/\) :: a -> a -> a + (/\) = meet + + meet :: a -> a -> a + meet = (/\) + +#if __GLASGOW_HASKELL__ >= 707 + {-# MINIMAL (/\) | meet #-} +#endif +{-# DEPRECATED meet "Use '/\\' infix operator" #-} + +-- | The partial ordering induced by the meet-semilattice structure +meetLeq :: (Eq a, MeetSemiLattice a) => a -> a -> Bool +meetLeq x y = (x /\ y) == x + + + +-- | The combination of two semi lattices makes a lattice if the absorption law holds: +-- see and +-- +-- > Absorption: a \/ (a /\ b) == a /\ (a \/ b) == a +class (JoinSemiLattice a, MeetSemiLattice a) => Lattice a where + +-- | A join-semilattice with some element |bottom| that \/ approaches. +-- +-- > Identity: x \/ bottom == x +class JoinSemiLattice a => BoundedJoinSemiLattice a where + bottom :: a + +-- | The join of a list of join-semilattice elements +joins :: (BoundedJoinSemiLattice a, Foldable f) => f a -> a +joins = getJoin . foldMap Join + +-- | The join of at a list of join-semilattice elements (of length at least one) +joins1 :: (JoinSemiLattice a, Foldable1 f) => f a -> a +joins1 = getJoin . foldMap1 Join + +-- | A meet-semilattice with some element |top| that /\ approaches. +-- +-- > Identity: x /\ top == x +class MeetSemiLattice a => BoundedMeetSemiLattice a where + top :: a + +-- | The meet of a list of meet-semilattice elements +meets :: (BoundedMeetSemiLattice a, Foldable f) => f a -> a +meets = getMeet . foldMap Meet +-- +-- | The meet of at a list of meet-semilattice elements (of length at least one) +meets1 :: (MeetSemiLattice a, Foldable1 f) => f a -> a +meets1 = getMeet . foldMap1 Meet + +-- | Lattices with both bounds +class (Lattice a, BoundedJoinSemiLattice a, BoundedMeetSemiLattice a) => BoundedLattice a where + +-- | 'True' to 'top' and 'False' to 'bottom' +fromBool :: BoundedLattice a => Bool -> a +fromBool True = top +fromBool False = bottom + +-- +-- Sets +-- + +instance Ord a => JoinSemiLattice (S.Set a) where + (\/) = S.union + +instance Ord a => MeetSemiLattice (S.Set a) where + (/\) = S.intersection + +instance Ord a => Lattice (S.Set a) + +instance Ord a => BoundedJoinSemiLattice (S.Set a) where + bottom = S.empty + +instance (Ord a, Finite a) => BoundedMeetSemiLattice (S.Set a) where + top = S.fromList universeF + +instance (Ord a, Finite a) => BoundedLattice (S.Set a) + +-- +-- IntSets +-- + +instance JoinSemiLattice IS.IntSet where + (\/) = IS.union + +instance MeetSemiLattice IS.IntSet where + (/\) = IS.intersection + +instance Lattice IS.IntSet + +instance BoundedJoinSemiLattice IS.IntSet where + bottom = IS.empty + +-- +-- HashSet +-- + +instance (Eq a, Hashable a) => JoinSemiLattice (HS.HashSet a) where + (\/) = HS.union + +instance (Eq a, Hashable a) => MeetSemiLattice (HS.HashSet a) where + (/\) = HS.intersection + +instance (Eq a, Hashable a) => Lattice (HS.HashSet a) + +instance (Eq a, Hashable a) => BoundedJoinSemiLattice (HS.HashSet a) where + bottom = HS.empty + +instance (Eq a, Hashable a, Finite a) => BoundedMeetSemiLattice (HS.HashSet a) where + top = HS.fromList universeF + +instance (Eq a, Hashable a, Finite a) => BoundedLattice (HS.HashSet a) + +-- +-- Maps +-- + +instance (Ord k, JoinSemiLattice v) => JoinSemiLattice (M.Map k v) where + (\/) = M.unionWith (\/) + +instance (Ord k, MeetSemiLattice v) => MeetSemiLattice (M.Map k v) where + (/\) = M.intersectionWith (/\) + +instance (Ord k, Lattice v) => Lattice (M.Map k v) where + +instance (Ord k, JoinSemiLattice v) => BoundedJoinSemiLattice (M.Map k v) where + bottom = M.empty + +instance (Ord k, Finite k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (M.Map k v) where + top = M.fromList (universeF `zip` repeat top) + +instance (Ord k, Finite k, BoundedLattice v) => BoundedLattice (M.Map k v) where + +-- +-- IntMaps +-- + +instance JoinSemiLattice v => JoinSemiLattice (IM.IntMap v) where + (\/) = IM.unionWith (\/) + +instance JoinSemiLattice v => BoundedJoinSemiLattice (IM.IntMap v) where + bottom = IM.empty + +instance MeetSemiLattice v => MeetSemiLattice (IM.IntMap v) where + (/\) = IM.intersectionWith (/\) + +instance Lattice v => Lattice (IM.IntMap v) + + +-- +-- HashMaps +-- + +instance (Eq k, Hashable k, JoinSemiLattice v) => JoinSemiLattice (HM.HashMap k v) where + (\/) = HM.unionWith (\/) + +instance (Eq k, Hashable k, MeetSemiLattice v) => MeetSemiLattice (HM.HashMap k v) where + (/\) = HM.intersectionWith (/\) + +instance (Eq k, Hashable k, JoinSemiLattice v) => BoundedJoinSemiLattice (HM.HashMap k v) where + bottom = HM.empty + +instance (Eq k, Hashable k, Lattice v) => Lattice (HM.HashMap k v) where + +instance (Eq k, Hashable k, Finite k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (HM.HashMap k v) where + top = HM.fromList (universeF `zip` repeat top) + +instance (Eq k, Hashable k, Finite k, BoundedLattice v) => BoundedLattice (HM.HashMap k v) where + +-- +-- Functions +-- + +instance JoinSemiLattice v => JoinSemiLattice (k -> v) where + f \/ g = \x -> f x \/ g x + +instance MeetSemiLattice v => MeetSemiLattice (k -> v) where + f /\ g = \x -> f x /\ g x + +instance Lattice v => Lattice (k -> v) where + +instance BoundedJoinSemiLattice v => BoundedJoinSemiLattice (k -> v) where + bottom = const bottom + +instance BoundedMeetSemiLattice v => BoundedMeetSemiLattice (k -> v) where + top = const top + +instance BoundedLattice v => BoundedLattice (k -> v) where + +-- Unit +instance JoinSemiLattice () where + _ \/ _ = () + +instance BoundedJoinSemiLattice () where + bottom = () + +instance MeetSemiLattice () where + _ /\ _ = () + +instance BoundedMeetSemiLattice () where + top = () + +instance Lattice () where +instance BoundedLattice () where + +-- +-- Tuples +-- + +instance (JoinSemiLattice a, JoinSemiLattice b) => JoinSemiLattice (a, b) where + (x1, y1) \/ (x2, y2) = (x1 \/ x2, y1 \/ y2) + +instance (MeetSemiLattice a, MeetSemiLattice b) => MeetSemiLattice (a, b) where + (x1, y1) /\ (x2, y2) = (x1 /\ x2, y1 /\ y2) + +instance (Lattice a, Lattice b) => Lattice (a, b) where + +instance (BoundedJoinSemiLattice a, BoundedJoinSemiLattice b) => BoundedJoinSemiLattice (a, b) where + bottom = (bottom, bottom) + +instance (BoundedMeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (a, b) where + top = (top, top) + +instance (BoundedLattice a, BoundedLattice b) => BoundedLattice (a, b) where + +-- +-- Bools +-- + +instance JoinSemiLattice Bool where + (\/) = (||) + +instance MeetSemiLattice Bool where + (/\) = (&&) + +instance Lattice Bool where + +instance BoundedJoinSemiLattice Bool where + bottom = False + +instance BoundedMeetSemiLattice Bool where + top = True + +instance BoundedLattice Bool where + +--- Monoids + +-- | Monoid wrapper for JoinSemiLattice +newtype Join a = Join { getJoin :: a } + deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic) + +instance JoinSemiLattice a => Semigroup (Join a) where + Join a <> Join b = Join (a \/ b) + +instance BoundedJoinSemiLattice a => Monoid (Join a) where + mempty = Join bottom + Join a `mappend` Join b = Join (a \/ b) + +instance (Eq a, JoinSemiLattice a) => PO.PartialOrd (Join a) where + leq (Join a) (Join b) = joinLeq a b + +instance Functor Join where + fmap f (Join x) = Join (f x) + +instance Applicative Join where + pure = Join + Join f <*> Join x = Join (f x) + _ *> x = x + +instance Monad Join where + return = pure + Join m >>= f = f m + (>>) = (*>) + +instance MonadZip Join where + mzip (Join x) (Join y) = Join (x, y) + +instance Universe a => Universe (Join a) where + universe = fmap Join universe + +instance Finite a => Finite (Join a) where + universeF = fmap Join universeF + +-- | Monoid wrapper for MeetSemiLattice +newtype Meet a = Meet { getMeet :: a } + deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic) + +instance MeetSemiLattice a => Semigroup (Meet a) where + Meet a <> Meet b = Meet (a /\ b) + +instance BoundedMeetSemiLattice a => Monoid (Meet a) where + mempty = Meet top + Meet a `mappend` Meet b = Meet (a /\ b) + +instance (Eq a, MeetSemiLattice a) => PO.PartialOrd (Meet a) where + leq (Meet a) (Meet b) = meetLeq a b + +instance Functor Meet where + fmap f (Meet x) = Meet (f x) + +instance Applicative Meet where + pure = Meet + Meet f <*> Meet x = Meet (f x) + _ *> x = x + +instance Monad Meet where + return = pure + Meet m >>= f = f m + (>>) = (*>) + +instance MonadZip Meet where + mzip (Meet x) (Meet y) = Meet (x, y) + +instance Universe a => Universe (Meet a) where + universe = fmap Meet universe + +instance Finite a => Finite (Meet a) where + universeF = fmap Meet universeF + +-- All +instance JoinSemiLattice All where + All a \/ All b = All $ a \/ b + +instance BoundedJoinSemiLattice All where + bottom = All False + +instance MeetSemiLattice All where + All a /\ All b = All $ a /\ b + +instance BoundedMeetSemiLattice All where + top = All True + +instance Lattice All where +instance BoundedLattice All where + +-- Any +instance JoinSemiLattice Any where + Any a \/ Any b = Any $ a \/ b + +instance BoundedJoinSemiLattice Any where + bottom = Any False + +instance MeetSemiLattice Any where + Any a /\ Any b = Any $ a /\ b + +instance BoundedMeetSemiLattice Any where + top = Any True + +instance Lattice Any where +instance BoundedLattice Any where + +-- Endo +instance JoinSemiLattice a => JoinSemiLattice (Endo a) where + Endo a \/ Endo b = Endo $ a \/ b + +instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Endo a) where + bottom = Endo bottom + +instance MeetSemiLattice a => MeetSemiLattice (Endo a) where + Endo a /\ Endo b = Endo $ a /\ b + +instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Endo a) where + top = Endo top + +instance Lattice a => Lattice (Endo a) where +instance BoundedLattice a => BoundedLattice (Endo a) where + +-- Tagged +instance JoinSemiLattice a => JoinSemiLattice (Tagged t a) where + Tagged a \/ Tagged b = Tagged $ a \/ b + +instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Tagged t a) where + bottom = Tagged bottom + +instance MeetSemiLattice a => MeetSemiLattice (Tagged t a) where + Tagged a /\ Tagged b = Tagged $ a /\ b + +instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Tagged t a) where + top = Tagged top + +instance Lattice a => Lattice (Tagged t a) where +instance BoundedLattice a => BoundedLattice (Tagged t a) where + +-- Proxy +instance JoinSemiLattice (Proxy a) where + _ \/ _ = Proxy + +instance BoundedJoinSemiLattice (Proxy a) where + bottom = Proxy + +instance MeetSemiLattice (Proxy a) where + _ /\ _ = Proxy + +instance BoundedMeetSemiLattice (Proxy a) where + top = Proxy + +instance Lattice (Proxy a) where +instance BoundedLattice (Proxy a) where + +#if MIN_VERSION_base(4,8,0) +-- Identity +instance JoinSemiLattice a => JoinSemiLattice (Identity a) where + Identity a \/ Identity b = Identity (a \/ b) + +instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Identity a) where + bottom = Identity bottom + +instance MeetSemiLattice a => MeetSemiLattice (Identity a) where + Identity a /\ Identity b = Identity (a /\ b) + +instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Identity a) where + top = Identity top + +instance Lattice a => Lattice (Identity a) where +instance BoundedLattice a => BoundedLattice (Identity a) where +#endif + +-- Const +instance JoinSemiLattice a => JoinSemiLattice (Const a b) where + Const a \/ Const b = Const (a \/ b) + +instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Const a b) where + bottom = Const bottom + +instance MeetSemiLattice a => MeetSemiLattice (Const a b) where + Const a /\ Const b = Const (a /\ b) + +instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Const a b) where + top = Const top + +instance Lattice a => Lattice (Const a b) where +instance BoundedLattice a => BoundedLattice (Const a b) where + +-- Void +instance JoinSemiLattice Void where + a \/ _ = a + +instance MeetSemiLattice Void where + a /\ _ = a + +instance Lattice Void where + +-- | Implementation of Kleene fixed-point theorem . +-- Assumes that the function is monotone and does not check if that is correct. +{-# INLINE unsafeLfp #-} +unsafeLfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a +unsafeLfp = PO.unsafeLfpFrom bottom + +-- | Implementation of Kleene fixed-point theorem . +-- Forces the function to be monotone. +{-# INLINE lfp #-} +lfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a +lfp = lfpFrom bottom + +-- | Implementation of Kleene fixed-point theorem . +-- Forces the function to be monotone. +{-# INLINE lfpFrom #-} +lfpFrom :: (Eq a, BoundedJoinSemiLattice a) => a -> (a -> a) -> a +lfpFrom init_x f = PO.unsafeLfpFrom init_x (\x -> f x \/ x) + + +-- | Implementation of Kleene fixed-point theorem . +-- Assumes that the function is antinone and does not check if that is correct. +{-# INLINE unsafeGfp #-} +unsafeGfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a +unsafeGfp = PO.unsafeGfpFrom top + +-- | Implementation of Kleene fixed-point theorem . +-- Forces the function to be antinone. +{-# INLINE gfp #-} +gfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a +gfp = gfpFrom top + +-- | Implementation of Kleene fixed-point theorem . +-- Forces the function to be antinone. +{-# INLINE gfpFrom #-} +gfpFrom :: (Eq a, BoundedMeetSemiLattice a) => a -> (a -> a) -> a +gfpFrom init_x f = PO.unsafeGfpFrom init_x (\x -> f x /\ x) diff --git a/src/Algebra/Lattice/Divisibility.hs b/src/Algebra/Lattice/Divisibility.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Divisibility.hs @@ -0,0 +1,76 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeOperators #-} +#if __GLASGOW_HASKELL__ < 709 +{-# LANGUAGE Trustworthy #-} +#else +{-# LANGUAGE Safe #-} +#endif +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.Divisibility +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Divisibility ( + Divisibility(..) + ) where + +import Prelude () +import Prelude.Compat + +import Algebra.Lattice +import Algebra.PartialOrd + +import Control.DeepSeq +import Control.Monad +import Data.Data +import Data.Hashable +import GHC.Generics + +-- +-- Divisibility +-- + +-- | A divisibility lattice. @'join' = 'lcm'@, @'meet' = 'gcd'@. +newtype Divisibility a = Divisibility { getDivisibility :: a } + deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable +#if __GLASGOW_HASKELL__ >= 706 + , Generic1 +#endif + ) + +instance Applicative Divisibility where + pure = return + (<*>) = ap + +instance Monad Divisibility where + return = Divisibility + Divisibility x >>= f = f x + +instance NFData a => NFData (Divisibility a) where + rnf (Divisibility a) = rnf a + +instance Hashable a => Hashable (Divisibility a) + +instance Integral a => JoinSemiLattice (Divisibility a) where + Divisibility x \/ Divisibility y = Divisibility (lcm x y) + +instance Integral a => MeetSemiLattice (Divisibility a) where + Divisibility x /\ Divisibility y = Divisibility (gcd x y) + +instance Integral a => Lattice (Divisibility a) where + +instance Integral a => BoundedJoinSemiLattice (Divisibility a) where + bottom = Divisibility 1 + +instance (Eq a, Integral a) => PartialOrd (Divisibility a) where + leq (Divisibility a) (Divisibility b) = b `mod` a == 0 diff --git a/src/Algebra/Lattice/Dropped.hs b/src/Algebra/Lattice/Dropped.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Dropped.hs @@ -0,0 +1,91 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeOperators #-} +#if __GLASGOW_HASKELL__ < 709 +{-# LANGUAGE Trustworthy #-} +#else +{-# LANGUAGE Safe #-} +#endif +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.Dropped +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Dropped ( + Dropped(..) + , retractDropped + ) where + +import Prelude () +import Prelude.Compat + +import Algebra.Lattice + +import Control.DeepSeq +import Control.Monad +import Data.Data +import Data.Hashable +import GHC.Generics + +-- +-- Dropped +-- + +-- | Graft a distinct top onto an otherwise unbounded lattice. +-- As a bonus, the top will be an absorbing element for the join. +data Dropped a = Top + | Drop a + deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable +#if __GLASGOW_HASKELL__ >= 706 + , Generic1 +#endif + ) + +instance Applicative Dropped where + pure = return + (<*>) = ap + +instance Monad Dropped where + return = Drop + Top >>= _ = Top + Drop x >>= f = f x + +instance NFData a => NFData (Dropped a) where + rnf Top = () + rnf (Drop a) = rnf a + +instance Hashable a => Hashable (Dropped a) + +instance JoinSemiLattice a => JoinSemiLattice (Dropped a) where + Top \/ _ = Top + _ \/ Top = Top + Drop x \/ Drop y = Drop (x \/ y) + +instance MeetSemiLattice a => MeetSemiLattice (Dropped a) where + Top /\ drop_y = drop_y + drop_x /\ Top = drop_x + Drop x /\ Drop y = Drop (x /\ y) + +instance Lattice a => Lattice (Dropped a) where + +instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Dropped a) where + bottom = Drop bottom + +instance MeetSemiLattice a => BoundedMeetSemiLattice (Dropped a) where + top = Top + +instance BoundedLattice a => BoundedLattice (Dropped a) where + +-- | Interpret @'Dropped' a@ using the 'BoundedMeetSemiLattice' of @a@. +retractDropped :: BoundedMeetSemiLattice a => Dropped a -> a +retractDropped Top = top +retractDropped (Drop x) = x diff --git a/src/Algebra/Lattice/Free.hs b/src/Algebra/Lattice/Free.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Free.hs @@ -0,0 +1,148 @@ +{-# LANGUAGE RankNTypes #-} + +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.Free +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- + +module Algebra.Lattice.Free + ( -- * Free join-semilattices + FreeJoinSemiLattice + , liftFreeJoinSemiLattice + , lowerFreeJoinSemiLattice + , retractFreeJoinSemiLattice + + -- * Free meet-semilattices + , FreeMeetSemiLattice + , liftFreeMeetSemiLattice + , lowerFreeMeetSemiLattice + , retractFreeMeetSemiLattice + + -- * Free lattices + , FreeLattice + , liftFreeLattice + , lowerFreeLattice + , retractFreeLattice + ) where + +import Prelude () +import Prelude.Compat + +import Algebra.Lattice +import Data.Universe.Class + +-- +-- Free join-semilattices +-- + +newtype FreeJoinSemiLattice a = FreeJoinSemiLattice + { lowerFreeJoinSemiLattice :: forall b. JoinSemiLattice b => + (a -> b) -> b + } + +liftFreeJoinSemiLattice :: a -> FreeJoinSemiLattice a +liftFreeJoinSemiLattice a = FreeJoinSemiLattice (\inj -> inj a) + +retractFreeJoinSemiLattice :: JoinSemiLattice a => FreeJoinSemiLattice a -> a +retractFreeJoinSemiLattice a = lowerFreeJoinSemiLattice a id + +instance Functor FreeJoinSemiLattice where + fmap f (FreeJoinSemiLattice g) = FreeJoinSemiLattice (\inj -> g (inj . f)) + a <$ FreeJoinSemiLattice f = FreeJoinSemiLattice (\inj -> f (const (inj a))) + +instance JoinSemiLattice (FreeJoinSemiLattice a) where + FreeJoinSemiLattice f \/ FreeJoinSemiLattice g = + FreeJoinSemiLattice (\inj -> f inj \/ g inj) + +instance BoundedJoinSemiLattice a => + BoundedJoinSemiLattice (FreeJoinSemiLattice a) where + bottom = FreeJoinSemiLattice (\inj -> inj bottom) + +instance Universe a => Universe (FreeJoinSemiLattice a) where + universe = fmap liftFreeJoinSemiLattice universe + +instance Finite a => Finite (FreeJoinSemiLattice a) where + universeF = fmap liftFreeJoinSemiLattice universeF + + +-- +-- Free meet-semilattices +-- + +newtype FreeMeetSemiLattice a = FreeMeetSemiLattice + { lowerFreeMeetSemiLattice :: forall b. MeetSemiLattice b => + (a -> b) -> b + } + +instance Functor FreeMeetSemiLattice where + fmap f (FreeMeetSemiLattice g) = FreeMeetSemiLattice (\inj -> g (inj . f)) + a <$ FreeMeetSemiLattice f = FreeMeetSemiLattice (\inj -> f (const (inj a))) + +liftFreeMeetSemiLattice :: a -> FreeMeetSemiLattice a +liftFreeMeetSemiLattice a = FreeMeetSemiLattice (\inj -> inj a) + +retractFreeMeetSemiLattice :: MeetSemiLattice a => FreeMeetSemiLattice a -> a +retractFreeMeetSemiLattice a = lowerFreeMeetSemiLattice a id + +instance MeetSemiLattice (FreeMeetSemiLattice a) where + FreeMeetSemiLattice f /\ FreeMeetSemiLattice g = + FreeMeetSemiLattice (\inj -> f inj /\ g inj) + +instance BoundedMeetSemiLattice a => + BoundedMeetSemiLattice (FreeMeetSemiLattice a) where + top = FreeMeetSemiLattice (\inj -> inj top) + +instance Universe a => Universe (FreeMeetSemiLattice a) where + universe = fmap liftFreeMeetSemiLattice universe + +instance Finite a => Finite (FreeMeetSemiLattice a) where + universeF = fmap liftFreeMeetSemiLattice universeF + + +-- +-- Free lattices +-- + +newtype FreeLattice a = FreeLattice + { lowerFreeLattice :: forall b. Lattice b => + (a -> b) -> b + } + +instance Functor FreeLattice where + fmap f (FreeLattice g) = FreeLattice (\inj -> g (inj . f)) + a <$ FreeLattice f = FreeLattice (\inj -> f (const (inj a))) + +liftFreeLattice :: a -> FreeLattice a +liftFreeLattice a = FreeLattice (\inj -> inj a) + +retractFreeLattice :: Lattice a => FreeLattice a -> a +retractFreeLattice a = lowerFreeLattice a id + +instance JoinSemiLattice (FreeLattice a) where + FreeLattice f \/ FreeLattice g = FreeLattice (\inj -> f inj \/ g inj) + +instance MeetSemiLattice (FreeLattice a) where + FreeLattice f /\ FreeLattice g = FreeLattice (\inj -> f inj /\ g inj) + +instance Lattice (FreeLattice a) + +instance BoundedJoinSemiLattice a => + BoundedJoinSemiLattice (FreeLattice a) where + bottom = FreeLattice (\inj -> inj bottom) + +instance BoundedMeetSemiLattice a => + BoundedMeetSemiLattice (FreeLattice a) where + top = FreeLattice (\inj -> inj top) + +instance BoundedLattice a => + BoundedLattice (FreeLattice a) + +instance Universe a => Universe (FreeLattice a) where + universe = fmap liftFreeLattice universe + +instance Finite a => Finite (FreeLattice a) where + universeF = fmap liftFreeLattice universeF diff --git a/src/Algebra/Lattice/Levitated.hs b/src/Algebra/Lattice/Levitated.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Levitated.hs @@ -0,0 +1,100 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeOperators #-} +#if __GLASGOW_HASKELL__ < 709 +{-# LANGUAGE Trustworthy #-} +#else +{-# LANGUAGE Safe #-} +#endif +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.Levitated +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Levitated ( + Levitated(..) + , retractLevitated + ) where + +import Prelude () +import Prelude.Compat + +import Algebra.Lattice + +import Control.DeepSeq +import Control.Monad +import Data.Data +import Data.Hashable +import GHC.Generics + +-- +-- Levitated +-- + +-- | Graft a distinct top and bottom onto an otherwise unbounded lattice. +-- The top is the absorbing element for the join, and the bottom is the absorbing +-- element for the meet. +data Levitated a = Top + | Levitate a + | Bottom + deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable +#if __GLASGOW_HASKELL__ >= 706 + , Generic1 +#endif + ) + +instance Applicative Levitated where + pure = return + (<*>) = ap + +instance Monad Levitated where + return = Levitate + Top >>= _ = Top + Bottom >>= _ = Bottom + Levitate x >>= f = f x + +instance NFData a => NFData (Levitated a) where + rnf Top = () + rnf Bottom = () + rnf (Levitate a) = rnf a + +instance Hashable a => Hashable (Levitated a) + +instance JoinSemiLattice a => JoinSemiLattice (Levitated a) where + Top \/ _ = Top + _ \/ Top = Top + Levitate x \/ Levitate y = Levitate (x \/ y) + Bottom \/ lev_y = lev_y + lev_x \/ Bottom = lev_x + +instance MeetSemiLattice a => MeetSemiLattice (Levitated a) where + Top /\ lev_y = lev_y + lev_x /\ Top = lev_x + Levitate x /\ Levitate y = Levitate (x /\ y) + Bottom /\ _ = Bottom + _ /\ Bottom = Bottom + +instance Lattice a => Lattice (Levitated a) where + +instance JoinSemiLattice a => BoundedJoinSemiLattice (Levitated a) where + bottom = Bottom + +instance MeetSemiLattice a => BoundedMeetSemiLattice (Levitated a) where + top = Top + +instance Lattice a => BoundedLattice (Levitated a) where + +-- | Interpret @'Levitated' a@ using the 'BoundedLattice' of @a@. +retractLevitated :: BoundedLattice a => Levitated a -> a +retractLevitated Top = top +retractLevitated Bottom = bottom +retractLevitated (Levitate x) = x diff --git a/src/Algebra/Lattice/Lexicographic.hs b/src/Algebra/Lattice/Lexicographic.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Lexicographic.hs @@ -0,0 +1,129 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeOperators #-} +#if __GLASGOW_HASKELL__ < 709 +{-# LANGUAGE Trustworthy #-} +#else +{-# LANGUAGE Safe #-} +#endif +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.Lexicographic +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Lexicographic ( + Lexicographic(..) + ) where + +import Prelude () +import Prelude.Compat + +import Algebra.Lattice +import Algebra.PartialOrd + +import Control.DeepSeq +import Control.Monad +import Data.Data +import Data.Hashable +import GHC.Generics + +-- +-- Lexicographic +-- + +-- | A pair lattice with a lexicographic ordering. This means in +-- a join the second component of the resulting pair is the second +-- component of the pair with the larger first component. If the +-- first components are equal, then the second components will be +-- joined. The meet is similar only it prefers the smaller first +-- component. +-- +-- An application of this type is versioning. For example, a +-- Last-Writer-Wins register would look like +-- 'Lexicographc (Ordered Timestamp) v' where the lattice +-- structure handles the, presumably rare, case of matching +-- 'Timestamps'. Typically this is done in an arbitary, but +-- deterministic manner. +data Lexicographic k v = Lexicographic !k !v + deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable +#if __GLASGOW_HASKELL__ >= 706 + , Generic1 +#endif + ) + +instance BoundedJoinSemiLattice k => Applicative (Lexicographic k) where + pure = return + (<*>) = ap + +-- Essentially the Writer monad. +instance BoundedJoinSemiLattice k => Monad (Lexicographic k) where + return = Lexicographic bottom + Lexicographic k v >>= f = + case f v of + Lexicographic k' v' -> Lexicographic (k \/ k') v' + +instance (NFData k, NFData v) => NFData (Lexicographic k v) where + rnf (Lexicographic k v) = rnf k `seq` rnf v + +instance (Hashable k, Hashable v) => Hashable (Lexicographic k v) + +-- Why we have 'bottom', and not @v1 \\/ v2@ in the @otherwise@ clause? +-- +-- For example what is the join of @(2, 1)@ and @(3, 2)@ +-- in lexicographic divisibility divisibility lattice. +-- +-- With @v1 \\/ v2@, we get the upper bound, but not least! +-- +-- @ +-- (2, 1) `leq` (6, 2) +-- (3, 2) `leq` (6, 2) +-- @ +-- +-- But @(6, 1) `leq` (6, 2)@, and +-- +-- @ +-- (2, 1) `leq` (6, 1) +-- (3, 2) `leq` (6, 1) +-- @ +-- +instance (PartialOrd k, JoinSemiLattice k, BoundedJoinSemiLattice v) => JoinSemiLattice (Lexicographic k v) where + l@(Lexicographic k1 v1) \/ r@(Lexicographic k2 v2) + | k1 == k2 = Lexicographic k1 (v1 \/ v2) + | k1 `leq` k2 = r + | k2 `leq` k1 = l + | otherwise = Lexicographic (k1 \/ k2) bottom + +instance (PartialOrd k, MeetSemiLattice k, BoundedMeetSemiLattice v) => MeetSemiLattice (Lexicographic k v) where + l@(Lexicographic k1 v1) /\ r@(Lexicographic k2 v2) + | k1 == k2 = Lexicographic k1 (v1 /\ v2) + | k1 `leq` k2 = l + | k2 `leq` k1 = r + | otherwise = Lexicographic (k1 /\ k2) top + +instance (PartialOrd k, Lattice k, BoundedLattice v) => Lattice (Lexicographic k v) where + +instance (PartialOrd k, BoundedJoinSemiLattice k, BoundedJoinSemiLattice v) => BoundedJoinSemiLattice (Lexicographic k v) where + bottom = Lexicographic bottom bottom + +instance (PartialOrd k, BoundedMeetSemiLattice k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (Lexicographic k v) where + top = Lexicographic top top + +instance (PartialOrd k, BoundedLattice k, BoundedLattice v) => BoundedLattice (Lexicographic k v) where + +instance (PartialOrd k, PartialOrd v) => PartialOrd (Lexicographic k v) where + Lexicographic k1 v1 `leq` Lexicographic k2 v2 + | k1 == k2 = v1 `leq` v2 + | k1 `leq` k2 = True + | otherwise = False -- Incomparable or k2 `leq` k1 + comparable (Lexicographic k1 v1) (Lexicographic k2 v2) + | k1 == k2 = comparable v1 v2 + | otherwise = comparable k1 k2 diff --git a/src/Algebra/Lattice/Lifted.hs b/src/Algebra/Lattice/Lifted.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Lifted.hs @@ -0,0 +1,91 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeOperators #-} +#if __GLASGOW_HASKELL__ < 709 +{-# LANGUAGE Trustworthy #-} +#else +{-# LANGUAGE Safe #-} +#endif +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.Lifted +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Lifted ( + Lifted(..) + , retractLifted + ) where + +import Prelude () +import Prelude.Compat + +import Algebra.Lattice + +import Control.DeepSeq +import Control.Monad +import Data.Data +import Data.Hashable +import GHC.Generics + +-- +-- Lifted +-- + +-- | Graft a distinct bottom onto an otherwise unbounded lattice. +-- As a bonus, the bottom will be an absorbing element for the meet. +data Lifted a = Lift a + | Bottom + deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable +#if __GLASGOW_HASKELL__ >= 706 + , Generic1 +#endif + ) + +instance Applicative Lifted where + pure = return + (<*>) = ap + +instance Monad Lifted where + return = Lift + Bottom >>= _ = Bottom + Lift x >>= f = f x + +instance NFData a => NFData (Lifted a) where + rnf Bottom = () + rnf (Lift a) = rnf a + +instance Hashable a => Hashable (Lifted a) + +instance JoinSemiLattice a => JoinSemiLattice (Lifted a) where + Lift x \/ Lift y = Lift (x \/ y) + Bottom \/ lift_y = lift_y + lift_x \/ Bottom = lift_x + +instance MeetSemiLattice a => MeetSemiLattice (Lifted a) where + Lift x /\ Lift y = Lift (x /\ y) + Bottom /\ _ = Bottom + _ /\ Bottom = Bottom + +instance Lattice a => Lattice (Lifted a) where + +instance JoinSemiLattice a => BoundedJoinSemiLattice (Lifted a) where + bottom = Bottom + +instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Lifted a) where + top = Lift top + +instance BoundedLattice a => BoundedLattice (Lifted a) where + +-- | Interpret @'Lifted' a@ using the 'BoundedJoinSemiLattice' of @a@. +retractLifted :: BoundedJoinSemiLattice a => Lifted a -> a +retractLifted Bottom = bottom +retractLifted (Lift x) = x diff --git a/src/Algebra/Lattice/Op.hs b/src/Algebra/Lattice/Op.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Op.hs @@ -0,0 +1,83 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeOperators #-} +#if __GLASGOW_HASKELL__ < 709 +{-# LANGUAGE Trustworthy #-} +#else +{-# LANGUAGE Safe #-} +#endif +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.Op +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Op ( + Op(..) + ) where + +import Prelude () +import Prelude.Compat + +import Algebra.Lattice +import Algebra.PartialOrd + +import Control.DeepSeq +import Control.Monad +import Data.Data +import Data.Hashable +import GHC.Generics + +-- +-- Op +-- + +-- | The opposite lattice of a given lattice. That is, switch +-- meets and joins. +newtype Op a = Op { getOp :: a } + deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable +#if __GLASGOW_HASKELL__ >= 706 + , Generic1 +#endif + ) + +instance Applicative Op where + pure = return + (<*>) = ap + +instance Monad Op where + return = Op + Op x >>= f = f x + +instance NFData a => NFData (Op a) where + rnf (Op a) = rnf a + +instance Hashable a => Hashable (Op a) + +instance MeetSemiLattice a => JoinSemiLattice (Op a) where + Op x \/ Op y = Op (x /\ y) + +instance JoinSemiLattice a => MeetSemiLattice (Op a) where + Op x /\ Op y = Op (x \/ y) + +instance Lattice a => Lattice (Op a) where + +instance BoundedMeetSemiLattice a => BoundedJoinSemiLattice (Op a) where + bottom = Op top + +instance BoundedJoinSemiLattice a => BoundedMeetSemiLattice (Op a) where + top = Op bottom + +instance BoundedLattice a => BoundedLattice (Op a) where + +instance PartialOrd a => PartialOrd (Op a) where + Op a `leq` Op b = b `leq` a -- Note swap. + comparable (Op a) (Op b) = comparable a b diff --git a/src/Algebra/Lattice/Ordered.hs b/src/Algebra/Lattice/Ordered.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Ordered.hs @@ -0,0 +1,83 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeOperators #-} +#if __GLASGOW_HASKELL__ < 709 +{-# LANGUAGE Trustworthy #-} +#else +{-# LANGUAGE Safe #-} +#endif +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.Ordered +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Ordered ( + Ordered(..) + ) where + +import Prelude () +import Prelude.Compat + +import Algebra.Lattice +import Algebra.PartialOrd + +import Control.DeepSeq +import Control.Monad +import Data.Data +import Data.Hashable +import GHC.Generics + +-- +-- Ordered +-- + +-- | A total order gives rise to a lattice. Join is +-- max, meet is min. +newtype Ordered a = Ordered { getOrdered :: a } + deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable +#if __GLASGOW_HASKELL__ >= 706 + , Generic1 +#endif + ) + +instance Applicative Ordered where + pure = return + (<*>) = ap + +instance Monad Ordered where + return = Ordered + Ordered x >>= f = f x + +instance NFData a => NFData (Ordered a) where + rnf (Ordered a) = rnf a + +instance Hashable a => Hashable (Ordered a) + +instance Ord a => JoinSemiLattice (Ordered a) where + Ordered x \/ Ordered y = Ordered (max x y) + +instance Ord a => MeetSemiLattice (Ordered a) where + Ordered x /\ Ordered y = Ordered (min x y) + +instance Ord a => Lattice (Ordered a) where + +instance (Ord a, Bounded a) => BoundedJoinSemiLattice (Ordered a) where + bottom = Ordered minBound + +instance (Ord a, Bounded a) => BoundedMeetSemiLattice (Ordered a) where + top = Ordered maxBound + +instance (Ord a, Bounded a) => BoundedLattice (Ordered a) where + +instance Ord a => PartialOrd (Ordered a) where + leq = (<=) + comparable _ _ = True diff --git a/src/Algebra/PartialOrd.hs b/src/Algebra/PartialOrd.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/PartialOrd.hs @@ -0,0 +1,171 @@ +{-# LANGUAGE Safe #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.PartialOrd +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.PartialOrd ( + -- * Partial orderings + PartialOrd(..), + partialOrdEq, + + -- * Fixed points of chains in partial orders + lfpFrom, unsafeLfpFrom, + gfpFrom, unsafeGfpFrom + ) where + +import Data.Foldable (Foldable (..)) +import Data.Hashable (Hashable (..)) +import qualified Data.HashMap.Lazy as HM +import qualified Data.HashSet as HS +import qualified Data.IntMap as IM +import qualified Data.IntSet as IS +import qualified Data.List as L +import qualified Data.Map as M +import Data.Monoid (All (..)) +import qualified Data.Set as S +import Data.Void (Void) + +-- | A partial ordering on sets +-- () is a set equipped +-- with a binary relation, `leq`, that obeys the following laws +-- +-- @ +-- Reflexive: a ``leq`` a +-- Antisymmetric: a ``leq`` b && b ``leq`` a ==> a == b +-- Transitive: a ``leq`` b && b ``leq`` c ==> a ``leq`` c +-- @ +-- +-- Two elements of the set are said to be `comparable` when they are are +-- ordered with respect to the `leq` relation. So +-- +-- @ +-- `comparable` a b ==> a ``leq`` b || b ``leq`` a +-- @ +-- +-- If `comparable` always returns true then the relation `leq` defines a +-- total ordering (and an `Ord` instance may be defined). Any `Ord` instance is +-- trivially an instance of `PartialOrd`. 'Algebra.Lattice.Ordered' provides a +-- convenient wrapper to satisfy 'PartialOrd' given 'Ord'. +-- +-- As an example consider the partial ordering on sets induced by set +-- inclusion. Then for sets `a` and `b`, +-- +-- @ +-- a ``leq`` b +-- @ +-- +-- is true when `a` is a subset of `b`. Two sets are `comparable` if one is a +-- subset of the other. Concretely +-- +-- @ +-- a = {1, 2, 3} +-- b = {1, 3, 4} +-- c = {1, 2} +-- +-- a ``leq`` a = `True` +-- a ``leq`` b = `False` +-- a ``leq`` c = `False` +-- b ``leq`` a = `False` +-- b ``leq`` b = `True` +-- b ``leq`` c = `False` +-- c ``leq`` a = `True` +-- c ``leq`` b = `False` +-- c ``leq`` c = `True` +-- +-- `comparable` a b = `False` +-- `comparable` a c = `True` +-- `comparable` b c = `False` +-- @ +class Eq a => PartialOrd a where + -- | The relation that induces the partial ordering + leq :: a -> a -> Bool + + -- | Whether two elements are ordered with respect to the relation. A + -- default implementation is given by + -- + -- > comparable x y = leq x y || leq y x + comparable :: a -> a -> Bool + comparable x y = leq x y || leq y x + +-- | The equality relation induced by the partial-order structure. It must obey +-- the laws +-- @ +-- Reflexive: a == a +-- Transitive: a == b && b == c ==> a == c +-- @ +partialOrdEq :: PartialOrd a => a -> a -> Bool +partialOrdEq x y = leq x y && leq y x + +instance PartialOrd () where + leq _ _ = True + +instance PartialOrd Void where + leq _ _ = True + +-- | @'leq' = 'Data.List.isInfixOf'@. +instance Eq a => PartialOrd [a] where + leq = L.isInfixOf + +instance Ord a => PartialOrd (S.Set a) where + leq = S.isSubsetOf + +instance PartialOrd IS.IntSet where + leq = IS.isSubsetOf + +instance (Eq k, Hashable k) => PartialOrd (HS.HashSet k) where + leq a b = HS.null (HS.difference a b) + +instance (Ord k, PartialOrd v) => PartialOrd (M.Map k v) where + leq = M.isSubmapOfBy leq + +instance PartialOrd v => PartialOrd (IM.IntMap v) where + leq = IM.isSubmapOfBy leq + +instance (Eq k, Hashable k, PartialOrd v) => PartialOrd (HM.HashMap k v) where + x `leq` y = {- wish: HM.isSubmapOfBy leq -} + HM.null (HM.difference x y) && getAll (fold $ HM.intersectionWith (\vx vy -> All (vx `leq` vy)) x y) + +instance (PartialOrd a, PartialOrd b) => PartialOrd (a, b) where + -- NB: *not* a lexical ordering. This is because for some component partial orders, lexical + -- ordering is incompatible with the transitivity axiom we require for the derived partial order + (x1, y1) `leq` (x2, y2) = x1 `leq` x2 && y1 `leq` y2 + +-- | Least point of a partially ordered monotone function. Checks that the function is monotone. +lfpFrom :: PartialOrd a => a -> (a -> a) -> a +lfpFrom = lfpFrom' leq + +-- | Least point of a partially ordered monotone function. Does not checks that the function is monotone. +unsafeLfpFrom :: Eq a => a -> (a -> a) -> a +unsafeLfpFrom = lfpFrom' (\_ _ -> True) + +{-# INLINE lfpFrom' #-} +lfpFrom' :: Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a +lfpFrom' check init_x f = go init_x + where go x | x' == x = x + | x `check` x' = go x' + | otherwise = error "lfpFrom: non-monotone function" + where x' = f x + + +-- | Greatest fixed point of a partially ordered antinone function. Checks that the function is antinone. +{-# INLINE gfpFrom #-} +gfpFrom :: PartialOrd a => a -> (a -> a) -> a +gfpFrom = gfpFrom' leq + +-- | Greatest fixed point of a partially ordered antinone function. Does not check that the function is antinone. +{-# INLINE unsafeGfpFrom #-} +unsafeGfpFrom :: Eq a => a -> (a -> a) -> a +unsafeGfpFrom = gfpFrom' (\_ _ -> True) + +{-# INLINE gfpFrom' #-} +gfpFrom' :: Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a +gfpFrom' check init_x f = go init_x + where go x | x' == x = x + | x' `check` x = go x' + | otherwise = error "gfpFrom: non-antinone function" + where x' = f x diff --git a/src/Algebra/PartialOrd/Instances.hs b/src/Algebra/PartialOrd/Instances.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/PartialOrd/Instances.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE Safe #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.PartialOrd.Instances +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +-- This module re-exports orphan instances from 'Data.Universe.Instances.Eq' +-- module, and @(PartialOrd v, Finite k) => PartialOrd (k -> v)@ instance. +---------------------------------------------------------------------------- +module Algebra.PartialOrd.Instances () where + +import Algebra.PartialOrd (PartialOrd (..)) +import Data.Universe.Class (Finite (..)) +import Data.Universe.Instances.Eq () + +-- | @Eq (k -> v)@ is from 'Data.Universe.Instances.Eq' +instance (PartialOrd v, Finite k) => PartialOrd (k -> v) where + f `leq` g = all (\k -> f k `leq` g k) universeF diff --git a/test/Tests.hs b/test/Tests.hs --- a/test/Tests.hs +++ b/test/Tests.hs @@ -30,6 +30,8 @@ import Data.IntSet (IntSet) import Data.Map (Map) import Data.Set (Set) +import Data.HashMap.Lazy (HashMap) +import Data.HashSet (HashSet) import Data.Universe.Instances.Base () import Test.QuickCheck.Instances () @@ -47,8 +49,10 @@ , latticeLaws "M2" True (Proxy :: Proxy M2) -- M2 , latticeLaws "Map" True (Proxy :: Proxy (Map Int (O.Ordered Int))) , latticeLaws "IntMap" True (Proxy :: Proxy (IntMap (O.Ordered Int))) + , latticeLaws "HashMap" True (Proxy :: Proxy (HashMap Int (O.Ordered Int))) , latticeLaws "Set" True (Proxy :: Proxy (Set Int)) , latticeLaws "IntSet" True (Proxy :: Proxy IntSet) + , latticeLaws "HashSet" True (Proxy :: Proxy (HashSet Int)) , latticeLaws "Ordered" True (Proxy :: Proxy (O.Ordered Int)) , latticeLaws "Divisibility" True (Proxy :: Proxy (Div.Divisibility Int)) , latticeLaws "LexOrdered" True (Proxy :: Proxy (LO.Lexicographic (O.Ordered Int) (O.Ordered Int)))