Parametric polymorphism and contextual equivalence

	    (Subtitle: making you pay for those free theorems!)

		   Andrew M. Pitts (Cambridge University)


John Reynolds (1983) introduced a semantical notion of parametric
polymorphism, involving binary logical relations, in his study of
models of the second order lambda calculus (Girard's system F). It is
known from the work of Hasegawa (1991), Plotkin-Abadi (1993), and
Abadi-Cardelli-Curien (1993), that equality in models of second order
lambda calculus has very strong properties if the model supports a
Reynolds-style logical relation. For example, weak product and sum
types are actually categorical products and co-products, weakly
(co)inductive types are actually (co)final, Wadler's "theorems for
free" (Wadler 1989) hold, etc, etc.

Unfortunately, second order lambda calculus is a theory of *total*
polymorphic functions, and the above results are not immediately
applicable to Turing-powerful programming languages combining
recursion with polymorphism. Here it is shown how to overcome this
problem and reap the rather rich consequences of relational parametric
polymorphism for proving contextual equivalences between programs in
such languages.

Since denotational models of the combination of impredicative
polymorphism with unrestricted fixpoint recursion are necessarily
rather complicated (and ones supporting relational parametricity are
scarce), it makes sense to take a syntactic approach and develop a
suitable parametric logical relation directly on the terms of such a
language, making use of its operational semantics. My thesis is that
this can always be done in such a way that the operationally defined
notion of contextual equivalence coincides with the logical relation
"on the diagonal". In other words:

 "polymorphic types are relationally parametric up to contextual
  equivalence"

and from this many non-trivial properties of contextual equivalence
follow. 

We give some supporting evidence for this thesis by verifying it for a
"polymorphic PCF"---a non-strict language combining full second-order
lambda calculus with fixpoint recursion, in which observations of
evaluation are allowed only at inductive types (lazy list types, for
definiteness). The main technical innovation of the work is a rather
simple treatment of the "admissibility" properties of the syntactical
logical relation, extending the approach in (Pitts-Stark,
1997). Examples of application to proving properties of polymorphic
types up to contextual equivalence will be given.

References

M Abadi, L Cardelli, and P-L Curien (1993), Formal parametric
polymorphism. In Proc. POPL'93.

R Hasegawa (1991), Parametricity of extensionally collapsed term models of
polymorphism and their categorical properties. In LNCS vol. 526
(Springer-Verlag), pp 495--512.

AM Pitts and IDB Stark (1997), Operational Reasoning for Functions with
Local State. In A Gordon and A Pitts (Eds), Higher Order Operational
Techniques in Semantics (CUP, to appear), pp 227--273.

GD Plotkin and M Abadi (1993), A logic for parametric
polymorphism. In LNCS vol. 664 (Springer-Verlag), pp 361--375.

JC Reynolds (1983), Types, abstraction and parametric polymorphism. In
REA Mason (Ed), Information Processing '83 (North-Holland), pp
513--523. 

P Wadler (1989), Theorems for free!. In Proc. FPCA'89.