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.

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!

I'm happy to do this, I'll aim to put it up over the next few days! Bhavik Mehta On Mon, 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.

Hi Olaf, I think I'd be interested in seeing your work-in-progress. Ryan Reich On Mon, Dec 10, 2018 at 12:29 PM 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.