Re: [Haskell-cafe] Faster set intersections?

11 Dec 2018

...
Am 11.12.2018 um 00:50 schrieb Clinton Mead :
One can write a function 
Eq a => ((a -> Bool) -> a) -> [a]
that enumerates the elements of the set. Because we have universal quantification, this list can not be infinite. Which makes sense, topologically: These so-called searchable sets are topologically compact, and the Eq constraint means the space is discrete. Compact subsets of a discrete space are finite.
Olaf
Olaf (or anyone else), can you help me out here and write this function, with some example inputs and outputs?
Below is my testing version of the searchable sets. The names differ slightly from the ones in the infinite-search package. The function you are looking for is called 'enumerate' -- Olaf

module Searchable where
import Control.Monad
import qualified Control.Applicative 
import Data.Set (Set)
import qualified Data.Set as Set
-- Escardo's Monad for non-empty compact subsets. 
-- Data type of searchable subsets of a.
-- Specification: 
-- For every predicate p :: a -> Bool and searchable set k :: S a, 
-- there exists some x in k with p(x) if and only if  p(find k p). 
newtype S a = Finder ((a -> Bool) -> a)

find :: S a -> (a -> Bool) -> a
find (Finder f) p = f p

exists :: S a -> (a -> Bool) -> Bool
exists (Finder f) p = p (f p)

forall :: S a -> (a -> Bool) -> Bool
forall k p = not $ exists k (not.p)

instance Functor S where
    fmap g (Finder f) = Finder (\p -> g(f(p.g)))

singleton :: a -> S a
singleton x = Finder (const x)

-- Compact subsets of totally ordered types have least and greatest elements.
isSingleton :: (Ord a) => S a -> Bool
isSingleton k = (inf k id) >= (sup k id)

doubleton :: a -> a -> S a
doubleton x y = Finder (\p -> if p x then x else y)

-- doubleton x y = finite [x,y]
finite :: [a] -> S a
finite [] = error "{} is compact, but empty"
finite [x] = singleton x
finite (x:xs) = (singleton x) \/ (finite xs)

-- the union of compactly many compact sets is compact.
-- union (doubleton x y) = x \/ y
union :: S (S a) -> S a
union (Finder ff) = Finder (\p -> 
    let Finder f = ff (\k -> exists k p)
    in f p)

-- binary union. Generalises doubleton. 
infixl 5 \/
(\/) :: S a -> S a -> S a
(Finder f) \/ (Finder f') = Finder (\p -> if p (f p) then f p else f' p)

instance Monad S where
    return = singleton
    k >>= f = union $ fmap f k
instance Control.Applicative.Applicative S where
    pure = return
    (<*>) = ap

-- Searchable subsets of discrete spaces are clopen, 
-- searchable subsets of Hausdorff spaces are closed.  
-- Notice that 
--
-- @
-- (flip member) :: S a -> (a -> Bool)
-- @
--
-- This predicate returns 'False' iff the element is not member of the set 
-- and 'True' for every element of the set, provided that equality is decidable. 
member :: (Eq a) => a -> S a -> Bool
x `member` k = exists k (x ==) 

-- output the part of the list that is in the compact set. 
filterS :: (Eq a) => S a -> [a] -> [a]
filterS k = filter (flip member k)

-- In every sober space, the intersection of a compact set 
-- with a closed set is compact (but may be empty). 
-- If the intersection is not empty, this function will compute it. 
intersect :: (a -> Bool) -> S a -> S a
intersect c k = Finder (\p -> find k (\x -> p x && c x))

-- instances of Ord have searchable subsets that can be well-ordered.
sort :: (Ord a) => S a -> Set a
sort k = let 
    i = inf k id
    extend current_largest set = if y > current_largest then extend y (Set.insert y set) else set where
        y = find k (current_largest <)
    in extend i (Set.singleton i)

-- instances of Eq have searchable subsets that can be enumerated. O(n^2).
-- The Eq constraint means the underlying space is discrete, 
-- and compact subsets of a discrete space are finite. 
enumerate :: (Eq a) => S a -> [a]
enumerate k = let
    another p = let y = find k p in if p y then Just y else Nothing
    Just x0 = another (const True)
    extend enumeration = case another (not.flip elem enumeration) of
        Nothing -> enumeration
        Just e  -> extend (e:enumeration)
    in extend [x0]

-- fold of a function into a commutative monoid. 
-- Since searchable sets have no intrinsic order, 
-- the result of the fold is only well-defined if the monoid is commutative. 
foldMapEq :: (Monoid m, Eq m) => (a -> m) -> S a -> m
foldMapEq f k = mconcat (enumerate (fmap f k))

-- show at most 8 elements of a compact set. 
instance (Show a, Ord a) => Show (S a) where
    show k = begin $ take 8 $ Set.elems $ sort k where
        begin l
            | length l < 8 = show l
            | otherwise = (init $ show l)++", ...]"

-- Equality lifts to searchable subsets, 
-- because the subset relation is computable. 
instance (Eq a) => Eq (S a) where
    k == k' = let 
        subset k k' = forall k (\x -> member x k')
        in (subset k k') && (subset k' k)

-- A continuous map on a compact set attains its infimum and supremum. 
inf :: (Ord b) => S a -> (a -> b) -> a
inf k@(Finder f) g = f (\x -> forall k (\y -> g(x) <= g(y))) 

sup :: (Ord b) => S a -> (a -> b) -> a
sup k@(Finder f) g = f (\x -> forall k (\y -> g(y) <= g(x)))

-- Hausdorff distance, given a metric. 
-- This is a special case of the so-called Egli-Milner relation lifting.
dHaus :: (Ord r) => (a -> a -> r) -> S a -> S a -> r
dHaus d k k' = let
    h k1 k2 = i (sup k1 i) where 
        i = \x -> d x (inf k2 (d x))
    in max (h k k') (h k' k)

{-- Examples --}

-- [()] = ℕ ∪ {∞} is compact.
nats :: S [()]
nats = Finder f where
    f p = if p [] then [] else ():f (\n -> p (():n))

-- Cantor space (ℕ → 2) is a compact subspace of Baire space (ℕ → ℕ).
cantor :: S [Int]
cantor = sequence $ repeat $ doubleton 0 1

-- Drinker's paradox:
-- For evers non-empty compact pub, 
-- there is a person x such that 
-- if x drinks, then everybody in the pub drinks.
drinker :: S person -> (person -> Bool) -> person
drinker in_pub drinks = find in_pub (not.drinks)

Re: [Haskell-cafe] Faster set intersections?

Olaf Klinke