Stratified polymorphism

The author considers a spectrum of predicative type abstraction disciplines based on type quantification with stratified levels. These lie in the vast middle ground between parametric abstraction and full impredicative abstraction. Stratified polymorphism has an attractive, unproblematic semantics, and has the potential of offering new approaches to type inference, without sacrificing useful expressive power. He shows that the functions representable in the finitely stratified λ-calculus are precisely the superelementary functions, i.e., E₄ in A. Grzegorczyk´s (Rozprawy Mate. IV, Warsaw, 1953) subrecursive hierarchy. He also defines methods of transfinite stratification and shows that stratification up to ω^ω has a simple finitary representation, making it a potentially useful concept in programming language design. The author proves that the functions represented by stratified polymorphism up to ω^ω are precisely the primitive recursive functions. He points out that these results imply that the equality problem for finitely stratified λ-calculus is not superelementary, and that the equality problem for the calculus stratified up to ω^ω is not primitive recursive