[Haskell-cafe] References for topological arguments of programs?

[Stuart A. Kurtz]

I've not been following this, but (a -> Bool) -> a is essentially a choice function, which figured in Ernst Zermelo's proof of the well-ordering theorem.

> On Dec 10, 2018, at 6:38 AM, Siddharth Bhat <siddu.druid at gmail.com> wrote:
> 
> Hello,
> 
> I was recently intrigued by this style of argument on haskell cafe:
> 
> 
> 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. 
> -------
> 
> 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.
> 
> 
> I'd love to have a reference (papers / textbook preferred) to self learn this stuff!
> 
> Thanks
> Siddharth
> -- 
> 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.