# References for topological arguments of programs?

13 messages
Open this post in threaded view
|

## References for topological arguments of programs?

 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!ThanksSiddharth-- 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-cafeOnly members subscribed via the mailman list are allowed to post.
Open this post in threaded view
|

## Re: References for topological arguments of programs?

 Hi, Peter G. Hinman: Recursion-Theoretic Hierarchies might contain some related material. Best, Till Mossakowski Am 10.12.18 um 13:38 schrieb Siddharth Bhat: 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.``` _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafeOnly members subscribed via the mailman list are allowed to post.
Open this post in threaded view
|

## Re: References for topological arguments of programs?

 In reply to this post by Siddharth Bhat 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 <[hidden email]> 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. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafeOnly members subscribed via the mailman list are allowed to post.
Open this post in threaded view
|

## Re: References for topological arguments of programs?

 In reply to this post by Siddharth Bhat I highly recommend the So-called "Barbados notes" [1] of Martín Escardó. It is a systematic development of synthetic topology, with program fragments in Haskell. It is to my knowledge the first appearance of the so-called searchable sets and contains many other gems. I myself have been working on "Haskell for mathematicians", which shall become an entry point to the language for those with a background stronger in mathematics than in other programming languages. It is planned to touch on many areas of mathematics, not only topology. If anyone would like to have a look at the current stage, I'd be happy to share the source. Olaf [1] Synthetic Topology: of Data Types and Classical Spaces https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/87/Pages 21-156, Open access [Disclaimer: Martín Escardó was one of my PhD supervisors.] > Am 10.12.2018 um 13:38 schrieb Siddharth Bhat <[hidden email]>: > > 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-cafeOnly members subscribed via the mailman list are allowed to post.
Open this post in threaded view
|

## Re: References for topological arguments of programs?

Open this post in threaded view
|

## Re: References for topological arguments of programs?

Open this post in threaded view
|

## Re: References for topological arguments of programs?

Open this post in threaded view
|

## Re: References for topological arguments of programs?

Open this post in threaded view
|

## Re: References for topological arguments of programs?

Open this post in threaded view
|

## Re: References for topological arguments of programs?

Open this post in threaded view
|

## Re: References for topological arguments of programs?

 In reply to this post by Olaf Klinke > Does anyone know whether literate haskell can be used to generate html? You can use Pandoc¹.  Or alternatively, first use lhs2tex² to get LaTeX, and then use Pandoc or one of the tools listed here³ to convert LaTeX to HTML.  I haven’t tried either of the approaches, so it would be nice if someone could speak on how they compare in terms of the quality of the final document. HTH. Footnotes: ¹  https://pandoc.org/MANUAL.html#literate-haskell-support²  https://hackage.haskell.org/package/lhs2tex³  https://texfaq.org/FAQ-LaTeX2HTML_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafeOnly members subscribed via the mailman list are allowed to post.