<span>Hello,</span><div><br></div><div>I was recently intrigued by this style of argument on haskell cafe:</div><div><br></div><div><br></div><div>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></div><div>-------</div><div><br></div><div>I've seen arguments like these "in the wild" during Scott topology construction and in some other weird places (hyperfunctions), but I've never seen a systematic treatment of this.</div><div><br></div><div><br></div><div>I'd love to have a reference (papers / textbook preferred) to self learn this stuff!</div><div><br></div><div>Thanks</div><div>Siddharth</div>-- <br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr">Sending this from my phone, please excuse any typos!</div></div>