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
On 2004-06-10 at 10:39BST Martin Escardo wrote:
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.
Interesting. But why do you use Int rather than the Integer? In particular
This gives some surprising results, e.g. that the type ((Int->Bool)->Int) has decidable equality (for total elements).
is not at all surprising, since Int (and Bool) is finite, so there are only finitely many total elements of that type :-) For Integer it is surprising, but I haven't read that far yet... Jón -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk
Dear Jon, Thanks for your remarks. Jon Fairbairn writes:
Interesting. But why do you use Int rather than the Integer?
Ok, I admit that I should have used Integer. Moreover, in practice you would like to use [a] when I use (Int -> a), as you'll notice.
In particular
This gives some surprising results, e.g. that the type ((Int->Bool)->Int) has decidable equality (for total elements).
is not at all surprising, since Int (and Bool) is finite, so there are only finitely many total elements of that type :-) For Integer it is surprising,
Let me add that I don't count "seq" as part of the language, so that two functions are equal iff they are equal at all arguments (i.e., functions are functions). But, with more trouble, it is possible to consider the full language, although I don't find this particularly illuminating. Martin
participants (2)
-
Jon Fairbairn -
Martin Escardo