Naïvely, a set implemented as a predicate determining membership? On Sun, Dec 9, 2018 at 1:32 PM Siddharth Bhat wrote:

I don't understand, how does

(a -> Bool) -> a

model a set?

Thanks Siddharth

On Sun, 9 Dec, 2018, 22:08 Olaf Klinke, wrote:

...

...

Note that a concrete set "concretizes" anything it touches. Don't take unions of these sets, though, it'll just be a mess.

Won't a union just be the same as intersection but using || instead of && ?

-Jan-Willem Maessen

Unions of predicates and concrete sets are easy, thanks to Set.member:

union (Pred p) (Concrete s) = Pred (\k -> p k || member k s)

What you can not do, of course, is enumerate and fold these sets. There is a set type [1] which supports a litte bit more:

Set a = Maybe ((a -> Bool) -> a)

It has unions, intersections and a Monad instance and can represent infinite sets. If the base type has an Ord instance, the set can be enumerated. If the base type has an Eq instance, so has (Set a). Some functions usually implemented using Foldable are also possible, e.g. minimum and maximum. Caveat: Performance can be poor, depending on how the function inside the set was defined.

Cheers, Olaf

[1] http://hackage.haskell.org/package/infinite-search _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- Sending this from my phone, please excuse any typos! _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- brandon s allbery kf8nh allbery.b@gmail.com

My guess — by finding a member that satisfies a predicate, if it's at all possible, and any member if the predicate is const False. It's actually pretty awesome.

On 9 Dec 2018, at 19:36, Brandon Allbery wrote:

Naïvely, a set implemented as a predicate determining membership?

On Sun, Dec 9, 2018 at 1:32 PM Siddharth Bhat wrote: I don't understand, how does

(a -> Bool) -> a

model a set?

Thanks Siddharth

On Sun, 9 Dec, 2018, 22:08 Olaf Klinke, wrote:

...

Note that a concrete set "concretizes" anything it touches. Don't take unions of these sets, though, it'll just be a mess.

Won't a union just be the same as intersection but using || instead of && ?

-Jan-Willem Maessen

Unions of predicates and concrete sets are easy, thanks to Set.member:

union (Pred p) (Concrete s) = Pred (\k -> p k || member k s)

What you can not do, of course, is enumerate and fold these sets. There is a set type [1] which supports a litte bit more:

Set a = Maybe ((a -> Bool) -> a)

It has unions, intersections and a Monad instance and can represent infinite sets. If the base type has an Ord instance, the set can be enumerated. If the base type has an Eq instance, so has (Set a). Some functions usually implemented using Foldable are also possible, e.g. minimum and maximum. Caveat: Performance can be poor, depending on how the function inside the set was defined.

Cheers, Olaf

[1] http://hackage.haskell.org/package/infinite-search _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. -- Sending this from my phone, please excuse any typos! _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- brandon s allbery kf8nh allbery.b@gmail.com _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Am 09.12.2018 um 19:47 schrieb David Feuer :

That does seem to be what the source code says. The code only handles non-empty sets, but I *believe* the Maybe-wrapped version can handle intersections, albeit inefficiently. Can a version that looks like (a -> Bool) -> Maybe a work? I think so. The empty set is then represented by the function that returns Nothing even on (const True). Indeed, with Maybe on the outside the intersection function requires the Eq constraint on the base type: We have member :: Eq a => a -> ((a -> Bool) -> a) -> Bool member x find = x == (find (x==))

Then the intersection of find and find' can be implemented using \p -> find (\x -> p x && member x find') But I fail to see how having Maybe on the inside remedies this situation. Furthermore, on Eq types these sets are not so interesting, for the following reason. 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

On Sun, Dec 9, 2018, 1:41 PM MigMit

...

On 9 Dec 2018, at 19:36, Brandon Allbery wrote:

Naïvely, a set implemented as a predicate determining membership?

On Sun, Dec 9, 2018 at 1:32 PM Siddharth Bhat wrote: I don't understand, how does

(a -> Bool) -> a

model a set?

Thanks Siddharth

On Sun, 9 Dec, 2018, 22:08 Olaf Klinke, wrote:

...

Note that a concrete set "concretizes" anything it touches. Don't take unions of these sets, though, it'll just be a mess.

Won't a union just be the same as intersection but using || instead of && ?

-Jan-Willem Maessen

Unions of predicates and concrete sets are easy, thanks to Set.member:

union (Pred p) (Concrete s) = Pred (\k -> p k || member k s)

What you can not do, of course, is enumerate and fold these sets. There is a set type [1] which supports a litte bit more:

Set a = Maybe ((a -> Bool) -> a)

It has unions, intersections and a Monad instance and can represent infinite sets. If the base type has an Ord instance, the set can be enumerated. If the base type has an Eq instance, so has (Set a). Some functions usually implemented using Foldable are also possible, e.g. minimum and maximum. Caveat: Performance can be poor, depending on how the function inside the set was defined.

Cheers, Olaf

[1] http://hackage.haskell.org/package/infinite-search _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. -- Sending this from my phone, please excuse any typos! _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- brandon s allbery kf8nh allbery.b@gmail.com _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

On Sun, Dec 9, 2018, 3:54 PM David Feuer

I don't understand how that's finite and not just countable.

Ah, I guess because there's no way to look at all elements of an infinite set. D'oh.

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)