[ 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. Thanks, Izzy
