Finitely stratified polymorphism

AbstractWe consider predicative type-abstraction disciplines based on type quantification with finitely stratified levels. These lie in the vast middle ground between quantifier-free parametric abstraction and full impredicative abstraction. Stratified polymorphism has an unproblematic set-theoretic semantics, and may lend itself to new approaches to type inference, without sacrificing useful expressive power. Our main technical result is that the functions representable in the finitely stratified polymorphic λ-calculus are precisely the super-elementary functions, i.e., the class ε4 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 λ-expressions is not super-elementary. We also observe that finitely stratified polymorphism augmented with type recursion admits functional algorithms that are not typable in the full second order λ-calculus