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

[Guy McCusker]

On 30 Nov 2014, at 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 semantics of this type were studied quite closely by Abramsky and Ong in their work on the lazy lambda-calculus. I don't know if this work will answer your question but it is surely worth a look. Some references: 

S. Abramsky, C.H.L. Ong, Full Abstraction in the Lazy Lambda Calculus, Information and Computation, Volume 105, Issue 2, August 1993, Pages 159-267, ISSN 0890-5401, http://dx.doi.org/10.1006/inco.1993.1044.
(http://www.sciencedirect.com/science/article/pii/S0890540183710448)

Samson Abramsky. 1990. The lazy lambda calculus. In Research topics in functional programming, David A. Turner (Ed.). Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA 65-116.
(http://www.cs.ox.ac.uk/samson.abramsky/lazy.pdf)

C.-H. L. Ong, Lazy Lambda Calculus: Theories, Models and Local Structure Characterization. In Proceedings of 19th International Colloquium on Automata, Programming and Languages (ICALP 1992), Springer-Verlag, Lecture Notes in Computer Science Volume 623, 1992. (ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Luke.Ong/pse.ps.gz)

Guy.