[Prev][Next][Index][Thread]
Parametricity and Local Variables
The following paper is available by anonymous ftp from top.cis.syr.edu
in ohearn/plv.dvi
Parametricity and Local Variables
P. W. O'Hearn and R. D. Tennent
We propose that the phenomenon of local state may be understood
in terms of Strachey's concept of parametric (i.e., uniform)
polymorphism. The intuitive basis for our proposal is the following
analogy: a non-local procedure is independent of locally-declared
variables in the same way that a parametrically polymorphic function
is independent of types to which it is instantiated.
A connection between parametricity and representational abstraction
was first suggested by J.\,C.~Reynolds. Reynolds used logical
relations to formalize this connection in languages with type
variables and user-defined types. We use relational parametricity
to construct a model for an Algol-like language in which interactions
between local and non-local entities satisfy certain relational
criteria. Reasoning about local variables essentially involves
proving properties of polymorphic functions. The new model supports
straightforward validations of all the test equivalences that have
been proposed in the literature for local-variable semantics,
and encompasses standard methods of reasoning about data
representations. It is not known whether our techniques yield fully
abstract semantics. A model based on partial equivalence relations
on the natural numbers is also briefly examined.
This is an expansion and elaboration of material from
the preliminary report "Relational Parametricity and Local Variables",
which appeared in POPL93.