refined-subtype-0.1.0.0: compute subtypes from refinement types
MaintainerOlaf Klinke
Stabilityexperimental
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Searchable

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