infinite-search-0.12: Exhaustively searchable infinite sets.

Portability portable experimental Luke Palmer

Data.Searchable

Description

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/`

Synopsis

# Documentation

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.

Instances

 Monad Set Functor Set Applicative Set

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