[Prev][Next][Index][Thread]

About parametricity

ABOUT PARAMETRICITY
The Genericity Theorem: a note by
 
 
        Giuseppe Longo     Kathleen Milsted    Sergei Soloviev
 
 
BACKGROUND
----------
 
As is well-known, the second order lambda-calculus (system F) allows
"computing with types", i.e., type variables may be lambda-abstracted
in terms (Lambda X . M), and terms may be applied to types (MA).
In his 71 paper, though, Girard remarked that, under certain circumstances,
input types "cannot modify output values".  More precisely, if one
takes a term  J such that, for types  A  and  B,  JB  is equal to
numeral 1 if  B = A  and is equal to 0 if  B /= A, then  F+J does
not normalize. As a consequence,  J  is not definable in F.  The
point here is that the polymorphic term  J  gives "essentially"
different output terms (different erasures), which live in the same
type, according to the (values of the) input types.
 
What can we say about arbitrary polymorphic terms  M  of type
ForAll X. D ?  How do they "depend" on input types?  The so-called
"proper" form of implicit and explicit polymorphism of lambda-calculus
(distinguished by Strachey from the so called "ad hoc"  polymorphism,
of, for example, overloading) has been largely investigated.
 
A semantic criterion for parametricity was proposed by
Reynolds as an invariance property under relations between type values.
 
Another meaning of the proper polymorphism of system F was given
by  Bainbridge&Freyd&Scedrov&Scott by interpreting terms as ``dinatural''
transformations, an elegant categorical notion derived from tensor
algebra and algebraic topology. (Unfortunately dinaturals happen
to  compose only in some models.)
 
More recent, proof theoretic work for an understanding of  parametricity
is due to Abadi&Curien&Cardelli (+Plotkin), where Wadler's "theorems-for-free"
idea can be fully formalized. Yet another recent syntactic understanding
of parametricity is due to Mairson.
 
 
WHAT WE PROPOSE
---------------
 
We announce here a one line theorem (requiring a 20 page proof),
which, in our view, gives a direct understanding of the phenomenon
of parametricty and relates, in various ways, to the work of the
authors quoted above.
 
First, add to II order lambda calculus (system F) the following axiom:
 
 
Axiom C:
 
MA = MB   if  M  has type  ForAll X.C  with  X  not free in  C.
 
 
That is, polymorphic terms, living in II order types which do NOT
contain free the universally quantified type variable, are constant.
Realizability or PER models, models on coherent spaces and stable
functions ... realize Axiom C. Indeed, all models that satisfy Reynolds'
parametricity conditions satisfy it. Call Fc this extension of F
with Axiom C. Then the following theorem holds:
 
 
GENERICITY THEOREM: (for II order lambda calculus)
 
Let  M,N  have type  ForAll X . D.  Then
 
if  Fc |- MA = NA  for some type A, one has  Fc |- M = N.
 
 
The Genericity Theorem says that if two second order terms
coincide on one type, they coincide everywhere (Note: no  restriction
on type D). Or, equivalently, that each single type acts as a ``generic''
input, as a variable.
 
A lot needs to be settled, in particular the semantics of the
implication in the theorem.
 
This work is reported in the soon available paper:
 
 
        The Genericity Theorem and the notion of Parametricity
                      in Polymorphic Languages
 
 
Authors:
    Giuseppe Longo (longo@dmi.ens.fr)
        LIENS-DMI, Ecole Normale Superieure, 45 rue d'Ulm, 75005
        Paris, FRANCE.
    Kathleen Milsted (milsted@prl.dec.com)
        Digital Equipment Corporation, Paris Research Laboratory, 85
        avenue Victor Hugo, 92563 Rueil-Malmaison, FRANCE.
    Sergei Soloviev (sergei@iias.spb.su)
        St. Petersburg Institute for Informatics and Automation, Russian
        Academy of Sciences, 14th line, 39, St. Petersburg, 199178, RUSSIA.