6
$\begingroup$

There are many closed terms of a given type. For instance, both of these terms:

$$ \lambda x . x $$ $$ \lambda x . (\lambda y . y) x $$

have a type of a polymorphic identity function:

$$ \forall X . X \rightarrow X$$

On the other hand, there is only one normalized term of that type i.e: $\lambda x . x$. Similarly, given the type of Church natural numbers:

$$ \mathtt{Nat} = \forall X . (X \rightarrow X) \rightarrow X \rightarrow X $$

one can argue that all the normal form terms of type $\mathtt{Nat}$ are in the form:

$$\lambda s . \lambda z . s (\ldots (s\; z)) $$

Is there any research that goes along these lines and perhaps formalizes this intuition?

Is this idea correct and strong enough to prove (by case analysis on the normal forms of the terms) 'free theorems' or more general parametricity results?

Clarification: The type system in question is System F

$\endgroup$
  • 1
    $\begingroup$ Note that the $\eta$-expansion has to be included in the definition of the normal form. $\endgroup$ – Łukasz Lew Jan 23 at 3:54
  • 1
    $\begingroup$ A small aside: You need to specify the typing system you have in mind, because inhabitation strongly depend on the ambient typing system. Consider for example the (pure lambda-calculus versions of the) programs let rec f x = f x and throw new Exception ("Hello Mum") . What you have in mind is some variant of System F or F$\omega$. $\endgroup$ – Martin Berger Jan 23 at 10:31
  • 2
    $\begingroup$ I believe this is mostly folklore. See this blog post by Gabriel Scherer: prl.ccs.neu.edu/blog/2017/06/05/… $\endgroup$ – Max New Jan 23 at 13:25
  • 1
    $\begingroup$ @MartinBerger indeed, I've meant System F. $\endgroup$ – Łukasz Lew Jan 23 at 20:23
4
$\begingroup$

I thought this might be tough, given the fact that the proof usually goes in the other direction (Parametricity $\Rightarrow$ Normalization), and the post by Gabriel is somewhat involved, but in system F one can do a relatively straightforward induction.

I'm going to assume you're somewhat familiar with the usual statement of parametricty, e.g. from the "Theorems for free!" paper, and I'll treat only binary relations for simplicity.

I'll also be working in the "Curry-style" calculus for brevity.

Theorem: if $T(X)$ is a type in system F with (only) the free type variable $X$, then for any well-typed term $$ \vdash t : \forall X.T(X)$$ and any relation $\cal R$ between terms that respects $\beta\eta$, $$ t\ T({\cal R})\ t$$ where $T(\cal R)$ is the parametricity relation defined in the usual way by induction on the structure of types.

The proof requires a more general lemma, which will handle arbitrary amounts of type variables and term variables (rather than working in a closed context).

Let $\theta$ be a map from type variables to $\beta\eta$ respecting binary relations over terms, and if $\Gamma$ is a type context, then $\sigma$ is a map from variables $x$ to pairs of terms $(u_1, u_2)$ such that, if $x : U\in\Gamma$, then $u_1\ U\theta\ u_2$, i.e. $u_1$ and $u_2$ are related by the parametricity relation at the appropriate type (where $\theta$ is used to instantiate type variables).

Given this, the lemma then states:

Lemma: for any such $\theta, \Gamma, \sigma$, if $\Gamma \vdash t : T$, then $t\sigma_1\ T\theta\ t\sigma_2$. (With the obvious interpretation of $\sigma_i$ as a plain substitution).

Proof. First we note that $T\theta$ is closed under $\beta\eta$ conversion, so we may take the $\beta$-normal $\eta$-long normal form of $t$, and reason by induction on its size.

Now we reason by cases (not induction!) on the structure of $T$.

Base case: suppose $T=X$. The normal form of $t$ is also of type $X$ and the only possible form is $x\ t_1\ldots t_n$, with the $t_i$ in normal forms.

If t is just $x$, then $\sigma_1(x)\ X\theta\ \sigma_2(x)$ by construction.

Otherwise, by inversion the type of $x$ is $T'=T_1\rightarrow\ldots\rightarrow T_n\rightarrow X$. Now by construction, $\sigma_1(x)\ T'\theta\sigma_2(x)$, which means that $\sigma_1(x\ t_1\ldots t_n)\ \theta(X)\ \sigma_2(x\ t_1\ldots t_n)$ if $\sigma_1(t_i)\ T_i\theta\ \sigma_2(t_i)$. But this is exactly the induction hypothesis.

Suppose now that $T=T_1\rightarrow T_2$. We proceed similarly: take 2 arbitrary terms $u$ and $u'$ such that $u\ T_1\theta\ u'$. We need to show that $t\sigma_1\ u\ T_2\theta\ t\sigma_2\ u'$. But by inversion again, (and the definition of $\eta$-long forms), $t$ must be of the form $\lambda x.t'$, so $t'\sigma_1\ u\ =_{\beta\eta}\ t'\sigma_1'$, where $\sigma_1'$ is $\sigma_1$ extended with the mapping $x\mapsto u$, and similarly for $u'$.

The induction hypothesis applies again, using $\sigma'$ instead of $\sigma$.

Finally, if $T=\forall X.T'$, then inversion tells us that $\Gamma\vdash t:T'$, and $X$ does not appear free in $\Gamma$. This means we can take $\theta'$ to be $\theta$ extended with an arbitrary binding for $X$, which does not affect the correctness of $\sigma$, since $X$ does not appear in the types of any of the variables.

This gives $t\sigma_1\ T'\theta'\ t\sigma_2$ for an arbitrary such extension, implying $t\sigma_1\ T\theta\ t\sigma_2$, which concludes the proof.


I'm not 100% certain, but I suspect this proof can be carried out in some weak form of 2nd order arithmetic, which would show that normalization does imply parametricity in some strong sense.

$\endgroup$
  • $\begingroup$ Cody, thank you for working that out, I appreciate that. $\endgroup$ – Łukasz Lew Feb 17 at 7:28
5
$\begingroup$

I'd like to offer some pointers.

Is there any research that goes along these lines and perhaps formalizes this intuition?

Parametricity by analysis of the shape of (simply-typed) normal forms preceded by a normalisation argument was proposed by Girard, Scedrov, and Scott [1]. This connects parametricity, cut-elimination in logic, and a proof technique for coherence in category theory. Here, parametricity is understood as a property of dinaturality, originally proposed for system F in [2].

Is this idea correct and strong enough to prove (by case analysis on the normal forms of the terms) 'free theorems' or more general parametricity results?

In [1], it is noted that this includes the so-called "free theorems" as a special case. But the argument does not extend to all of system F, and dinaturality fails to capture relational parametricity (see e.g. [3]). On the other hand, a work by Paolo Pistone shows that one indeed thus obtains a syntactic characterisation of parametricity for a class of types a bit larger than the simple types including your examples [4]:

Our results imply that, for positive second order types, realizability, parametricity, dinaturality and typability are equivalent properties of closed normal lambda-terms.

So there is indeed an elementary technique based on looking at shapes of normal forms, which provides a syntactic characterisation of some parametricity results including the "free theorems", that also hints at a connection with categorical coherence.

[1]: Girard, J.-Y.; Scedrov, A. & Scott, P. J. Normal Forms and Cut-Free Proofs as Natural Transformations. Logic From Computer Science, Mathematical Science Research Institute Publications 21, Springer-Verlag, 1992, 217-241. http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.811

[2]: Bainbridge, E. S.; Freyd, P. J.; Scedrov, A. & Scott, P. J. Functorial polymorphism. Theoretical computer science, Elsevier, 1990, 70, 35-64. https://core.ac.uk/display/82270459

[3]: De Lataillade, J. Dinatural Terms in System F. Logic in Computer Science, 24th Annual IEEE Symposium, 267-276, 2009. https://www.irif.fr/~delatail/dinat.pdf

[4]: Pistone, P. On completeness and parametricity in the realizability semantics of System F. https://arxiv.org/abs/1802.05143

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.