---------------------------------------- -- | -- Module : Data.IVar -- License : BSD3 -- -- Maintainer : Luke Palmer <lrpalmer@gmail.com> -- Stability : experimental -- Portability : portable -- -- An implementation of nonempty "searchable" sets, i.e. sets s which admit a -- total operation @search s :: (a -> Bool) -> Maybe a@. -- -- Example usage: -- -- > bit = pair True False -- > cantor = sequence (repeat bit) -- > take 5 $ search cantor (\s -> not (s !! 3) && (s !! 4)) -- > -- gives [True, True, True, False, True] -- -- This module is based on the paper "Exhaustible sets in higher-type computation" -- by Martin Escardo, and is almost identical to the code in his his expository blog -- post on the subject: http://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/ ---------------------------------------- module Data.Searchable (Set, search, bigUnion, contains, member, forsome, forevery, singleton, doubleton, union) where import Control.Applicative import Control.Monad (ap) -- | @Set a@ is a nonempty searchable set of a's. -- There is no Monoid or MonadPlus instance, since -- we lack the ability to represent the empty set, -- which would be the units of those structures. newtype Set a = Set { find :: (a -> Bool) -> a } instance Functor Set where fmap f s = Set (\p -> f (find s (p . f))) instance Monad Set where return = Set . const m >>= f = bigUnion (fmap f m) instance Applicative Set where pure = return (<*>) = ap -- | @bigUnion ss@ is the union of all the elemens of @ss@. In other words, -- @x `member` bigUnion ss@ iff @forsome ss (\s -> x `member` s)@. bigUnion :: Set (Set a) -> Set a bigUnion ss = Set (\p -> find (find ss (\s -> forsome s p)) p) -- | Tests whether the set contains an element. @contains s x = forsome s (== x)@. contains :: (Eq a) => Set a -> a -> Bool contains s x = forsome s (== x) -- | @member = flip contains@ member :: (Eq a) => a -> Set a -> Bool member = flip contains -- | Choose a member of the set satisfying a predicate. -- If @search s p = Just x@ then @p x = True@. search :: Set a -> (a -> Bool) -> Maybe a search s p = if p x then Just x else Nothing where x = find s p -- | @forsome s p@ returns True iff there is some element @x@ of @s@ such that -- @p x = True@. forsome :: Set a -> (a -> Bool) -> Bool forsome s p = p (find s p) -- | @forevery s p@ returns True iff every element @x@ of @s@ satisfies @p x = -- True@. forevery :: Set a -> (a -> Bool) -> Bool forevery s p = not (forsome s (not . p)) -- | @singleton x@ is the set @{x}@. singleton :: a -> Set a singleton = return -- | @pair x y@ is the set @{x,y}@. doubleton :: a -> a -> Set a doubleton x y = Set (\p -> if p x then x else y) -- | @x `member` union s t@ iff @(x `member` s) || (x `member` t)@. union :: Set a -> Set a -> Set a union s t = bigUnion (doubleton s t)