Finitely Stratified Polymorphism

Abstract: "We consider predicative type-abstraction disciplines based on type quantification with finitely stratified levels. The main technical result is that the functions representable in the finitely stratified polymorphic [lambda]-calculus are precisely the super-elementary functions, i.e. the class E4 in Grzegorczyk's subrecursive hierarchy. This implies that there is no super-elementary bound on the length of optimal normalization sequences, and that the equality problem for finitely stratified polymorphic [lambda]-expressions is not super-elementary. We also observe that finitely stratified polmorphism augmented with type recursion admits functional algorithms that are not typable in the full second order [lambda]-calculus."