[TYPES] Topology of the type T = T -> T

[Izaak Meckler]

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