|Maintainer||Luke Palmer <firstname.lastname@example.org>|
An implementation of nonempty searchable (compact and overt) sets, i.e. sets s
which admit a total operation
search s :: (a -> Bool) -> Maybe a.
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
- search :: Set a -> (a -> Bool) -> Maybe a
- bigUnion :: Set (Set a) -> Set a
- contains :: Eq a => Set a -> a -> Bool
- member :: Eq a => a -> Set a -> Bool
- forsome :: Set a -> (a -> Bool) -> Bool
- forevery :: Set a -> (a -> Bool) -> Bool
- singleton :: a -> Set a
- doubleton :: a -> a -> Set a
- union :: Set a -> Set a -> 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.
Choose a member of the set satisfying a predicate.
search s p = Just x then
p x = True.
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).
Tests whether the set contains an element.
contains s x = forsome s (== x).
forsome s p returns True iff there is some element
s such that
p x = True.
forevery s p returns True iff every element
p x =