Problem # 17

Submitted by Paweł Urzyczyn
Date: 1999
Statement. Can recursive types be deﬁned in system $F$ ?

It was shown by Geuvers and Spławski that inductive types in the style of [Mendler, 1991] are deﬁnable in the polymorphic $βη$ -lambda-calculus. It is however an open question whether recursive types as in [Mendler, 1987] are also deﬁnable. In [Spławski and Urzyczyn, 1999] it is shown that system $F$ with $β$ -conversion only is not sufficient for this purpose. See also the paper [Regnier and Urzyczyn, 2001] and Problem 21.

References for # 17

[Mendler, 1987] Mendler, N. (1987). Recursive types and type constraints in second-order lambda calculus. In Logic in Computer Science, pages 30–36. IEEE Computer Society Press.

[Mendler, 1991] Mendler, N. (1991). Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51(1-2):159–172.

[Regnier and Urzyczyn, 2001] Regnier, L. and Urzyczyn, P. (2001). Retractions of types with many atoms. Technical Report 29, IML Marseille. http://arxiv.org/abs/cs/0212005.

[Spławski and Urzyczyn, 1999] Spławski, Z. and Urzyczyn, P. (1999). Type ﬁxpoints: Iteration vs. recursion. In International Conference on Functional Programming, pages 102–113. ACM Press.