7
$\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$
4
  • 1
    $\begingroup$ Note that the $\eta$-expansion has to be included in the definition of the normal form. $\endgroup$ Jan 23, 2019 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$ Jan 23, 2019 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, 2019 at 13:25
  • 1
    $\begingroup$ @MartinBerger indeed, I've meant System F. $\endgroup$ Jan 23, 2019 at 20:23

2 Answers 2

5
$\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$
1
  • $\begingroup$ Cody, thank you for working that out, I appreciate that. $\endgroup$ Feb 17, 2019 at 7:28
7
$\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 obtains with a “syntactic” notion of dinaturality a characterisation of parametricity for positive types (system F types whose quantifiers are in positive positions), including your example: “in the case of positive types, realizability, invariance with respect to logical relations, dinaturality and typability are equivalent properties for closed normal λ-terms” [4, §7.1].

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. Logical Methods in Computer Science, October 29, 2019, Volume 15, Issue 4. https://doi.org/10.23638/LMCS-15(4:6)2019

$\endgroup$
6
  • $\begingroup$ The paper [3] proves dinaturality by the analysis of normal forms of lambda-terms. This is sufficient to prove that there is only one function of type $\forall X.\,X\to X$ in System F. However, as pointed out already, dinaturality is weaker than full relational parametricity. For example, dinaturality is insufficient to prove that $\forall X.\,(X\to X)\to X\to X$ is equivalent to natural numbers. For that, you need something stronger. Short of full relational law, the property called "strong dinaturality" is sufficient for Church numbers. But it will be still insufficient for other cases. $\endgroup$
    – winitzki
    Sep 30, 2022 at 9:20
  • $\begingroup$ Thanks, I have made some clarifications. First, I have restored the quote of [4] to mention like in my original answer the link with dinaturality (the original quote has changed between the preprint and the published version). Second, I have mentioned that [4] uses a so-called "syntactic" version of dinaturality for System F. This variant of dinaturality seems sufficent for Church numerals (Example 6.10 in [4]). With this in mind, we can still ask whether Theorem 6.16 in [4] (which generalizes the one in [1] to positive types) can be proved directly by looking at the shape of normal forms. $\endgroup$
    – gadmm
    Oct 2, 2022 at 20:30
  • $\begingroup$ I meant Theorem 6.18 in [4]. $\endgroup$
    – gadmm
    Oct 2, 2022 at 20:48
  • $\begingroup$ I looked at Example 6.10 in [4]. The paper only shows that the Church numeral terms satisfy dinaturality. They do satisfy it. However, dinaturality is not sufficient for proving that the type of terms $\forall X.,(X\to X)\to X \to X$ is equivalent to the inductive type of natural numbers. $\endgroup$
    – winitzki
    Jan 6, 2023 at 18:33
  • $\begingroup$ Right, my answer does not address the first question. It addresses the second one. It might be worthwhile developing your comment into a reply. $\endgroup$
    – gadmm
    Jan 8, 2023 at 21:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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