module Algebra.PartialOrd (
PartialOrd(..),
partialOrdEq,
lfpFrom, unsafeLfpFrom,
gfpFrom, unsafeGfpFrom
) where
import Algebra.Enumerable
import qualified Data.Set as S
import qualified Data.Map as M
class Eq a => PartialOrd a where
leq :: a -> a -> Bool
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 (Ord k, PartialOrd v) => PartialOrd (M.Map k v) where
leq = M.isSubmapOf
instance (Eq v, Enumerable k) => Eq (k -> v) where
f == g = all (\k -> f k == g k) universe
instance (PartialOrd v, Enumerable k) => PartialOrd (k -> v) where
f `leq` g = all (\k -> f k `leq` g k) universe
instance (PartialOrd a, PartialOrd b) => PartialOrd (a, b) where
(x1, y1) `leq` (x2, y2) = x1 `leq` x2 && y1 `leq` y2
lfpFrom :: PartialOrd a => a -> (a -> a) -> a
lfpFrom = lfpFrom' leq
unsafeLfpFrom :: Eq a => a -> (a -> a) -> a
unsafeLfpFrom = lfpFrom' (\_ _ -> True)
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
gfpFrom :: PartialOrd a => a -> (a -> a) -> a
gfpFrom = gfpFrom' leq
unsafeGfpFrom :: Eq a => a -> (a -> a) -> a
unsafeGfpFrom = gfpFrom' (\_ _ -> True)
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