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

Siddharth Bhat siddu.druid at gmail.com
Mon Dec 10 12:38:20 UTC 2018


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!

Sending this from my phone, please excuse any typos!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181210/564f0da6/attachment.html>

More information about the Haskell-Cafe mailing list