[Haskell-cafe] 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 <olf at aatal-apotheke.de> 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 <siddu.druid at gmail.com>:
>> 
>> Agreed, having access to the book would be fantastic. :)
>> 
>> On Tue, 11 Dec, 2018, 02:05 MigMit, <migmit at gmail.com> wrote:
>> Same here!
>> 
>> Az iPademről küldve
>> 
>> 2018. dec. 10. dátummal, 21:32 időpontban Ara Adkins <me at ara.io> í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 <olf at aatal-apotheke.de> 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 <siddu.druid at gmail.com>:
>>>>> 
>>>>> 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.