Portability | portable |
---|---|
Stability | experimental |
Maintainer | Luke Palmer <lrpalmer@gmail.com> |
An implementation of nonempty searchable sets, i.e. sets s which admit a
total operation search s :: (a -> Bool) -> Maybe a
.
Example usage:
bit = pairSet 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.com20081121a-haskell-monad-for-infinite-search-in-finite-time/
Documentation
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
.
This operation is total whenever p
is total.
bigUnion :: Set (Set a) -> Set aSource
bigUnion ss
is the union of all the elemens of ss
. In other words,
x
iff member
bigUnion ssforsome ss (s -> x
.
member
s)
forsome :: Set a -> (a -> Bool) -> BoolSource
forsome s p
returns True iff there is some element x
of s
such that
p x = True
.