Maintainer	Olaf Klinke
Stability	experimental
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Searchable

Contents

Data types
Queries
Construction

Description

There exist two packages for exhaustive search: infinite-search and the Select monad transformer.

This module extends the former (which has a much smaller dependency footprint) with the empty subset. The resulting monad K does not only support unions but also intersections.

Synopsis

data K a
- = Emptyset
- | Nonempty ((a -> Bool) -> a)
restrict :: K a -> (a -> Bool) -> K a
intersection :: Eq a => K a -> K a -> K a
exists :: K a -> (a -> Bool) -> Bool
forevery :: K a -> (a -> Bool) -> Bool
member :: Eq a => a -> K a -> Bool
list2K :: Foldable f => f a -> K a

Data types

data K a Source #

If sub-sets of a type admit continuous universal quantification ∀, then the empty sub-set is an isolated element: Indeed, for no other set should ∀ (const False) be true.

Therefore it is sound to have a separate constructor for the empty set.

Constructors

Emptyset
Nonempty ((a -> Bool) -> a)	selection function

Instances

Instances details

Alternative K Source #
Instance details Defined in Data.Searchable Methods empty :: K a # (<\|>) :: K a -> K a -> K a # some :: K a -> K [a] # many :: K a -> K [a] #
Applicative K Source #
Instance details Defined in Data.Searchable Methods pure :: a -> K a # (<>) :: K (a -> b) -> K a -> K b # liftA2 :: (a -> b -> c) -> K a -> K b -> K c # (>) :: K a -> K b -> K b # (<*) :: K a -> K b -> K a #
Functor K Source #
Instance details Defined in Data.Searchable Methods fmap :: (a -> b) -> K a -> K b # (<$) :: a -> K b -> K a #
Monad K Source #
Instance details Defined in Data.Searchable Methods (>>=) :: K a -> (a -> K b) -> K b # (>>) :: K a -> K b -> K b # return :: a -> K a #
MonadPlus K Source #
Instance details Defined in Data.Searchable Methods mzero :: K a # mplus :: K a -> K a -> K a #
(Ord a, Show a) => Show (K a) Source #
Instance details Defined in Data.Searchable Methods showsPrec :: Int -> K a -> ShowS # show :: K a -> String # showList :: [K a] -> ShowS #
Eq a => Eq (K a) Source #
Instance details Defined in Data.Searchable Methods (==) :: K a -> K a -> Bool # (/=) :: K a -> K a -> Bool #

restrict :: K a -> (a -> Bool) -> K a Source #

Intersect a compact with a clopen

intersection :: Eq a => K a -> K a -> K a Source #

If every compact set is clopen, then the space is discrete. Indeed, discreteness means singletons are open. Singletons are always compact.

Queries

exists :: K a -> (a -> Bool) -> Bool Source #

existential quantification

forevery :: K a -> (a -> Bool) -> Bool Source #

universal quantification

member :: Eq a => a -> K a -> Bool Source #

membership is decidable for discrete spaces

Construction

list2K :: Foldable f => f a -> K a Source #

convert lists

>>> list2K [4,2,2,2,3 :: Integer]
{2,3,4}