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

[Olaf Klinke]

I suggest to use Bhavik Mehta's page haskellformathematicians.wordpress.com if we can not find a more official place for it on haskell.org. At this point I'd like to thank Haskell Café member Sergiu Ivanov for inspiring me to start working on this. 

Does anyone know whether literate haskell can be used to generate html? 

Olaf

> Am 10.12.2018 um 21:56 schrieb Siddharth Bhat <siddu.druid at gmail.com>:
> 
> Agreed, having access to the book would be fantastic. :)
> 
> On Tue, 11 Dec, 2018, 02:05 MigMit, <migmit at gmail.com> wrote:
> Same here!
> 
> Az iPademről küldve
> 
> 2018. dec. 10. dátummal, 21:32 időpontban Ara Adkins <me at ara.io> írta:
> 
> > I’d love to take a read of the current stage of your book!
> > 
> > _ara
> > 
> >> On 10 Dec 2018, at 20:28, Olaf Klinke <olf at aatal-apotheke.de> wrote:
> >> 
> >> 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 <siddu.druid at gmail.com>:
> >>> 
> >>> 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-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-cafe
> Only members subscribed via the mailman list are allowed to post.
> -- 
> Sending this from my phone, please excuse any typos!