[Haskell] topology in Haskell

[Martin Escardo]

Dear Haskell-list members,

This is to advertise the monograph

 Synthetic topology of data types and classical spaces, to appear in
 ENTCS 87, 150pp, three parts, 6+5+2 chapters.

 http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf (or .dvi or .ps)

Chapter 3 develops topology in Haskell, without assuming any previous
knowledge of topology. Notions of topology such as space, continuous
map, open set, closed set, discrete space, Hausdorff space, compact
space are defined directly in the programming language. Theorems in
topology are proved by writing programs.  The development here is
purely operational.

This gives some surprising results, e.g. that the type
((Int->Bool)->Int) has decidable equality (for total elements).

Chapter 12 has more sophisticated computational applications, which
invoke classical topology with the aid of denotational semantics. We
apply the Tychonoff theorem of classical topology to show that a
certain (we hope surprising) Haskell program has the correct
termination properties.

Martin Escardo