Discussion:
[Haskell-cafe] References for topological arguments of programs?
Olaf Klinke
2018-12-10 20:28:20 UTC
Permalink
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.]
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!
Ara Adkins
2018-12-10 20:32:14 UTC
Permalink
I’d love to take a read of the current stage of your book!

_ara
Post by Olaf Klinke
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.]
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!
_______________________________________________
Haskell-Cafe mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
MigMit
2018-12-10 20:35:18 UTC
Permalink
Same here!

Az iPademről küldve
Post by Ara Adkins
I’d love to take a read of the current stage of your book!
_ara
Post by Olaf Klinke
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.]
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!
_______________________________________________
Haskell-Cafe mailing list
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Siddharth Bhat
2018-12-10 20:56:23 UTC
Permalink
Agreed, having access to the book would be fantastic. :)
Post by MigMit
Same here!
Az iPademről kÃŒldve
I’d love to take a read of the current stage of your book!
_ara
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.]
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!
_______________________________________________
Haskell-Cafe mailing list
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
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
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!
Olaf Klinke
2018-12-10 21:05:03 UTC
Permalink
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
Post by Siddharth Bhat
Agreed, having access to the book would be fantastic. :)
Same here!
Az iPademről küldve
Post by Ara Adkins
I’d love to take a read of the current stage of your book!
_ara
Post by Olaf Klinke
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.]
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!
_______________________________________________
Haskell-Cafe mailing list
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
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
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!
Ara Adkins
2018-12-10 21:06:10 UTC
Permalink
Thanks so much Olaf! I’m looking forward to giving this a read on my plane ride tomorrow!

_ara
Post by 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
Post by Siddharth Bhat
Agreed, having access to the book would be fantastic. :)
Same here!
Az iPademről küldve
Post by Ara Adkins
I’d love to take a read of the current stage of your book!
_ara
Post by Olaf Klinke
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.]
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!
_______________________________________________
Haskell-Cafe mailing list
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
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
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Bhavik Mehta
2018-12-10 21:32:25 UTC
Permalink
I'm happy to do this, I'll aim to put it up over the next few days!

Bhavik Mehta
Post by 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
Post by Siddharth Bhat
Agreed, having access to the book would be fantastic. :)
Same here!
Az iPademről kÃŒldve
I’d love to take a read of the current stage of your book!
_ara
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.
Post by Siddharth Bhat
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.
Post by Siddharth Bhat
Olaf
[1] Synthetic Topology: of Data Types and Classical Spaces
https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/87/
Post by Siddharth Bhat
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.
Post by Siddharth Bhat
-------
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.
Post by Siddharth Bhat
I'd love to have a reference (papers / textbook preferred) to self
learn this stuff!
Post by Siddharth Bhat
Thanks
Siddharth
--
Sending this from my phone, please excuse any typos!
_______________________________________________
Haskell-Cafe mailing list
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
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
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Amin Bandali
2018-12-10 21:33:09 UTC
Permalink
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
Stuart A. Kurtz
2018-12-10 14:43:43 UTC
Permalink
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.
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!
_______________________________________________
Haskell-Cafe mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Till Mossakowski
2018-12-10 13:34:07 UTC
Permalink
Hi,

Peter G. Hinman: Recursion-Theoretic Hierarchies might contain some
related material.

Best, Till Mossakowski
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!
_______________________________________________
Haskell-Cafe mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Ryan Reich
2018-12-10 21:53:07 UTC
Permalink
Hi Olaf,

I think I'd be interested in seeing your work-in-progress.

Ryan Reich
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.]
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!
_______________________________________________
Haskell-Cafe mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Loading...