[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On 30/11/14 22:05, Izaak Meckler wrote:
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Hi all, Does anyone know any resources describing the topology of the (say, Haskell 98) type given by data T = T (T -> T) This is something like the type of untyped lambda calculus programs. The topology I have in mind is defined as follows. A subset X of T is open set if there is a Haskell term f :: T -> () with f x = () for x in A, and f x = undefined otherwise. The topology on T is the one generated by these open sets (generated in the classical sense, although I'd be interested also in the case where the unions are required to be definable functions out of Nat as described by Martin Escardo here <http://www.cs.bham.ac.uk/%7Emhe/papers/entcs87.pdf>, p. 33). It is not hard to show that T has non-trivial topology (for example, there are open sets separating the two church booleans) and it seems it's not compact. I'd appreciate any other info people have on this topology.
The references Guy gave you should help you to describe the topology more explicitly. Just one comment: the topology is compact, simply because there is a bottom element in the domain. The same is true for the type of integers: it is compact because it has a bottom. What is not true for the type of integers is that the total elements form a compact set (related to the Halting Problem). You could ask whether the total elements of T form a compact set. But we first have to agree what the total elements of T are/should be. Back in 1997 in a domains workshop in Munich, Gordon Plotkin showed that there is no reasonable notion of totality for such a domain, if I remember correctly. But he didn't write this up, as far as I know. Best wishes, Martin
