Olaf Klinke
2018-12-10 20:28:20 UTC
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.]
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.]
Hello,
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!
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!