[Prev][Index][Thread]

Parametricity and variants of Girard's J operator



We have written a short (5 page) note on parametricity and
Girard's J operator in impredicative polymorphic systems.
This is available by anon ftp from theory.stanford.edu,
file pub/jcm/girard-j.dvi, or through the web page
http://theory.stanford.edu/people/jcm/home.html

-------------------------------------------------------------------


      Parametricity and variants of Girard's $J$ operator

             Robert Harper and John Mitchell
                     Dec 29, 1994


                         SUMMARY

The impredicative polymorphic lambda calculus, or System F,
is generally recognized as a calculus of parametric polymorphism.
Intuitively, this means that the polymorphic functions definable 
in the language must use the same algorithm at all types. There 
are no non-parametric functions such as a single multiplication 
function that computes an inner product on vectors, ordinary product 
on natural numbers and similar or unrelated ``products'' on other types.

In his 1971 paper, Girard discusses parametricity in System F and 
gives an example showing that if we add a non-parametric operator to
the calculus, normalization fails.  This example has been interpreted 
as a demonstration that System F is inherently a calculus of parametric 
functions. Specifically, since adding a non-parametric operator alters 
a fundamental property of the system, we can conclude the System F is
inherently parametric. However, this interpretation of the example relies on
the implicit assumption that J is as simple a non-parametric
operator as possible. If it is possible to add a simpler non-parametric
operator to System F in a manner that preserves strong normalization,
we could not really say that Girard's example convincingly demonstrates 
the parametric nature of System F. In this short note, we give some 
variants of Girard's example, hoping to more clearly identify the kind 
of non-parametric operations that invalidate normalization.
In the concluding remarks, we observe that impredicativity appears essential.

One possible reservation regarding Girard's example is that it combines
non-parametric functions with a change in the typing properties
of the language. More specifically, the type of $J$ is  
$\fa s. \fa t. s \aro t$, which is not  the type of any pure closed
term of System F since it is not a provable propositional formula.
The non-normalizing term constructed using $J$ also seems to
require a term  $0: \fa t.t$. Again, there are no pure
closed terms with type $0: \fa t.t$. 
This led us to formulate the following question:
 
   Is there a simple non-parametric operator Op :\sigma such that
      (i) there exist pure closed terms of type \sigma, and 
     (ii) adding Op to System F causes normalization to fail?

We settle this question affirmatively and give a simple example, J'. 
Our goal is to dispel the possible misconception that in impredicative 
systems, Girard's example is simply a ``typing trick'' that
could not be carried out with other non-parametric operations.

One consequence of replacing J by an operator whose type already contains pure
closed terms is that we can easily show that the fixed-point operator is not
definable.  More specifically, suppose Op : \sigma$ and there
exists a pure closed term of type \sigma.  Then using the formulas-as-types
analogy, we can show that there exists a closed term of type
\tau containing Op iff there exists a pure closed term of type \tau
not containing Op.  The argument is simply that if we add a new axiom for
a formula that is already provable, we do not change the set of provable
formulas.  Since \fa t.(t \aro t)\aro t is not a provable formula of
intuitionistic logic, there is no pure closed term of this type.  
It follows that when the type of Op contains pure closed
terms, no closed term of type \fa t.(t \aro t)\aro t is definable from Op.  
In particular, since the fixed-point operator $Y$ has this type, Y
is not definable from J'.  In light of various studies relating logical
paradoxes and fixed-point operators, it does not seem easy to establish 
that no fixed-point operator or ``looping combinator'' is definable from J.