References for topological arguments of programs?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
13 messages Options
Reply | Threaded
Open this post in threaded view
|

References for topological arguments of programs?

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.
Reply | Threaded
Open this post in threaded view
|

Re: References for topological arguments of programs?

Till Mossakowski-3
Hi,

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

Best, Till Mossakowski


Am 10.12.18 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.
Reply | Threaded
Open this post in threaded view
|

Re: References for topological arguments of programs?

Stuart A. Kurtz
In reply to this post by Siddharth Bhat
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.

> On Dec 10, 2018, at 6:38 AM, Siddharth Bhat <[hidden email]> wrote:
>
> 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.
Reply | Threaded
Open this post in threaded view
|

Re: References for topological arguments of programs?

Olaf Klinke
In reply to this post by Siddharth Bhat
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 <[hidden email]>:
>
> 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.
Reply | Threaded
Open this post in threaded view
|

Re: References for topological arguments of programs?

Ara Adkins
I’d love to take a read of the current stage of your book!

_ara

> On 10 Dec 2018, at 20:28, Olaf Klinke <[hidden email]> 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 <[hidden email]>:
>>
>> 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.
Reply | Threaded
Open this post in threaded view
|

Re: References for topological arguments of programs?

migmit-2
Same here!

Az iPademről küldve

2018. dec. 10. dátummal, 21:32 időpontban Ara Adkins <[hidden email]> í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 <[hidden email]> 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 <[hidden email]>:
>>>
>>> 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.
Reply | Threaded
Open this post in threaded view
|

Re: References for topological arguments of programs?

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

On Tue, 11 Dec, 2018, 02:05 MigMit, <[hidden email]> wrote:
Same here!

Az iPademről küldve

2018. dec. 10. dátummal, 21:32 időpontban Ara Adkins <[hidden email]> í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 <[hidden email]> 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 <[hidden email]>:
>>>
>>> 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.
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]>:
>
> Agreed, having access to the book would be fantastic. :)
>
> On Tue, 11 Dec, 2018, 02:05 MigMit, <[hidden email]> wrote:
> Same here!
>
> Az iPademről küldve
>
> 2018. dec. 10. dátummal, 21:32 időpontban Ara Adkins <[hidden email]> í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 <[hidden email]> 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 <[hidden email]>:
> >>>
> >>> 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.
Reply | Threaded
Open this post in threaded view
|

Re: References for topological arguments of programs?

Ara Adkins
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 <[hidden email]> 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 <[hidden email]>:
>>
>> Agreed, having access to the book would be fantastic. :)
>>
>> On Tue, 11 Dec, 2018, 02:05 MigMit, <[hidden email]> wrote:
>> Same here!
>>
>> Az iPademről küldve
>>
>> 2018. dec. 10. dátummal, 21:32 időpontban Ara Adkins <[hidden email]> í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 <[hidden email]> 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 <[hidden email]>:
>>>>>
>>>>> 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.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: References for topological arguments of programs?

Bhavik Mehta
In reply to this post by Olaf Klinke
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 <[hidden email]> 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 <[hidden email]>:
>
> Agreed, having access to the book would be fantastic. :)
>
> On Tue, 11 Dec, 2018, 02:05 MigMit, <[hidden email]> wrote:
> Same here!
>
> Az iPademről küldve
>
> 2018. dec. 10. dátummal, 21:32 időpontban Ara Adkins <[hidden email]> í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 <[hidden email]> 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 <[hidden email]>:
> >>>
> >>> 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.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: References for topological arguments of programs?

Amin Bandali-2
In reply to this 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
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: References for topological arguments of programs?

Ryan Reich
In reply to this post by Olaf Klinke
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 <[hidden email]> 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 <[hidden email]>:
>
> 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.
Reply | Threaded
Open this post in threaded view
|

Re: References for topological arguments of programs?

Vanessa McHale
In reply to this post by Olaf Klinke
I'd be quite interested in such a book/monograph - less as an
introduction to the language and more as a way of seeing the higher
mathematics one can use in Haskell/functional programming.

On 12/10/18 2:28 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-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 <[hidden email]>:
>>
>> 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.

signature.asc (499 bytes) Download Attachment