<div dir="auto"><div><div class="gmail_quote"><div dir="ltr">On Sun, Dec 9, 2018, 2:30 PM Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de" target="_blank" rel="noreferrer">olf@aatal-apotheke.de</a> wrote:</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
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. <br></blockquote></div></div><div dir="auto"><br></div><div dir="auto">With Maybe on the outside, you can't jump straight to defining the function; you must first determine whether the intersection is empty. To my mind, a more natural definition for (possibly empty) sets is</div><div dir="auto"><br></div><div dir="auto">data Set a = Set {find :: (a -> Maybe b) -> Maybe b}</div><div dir="auto"><br></div><div dir="auto">which really explains how this is a set.</div><div dir="auto"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
One can write a function <br>
Eq a => ((a -> Bool) -> a) -> [a]<br>
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.<br></blockquote></div></div><div dir="auto"><br></div><div dir="auto">I don't understand how that's finite and not just countable.</div></div>