Relational parametricity and local variables

ABSTRACT

J. C. Reynolds suggested that Strachey's intuitive concept of “parametric” (i.e., uniform) polymorphism is closely linked to representation independence, and used logical relations to formalize this principle in languages with type variables and user-defined types. Here, we use relational parametricity to address long-standing problems with the semantics of local-variable declarations, by showing that interactions between local and non-local entities satisfy certain relational criteria. The new model is based on a cartesian closed category of “relation-preserving” functors and natural transformations which is induced by a suitable category of “possible worlds” with relations assigned to its objects and morphisms. The semantic interpretation supports straightforward validations of all the test equivalences that have been proposed in the literature, and encompasses standard methods of reasoning about data representations; however, it is not known whether it is fully abstract.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.2 Language Classifications

          Nouns: ALGOL
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures; Procedures, functions, and subroutines

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs

General Terms:
Algorithms, Languages