{-# LANGUAGE Safe #-} ---------------------------------------------------------------------------- -- | -- Module : Algebra.PartialOrd -- Copyright : (C) 2010-2015 Maximilian Bolingbroke -- License : BSD-3-Clause (see the file LICENSE) -- -- Maintainer : Oleg Grenrus <oleg.grenrus@iki.fi> -- ---------------------------------------------------------------------------- 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 -- (<http://en.wikipedia.org/wiki/Partially_ordered_set>) 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