infinite-search-0.12: Exhaustively searchable infinite sets.

MaintainerLuke Palmer <>



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:



data Set a Source

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.

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

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

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

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 -> BoolSource

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

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

member = flip contains

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

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

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

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

singleton :: a -> Set aSource

singleton x is the set {x}.

doubleton :: a -> a -> Set aSource

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

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

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