Semantics of Parametric Polymorphism in Imperative Programming Languages
Programming languages such as CLU, Ada and Modula-3 have included facilities for parametric polymorphism and, more recently, C++ and Java have also added similar facilities. In this paper, the authors examine the issues of defining denotational semantics for imperative programming languages with polymorphism. They use the framework of reflexive graphs of categories previously developed for a general axiomatization of relational parametricity constraints implicit in polymorphic functions. They specialize it to the context of imperative programming languages, which in turn involve parametricity constraints implicit in local variables. The two levels of parametricity inherent in such languages can be captured in a pleasing way in "Higher-order" reflexive graphs.