[Haskell-cafe] References for topological arguments of programs?
ryan.reich at gmail.com
Mon Dec 10 21:53:07 UTC 2018
I think I'd be interested in seeing your work-in-progress.
On Mon, Dec 10, 2018 at 12:29 PM Olaf Klinke <olf at aatal-apotheke.de> wrote:
> I highly recommend the So-called "Barbados notes"  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.
>  Synthetic Topology: of Data Types and Classical Spaces
> 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:
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe