Stratified polymorphism
Daniel M. Leivant · 2003
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 lambda -calculus are precisely the superelementary functions, i.e., E/sub 4/ in A. Grzegorczyk's (Rozprawy Mate. IV, Warsaw, 1953) subrecursive hierarchy. He also defines methods of transfinite stratification and shows that stratification up to omega /sup omega / 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 omega /sup omega / are precisely the primitive recursive functions. He points out that these results imply that the equality problem for finitely stratified lambda -calculus is not superelementary, and that the equality problem for the calculus stratified up to omega /sup omega / is not primitive recursive.>