Data.Searchable

An implementation of nonempty searchable (compact and overt) 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/

Documentation

data Set a

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.

Instances

Monad Set

Functor Set

Applicative Set

search :: Set a -> (a -> Bool) -> Maybe a

Choose a member of the set satisfying a predicate. If search s p = Just x then p x = True.

bigUnion :: Set (Set a) -> Set a

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).

contains :: Eq a => Set a -> a -> Bool

Tests whether the set contains an element. contains s x = forsome s (== x).

member :: Eq a => a -> Set a -> Bool

member = flip contains

forsome :: Set a -> (a -> Bool) -> Bool

forsome s p returns True iff there is some element x of s such that p x = True.

forevery :: Set a -> (a -> Bool) -> Bool

forevery s p returns True iff every element x of s satisfies p x = True.

singleton :: a -> Set a

singleton x is the set {x}.

doubleton :: a -> a -> Set a

pair x y is the set {x,y}.

union :: Set a -> Set a -> Set a

x `member` union s t iff (x `member` s) || (x `member` t).