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

Thanks so much Olaf! I’m looking forward to giving this a read on my plane ride tomorrow! _ara

On 10 Dec 2018, at 21:05, Olaf Klinke wrote:

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 :

Agreed, having access to the book would be fantastic. :)

On Tue, 11 Dec, 2018, 02:05 MigMit, wrote: Same here!

Az iPademről küldve

2018. dec. 10. dátummal, 21:32 időpontban Ara Adkins í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 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-comput... 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 :

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!

_______________________________________________ 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.