<p>We can simplify the five type expressions given in the question. But we need to use different methods for these cases. Parametricity theorems give us a law that a value will satisfy, but we are not always able to derive useful information from those laws directly. We need other techniques.</p>
<p>One technique looks like this: given a type constructor <span class="math-container">$F$</span> check whether <span class="math-container">$F \,\textrm{Void} \cong \textrm{Void}$</span>. It turns out that then we also have <span class="math-container">$\forall a.\,F\,a \cong \textrm{Void}$</span>.</p>
<p>The reason is that a value of type <span class="math-container">$\forall a.\,F\,a $</span> is supposed to work in the same way for every type <span class="math-container">$a$</span>, including the Void type. For every type <span class="math-container">$a$</span> there must be a value of type <span class="math-container">$F\,a$</span>. If <span class="math-container">$F \,\textrm{Void} \cong \textrm{Void}$</span> then we cannot have a value of type <span class="math-container">$F\,a$</span> for some <span class="math-container">$a$</span>, which means that the type <span class="math-container">$\forall a.\,F\,a$</span> has no values (is void).</p>
<p>Now we apply this technique to the five cases (assuming that the fixed types <span class="math-container">$r$</span> and <span class="math-container">$s$</span> are not themselves Void). We find that setting <span class="math-container">$a = \textrm{Void}$</span> we get Void for the following types:</p>
<p><span class="math-container">$$ \forall a.\, (a \to r)  \to a $$</span></p>
<p><span class="math-container">$$ \forall a.\, (a \to a)  \to a $$</span></p>
<p><span class="math-container">$$ \forall a.\, ((a \to r)  \to s) \to a $$</span></p>
<p>It means that these three types are void (uninhabited).</p>
<p>The question about this type:</p>
<p><span class="math-container">$$ F\, r = \forall a.\, ((a \to r)  \to a) \to a $$</span></p>
<p>is much more complicated. It turns out that <span class="math-container">$ F\,r \cong r$</span>. Here is a solution:</p>
<p>First, use the contravariant Yoneda identity to get:
<span class="math-container">$$  ((a \to r)  \to a) \to a \cong \forall b.\, (b\to a)\to ((b \to r)  \to a) \to a $$</span></p>
<p>This allows us to rewrite the type <span class="math-container">$F\,r$</span> equivalently as:</p>
<p><span class="math-container">$$ F \, r = \forall a.\, \forall b.\, (b\to a)\to ((b \to r)  \to a) \to a $$</span></p>
<p>Exchange the quantifiers and uncurry some arguments:</p>
<p><span class="math-container">$$ F\,r = \forall b.\, \forall a.\, ((b + (b\to r))\to a)\to a $$</span></p>
<p>Use the covariant Yoneda identity:
<span class="math-container">$$ \forall a. \, (x \to a)\to a \cong x $$</span></p>
<p>and simplify <span class="math-container">$F\, r$</span> further:</p>
<p><span class="math-container">$$ F\,r = \forall b.\,  b + (b\to r)  $$</span></p>
<p>Now use the &quot;disjunctivity lemma&quot; (see at the end of my answer to <a href="https://cstheory.stackexchange.com/questions/53855/">Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?</a>) and simplify:</p>
<p><span class="math-container">$$ F\, r = (\forall b.\,  b) + (\forall b.\,  b\to r) $$</span></p>
<p>By the Yoneda identity again, we simplify <span class="math-container">$\forall b. \, b \cong\mathrm{Void}$</span> and <span class="math-container">$\forall b.\, b\to r \cong \mathbb1 \to r\cong r$</span>.
So, we have finally:
<span class="math-container">$$ F\, r \cong \mathrm{Void} + r \cong r$$</span></p>
<p>Simplifying the type <span class="math-container">$\forall a.\,((a\to a)\to a)\to a$</span> can be done via a similar derivation shown in my answer here: <a href="https://cstheory.stackexchange.com/questions/53855/">Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?</a></p>

CC BY-SA 4.0
2022-10-06T11:36:44.907Z
2024-04-02T21:35:06.720Z
2024-04-02T21:35:06.720Z
winitzki
<p>Another proof technique that is more intuitive <a href="https://prl.khoury.northeastern.edu/blog/2017/06/05/syntactic-parametricity-strikes-again/" rel="nofollow noreferrer">in my biased opinion</a> is to enumerate normal forms of System F terms of the given type.</p>
<p>The most interesting example among those five given is <span class="math-container">$\forall a. ((a \to r) \to a) \to a$</span>.</p>
<ol>
<li><p>A term (or derivation) of <span class="math-container">$\vdash \forall a. ((a \to r) \to a) \to a$</span> in <span class="math-container">$\beta\eta$</span>-normal form must start with introduction rules. There is only one way forward.</p>
</li>
<li><p>An open term of <span class="math-container">$a : \star, x : (a \to r) \to a \vdash a$</span> in <span class="math-container">$\beta\eta$</span>-normal form can only be an application of a variable (because a <span class="math-container">$\beta$</span>-normal form is a head-normal form). There is only <span class="math-container">$x$</span>, which expects one argument.</p>
</li>
<li><p>A term of <span class="math-container">$a : \star, x : \dots \to a \vdash (a \to r)$</span> in <span class="math-container">$\beta\eta$</span>-normal form must start with an introduction rule.</p>
</li>
<li><p>Since there were no choices to be made in the previous steps, we have thus obtained a bijection between terms of <span class="math-container">$\vdash \forall a. ((a \to r) \to a)$</span> and terms of <span class="math-container">$a : \star, x : \dots \to a, y : a \vdash r$</span>, which can be closed into terms of type <span class="math-container">$\forall a. (\dots \to a) \to a \to r$</span>.</p>
</li>
<li><p>Concluding with standard argument by semantic parametricity, that is isomorphic to <span class="math-container">$r$</span>.</p>
</li>
</ol>

CC BY-SA 4.0
2024-04-06T09:32:25.307Z
This is an interesting technique. I have seen that blog post by G. Scherer and yourself. But I still have questions about that technique. 1) At step 4 you still require a relational parametricity argument (or Yoneda's identity) to show that $\forall a.\,((a\to r)\to a)\to a\to r \cong r$? 2) Would that technique also apply to all other examples in my question and, in particular, to $\forall a.\,((a\to a)\to a)\to a)$? At some point I thought I was able to prove that there was only one term of that type, because I thought there was only one proof in normal form, but I was wrong about that.
winitzki
CC BY-SA 4.0
2024-04-07T22:16:51.593Z
1. Yes, I don't know how to make that argument syntactically. My point is, in the cases where syntactic parametricity does apply, even if incomplete, it makes things simpler. 2. Yes. For $((a \to a) \to a) \to a$ I just haven't come up with a recipe to distinguish the normal forms thus enumerated, but at the very least, writing down the decision tree like I did makes it obvious that there are more than 2 normal forms. For $(a \to a) \to a$ you run into an infinite descent which implies there is no solution. And for the two others the enumeration terminates immediately.
Li-yao Xia
CC BY-SA 4.0
2024-04-12T07:43:06.413Z
What is the difficulty for $\forall a.\, (...)\to a \to r \cong r$? Is the syntactic technique unable to deal with fixed types (such as $r$ here)? I am getting an impression that the syntactic parametricity technique is good only for terms of the form $\forall a.\, P a$ where $P$ depends only on $a$ and contains no other types.
winitzki
CC BY-SA 4.0
2024-04-12T08:20:30.577Z
Now that I think about it in the semantic argument, you never say what the semantic model is. You basically postulate that it somehow internalizes many categorical concepts (notably that polymorphic functions satisfy naturality). But you can instantiate it with the syntactic model, so any "semantic parametricity" argument is actually also a syntactic parametricity argument.
Li-yao Xia
CC BY-SA 4.0
2024-04-12T12:12:04.297Z
To me, the important question is what techniques of derivation do we have for solving various problems. The question of model theory is not directly relevant. Suppose we implement a System F interpreter as a specific computer program. Then some kind of semantic model will exist in the computer. And, most likely, that model will be based on sets, because everything in a computer's memory is a set. Maybe theorists have trouble with set-theoretic models of polymorphic lambda calculus, but that only says that the theorists haven't done their job properly, because our program already works.
winitzki
CC BY-SA 4.0
2024-04-12T14:45:49.720Z
So, I'm quite interested to learn the syntactic parametricity techniques, if those techniques help me get the correct solution easier than other ways. In this case, I was able eventually to get the answer without any guessing just by using what you call the "semantic" parametricity.
winitzki
CC BY-SA 4.0
2024-04-05T00:38:49.587Z
2024-04-05T00:38:49.587Z
Li-yao Xia
<p>This question is similar to <a href="https://cstheory.stackexchange.com/questions/51932/can-we-use-relational-parametricity-to-simplify-the-type-forall-a-a-to-r/51944">Can we use relational parametricity to simplify the type $\forall a. ( (a \to r) \to r ) \to (a \to r) \to r$?</a> but looks more complicated. It is about using relational parametricity to resolve practical questions in pure functional programming in System F.</p>
<p>Consider the following types of polymorphic functions:</p>
<p><span class="math-container">$$ \forall a.\, (a \to r)  \to a $$</span></p>
<p><span class="math-container">$$ \forall a.\, (a \to a)  \to a $$</span></p>
<p><span class="math-container">$$ \forall a.\, ((a \to a)  \to a) \to a $$</span></p>
<p><span class="math-container">$$ \forall a.\, ((a \to r)  \to a) \to a $$</span></p>
<p><span class="math-container">$$ \forall a.\, ((a \to r)  \to s) \to a $$</span></p>
<p>where <span class="math-container">$r$</span> and <span class="math-container">$s$</span> are free type variables, i.e., fixed arbitrary types. Here we only consider pure lambda terms from System F, there are no side effects, all code is fully parametric, and so the parametricity theorems apply.</p>
<h2>Question</h2>
<p>Under these assumptions, can we simplify these types? What methods are available for this task? Presumably, either we can find simpler equivalent types that have no type quantifiers, or we cannot find such a general simplification (because different models of System F will have different results?).</p>
<h3>Discussion</h3>
<p>Let me show how I proved the the first two types are void.</p>
<p>I denote the void type by <span class="math-container">$\underline0$</span> and the unit type by <span class="math-container">$\underline1$</span>.</p>
<h2>First example</h2>
<p>The first type, <span class="math-container">$\forall a.\, (a \to r)  \to a$</span>, is of the form <span class="math-container">$(\forall a.\,F\,a)$</span> where <span class="math-container">$F$</span> is a covariant functor. The covariant Yoneda lemma shows that <span class="math-container">$(\forall a.\,F\,a)$</span> is equivalent to <span class="math-container">$F\, \underline0$</span>. So, we find:</p>
<p><span class="math-container">$$ \forall a.\, (a \to r) \to a  \cong \forall a.\,F\,a \cong F\,\underline0 = (\underline0\to r)\to\underline0 \cong \underline1\to\underline0 \cong \underline0$$</span></p>
<h2>Second example</h2>
<p>To show that the type <span class="math-container">$\forall a.\, (a \to a) \to a$</span> is void, we cannot use the Yoneda lemma. Instead, we need to use the full parametricity theorem with carefully chosen types and relations. I have a shorter proof using something called &quot;strong dinaturality&quot; but this is not a widely known technique, so let me stick to straightforward relational reasoning.</p>
<p>The parametricity theorem says that any value <span class="math-container">$\phi : \forall a.\, (a \to a) \to a$</span> is in a certain relation with itself, the relation being the lifting of the identity relation to the type <span class="math-container">$\forall a.\, (a \to a) \to a$</span>. Denote by superscript the type application, so <span class="math-container">$\phi^a$</span> is the function <span class="math-container">$\phi$</span> specialized to the type <span class="math-container">$a$</span>.
So, I write <span class="math-container">$\phi^a : (a \to a) \to a$</span>.
To write down the relational parametricity law, we need to lift the identity relation explicitly to the type <span class="math-container">$\forall a.\, (a \to a) \to a$</span>. After some calculation, we find that, for any types <span class="math-container">$a$</span> and <span class="math-container">$b$</span> and any relation <span class="math-container">$r$</span> between values of types <span class="math-container">$a$</span> and <span class="math-container">$b$</span>, the function <span class="math-container">$\phi$</span> must satisfy:</p>
<p><span class="math-container">$$ \forall p: a\to a, q: b\to b. \, \textrm{ if } (p,q)\in s \textrm{ then } (\phi^a(p), \phi^b(q))\in r $$</span></p>
<p>where the relation <span class="math-container">$s$</span> is defined between values of types <span class="math-container">$a\to a$</span> and <span class="math-container">$b\to b$</span> as follows: For any <span class="math-container">$p: a\to a$</span> and <span class="math-container">$q: b\to b$</span>, the values <span class="math-container">$p$</span> and <span class="math-container">$q$</span> are in relation <span class="math-container">$s$</span> if and only if:</p>
<p><span class="math-container">$$ \forall x: a, y: b.\,\textrm { if } (x, y)\in r\textrm{ then }(p(x), q(y))\in r$$</span></p>
<p>Now we apply this condition to the types chosen as follows: <span class="math-container">$a = \underline0$</span>, <span class="math-container">$b$</span> remains arbitrary, <span class="math-container">$r$</span> is the empty relation. Then <span class="math-container">$(x,y)\in r$</span> never holds for any <span class="math-container">$x:a$</span> and <span class="math-container">$y:b$</span>, since the type <span class="math-container">$a$</span> is void.</p>
<p>It follows that any two functions <span class="math-container">$p: a\to a$</span> and <span class="math-container">$q: b\to b$</span> are always in the relation <span class="math-container">$s$</span>. Indeed, there are never any values <span class="math-container">$x:a$</span> and <span class="math-container">$y:b$</span> for which <span class="math-container">$(x,y)\in r$</span>, so the condition for <span class="math-container">$(p,q)\in s$</span> is a condition of the form &quot;if false then ...&quot;. That formula is always true.</p>
<p>Now, <span class="math-container">$p$</span> must be of type <span class="math-container">$\underline0 \to\underline0$</span> and there is only one such <span class="math-container">$p$</span>: the empty function. But <span class="math-container">$q: b\to b$</span> is still arbitrary.</p>
<p>Then the relational parametricity law of <span class="math-container">$\phi$</span> says that for arbitrary <span class="math-container">$q: b\to b$</span> we must have:</p>
<p><span class="math-container">$$ (\phi^a(p), \phi^b(q))\in r $$</span></p>
<p>Now, <span class="math-container">$\phi^b(q)$</span> is the value of <span class="math-container">$\phi$</span> for a specific argument <span class="math-container">$q$</span>. But <span class="math-container">$r$</span> is an empty relation to which no values may belong. This contradicts the assumption that a function <span class="math-container">$\phi$</span> exists. So, there are no functions <span class="math-container">$\phi$</span> of type <span class="math-container">$\forall a\,(a\to a)\to a$</span> that satisfy the relational parametricity law.</p>
<p>More generally, I can prove the type equivalence:</p>
<p><span class="math-container">$$ \forall a.\,(a \to a)\to F\,a \cong F\,\underline 0 $$</span></p>
<p>when <span class="math-container">$F$</span> is a covariant functor. I write the relational law with the type <span class="math-container">$a=\underline0$</span> and find that any function <span class="math-container">$\phi$</span> of type <span class="math-container">$ \forall a.\,(a \to a)\to F\,a $</span> must ignore its argument (of type <span class="math-container">$a\to a$</span>). Then the type <span class="math-container">$ \forall a.\,(a \to a)\to F\,a $</span> is effectively equivalent to just <span class="math-container">$\forall a.\,F\,a$</span>, which is in turn equivalent to <span class="math-container">$F\,\underline0$</span>.</p>
<p>However, these techniques do not apply to the other types listed at the beginning of this post.</p>

CC BY-SA 4.0
2022-09-30T07:20:21.490Z
When you say "p must be of type 0 -> 0 and there is only one such p: the empty function", I think you meant "the identity function"?  Your conclusion still holds as you can't extract a value out of an arbitrary endomorphism, which is what the type asks for.
Jacques Carette
CC BY-SA 4.0
2022-09-30T08:54:03.557Z
Yes, we have the intuition that "one can't extract information from an arbitrary value of type $a\to a$". But the whole problem here is to convert this intuition into a precise proof. To your comment about the function $p$: There is only one function of type $\underline 0\to\underline0$. I described it as an "empty function" because that function does not have any function body and is never applied to any arguments. You can also think of it as an "identity function for the type $\underline0$". It's still going to be the same function. The type $\underline0\to\underline0$ is equivalent to unit.
winitzki
CC BY-SA 4.0
2024-04-05T00:18:43.290Z
A relevant paper is [Logarithm and program testing](https://favonia.org/files/logarithm.pdf).
Li-yao Xia
CC BY-SA 4.0
2024-04-12T07:40:19.770Z
As far as I understood the "Logarithm" paper, their technique will sometimes produce a slightly larger type than necessary. Their focus is on testing, and for testing that's perfectly fine. But it's not so good for deriving type equivalence.
winitzki
<functional-programming><typed-lambda-calculus><parametricity>
Can we use relational parametricity to simplify the type $\forall a.\,((a\to r)\to a)\to a$ and similar types?
winitzki
# Can we use relational parametricity to simplify the type $\forall a.\,((a\to r)\to a)\to a$ and similar types?

(Asked by: username_0 on 2022-09-29)

This question is similar to [Can we use relational parametricity to simplify the type $\forall a. ( (a \to r) \to r ) \to (a \to r) \to r$?](https://cstheory.stackexchange.com/questions/51932/can-we-use-relational-parametricity-to-simplify-the-type-forall-a-a-to-r/51944) but looks more complicated. It is about using relational parametricity to resolve practical questions in pure functional programming in System F.

Consider the following types of polymorphic functions:

$$ \forall a.\, (a \to r) \to a $$

$$ \forall a.\, (a \to a) \to a $$

$$ \forall a.\, ((a \to a) \to a) \to a $$

$$ \forall a.\, ((a \to r) \to a) \to a $$

$$ \forall a.\, ((a \to r) \to s) \to a $$

where $r$ and $s$ are free type variables, i.e., fixed arbitrary types. Here we only consider pure lambda terms from System F, there are no side effects, all code is fully parametric, and so the parametricity theorems apply.

## Question

Under these assumptions, can we simplify these types? What methods are available for this task? Presumably, either we can find simpler equivalent types that have no type quantifiers, or we cannot find such a general simplification (because different models of System F will have different results?).

### Discussion

Let me show how I proved the the first two types are void.

I denote the void type by $\underline0$ and the unit type by $\underline1$.

## First example

The first type, $\forall a.\, (a \to r) \to a$, is of the form $(\forall a.\,F\,a)$ where $F$ is a covariant functor. The covariant Yoneda lemma shows that $(\forall a.\,F\,a)$ is equivalent to $F\, \underline0$. So, we find:

$$ \forall a.\, (a \to r) \to a \cong \forall a.\,F\,a \cong F\,\underline0 = (\underline0\to r)\to\underline0 \cong \underline1\to\underline0 \cong \underline0$$

## Second example

To show that the type $\forall a.\, (a \to a) \to a$ is void, we cannot use the Yoneda lemma. Instead, we need to use the full parametricity theorem with carefully chosen types and relations. I have a shorter proof using something called "strong dinaturality" but this is not a widely known technique, so let me stick to straightforward relational reasoning.

The parametricity theorem says that any value $\phi : \forall a.\, (a \to a) \to a$ is in a certain relation with itself, the relation being the lifting of the identity relation to the type $\forall a.\, (a \to a) \to a$. Denote by superscript the type application, so $\phi^a$ is the function $\phi$ specialized to the type $a$.
So, I write $\phi^a : (a \to a) \to a$.
To write down the relational parametricity law, we need to lift the identity relation explicitly to the type $\forall a.\, (a \to a) \to a$. After some calculation, we find that, for any types $a$ and $b$ and any relation $r$ between values of types $a$ and $b$, the function $\phi$ must satisfy:

$$ \forall p: a\to a, q: b\to b. \, \textrm{ if } (p,q)\in s \textrm{ then } (\phi^a(p), \phi^b(q))\in r $$

where the relation $s$ is defined between values of types $a\to a$ and $b\to b$ as follows: For any $p: a\to a$ and $q: b\to b$, the values $p$ and $q$ are in relation $s$ if and only if:

$$ \forall x: a, y: b.\,\textrm { if } (x, y)\in r\textrm{ then }(p(x), q(y))\in r$$

Now we apply this condition to the types chosen as follows: $a = \underline0$, $b$ remains arbitrary, $r$ is the empty relation. Then $(x,y)\in r$ never holds for any $x:a$ and $y:b$, since the type $a$ is void.

It follows that any two functions $p: a\to a$ and $q: b\to b$ are always in the relation $s$. Indeed, there are never any values $x:a$ and $y:b$ for which $(x,y)\in r$, so the condition for $(p,q)\in s$ is a condition of the form "if false then ...". That formula is always true.

Now, $p$ must be of type $\underline0 \to\underline0$ and there is only one such $p$: the empty function. But $q: b\to b$ is still arbitrary.

Then the relational parametricity law of $\phi$ says that for arbitrary $q: b\to b$ we must have:

$$ (\phi^a(p), \phi^b(q))\in r $$

Now, $\phi^b(q)$ is the value of $\phi$ for a specific argument $q$. But $r$ is an empty relation to which no values may belong. This contradicts the assumption that a function $\phi$ exists. So, there are no functions $\phi$ of type $\forall a\,(a\to a)\to a$ that satisfy the relational parametricity law.

More generally, I can prove the type equivalence:

$$ \forall a.\,(a \to a)\to F\,a \cong F\,\underline 0 $$

when $F$ is a covariant functor. I write the relational law with the type $a=\underline0$ and find that any function $\phi$ of type $ \forall a.\,(a \to a)\to F\,a $ must ignore its argument (of type $a\to a$). Then the type $ \forall a.\,(a \to a)\to F\,a $ is effectively equivalent to just $\forall a.\,F\,a$, which is in turn equivalent to $F\,\underline0$.

However, these techniques do not apply to the other types listed at the beginning of this post.

**Tags:** functional-programming, typed-lambda-calculus, parametricity
> **Comments:**
> **username_1**: When you say "p must be of type 0 -> 0 and there is only one such p: the empty function", I think you meant "the identity function"?  Your conclusion still holds as you can't extract a value out of an arbitrary endomorphism, which is what the type asks for.  
> **username_0**: Yes, we have the intuition that "one can't extract information from an arbitrary value of type $a\to a$". But the whole problem here is to convert this intuition into a precise proof. To your comment about the function $p$: There is only one function of type $\underline 0\to\underline0$. I described it as an "empty function" because that function does not have any function body and is never applied to any arguments. You can also think of it as an "identity function for the type $\underline0$". It's still going to be the same function. The type $\underline0\to\underline0$ is equivalent to unit.  
> **username_2**: A relevant paper is [Logarithm and program testing](https://favonia.org/files/logarithm.pdf).  
> **username_0**: As far as I understood the "Logarithm" paper, their technique will sometimes produce a slightly larger type than necessary. Their focus is on testing, and for testing that's perfectly fine. But it's not so good for deriving type equivalence.  

---

## 2 answers

### Answer by username_0 on 2022-10-06. Score: 0 | Accepted answer

We can simplify the five type expressions given in the question. But we need to use different methods for these cases. Parametricity theorems give us a law that a value will satisfy, but we are not always able to derive useful information from those laws directly. We need other techniques.

One technique looks like this: given a type constructor $F$ check whether $F \,\textrm{Void} \cong \textrm{Void}$. It turns out that then we also have $\forall a.\,F\,a \cong \textrm{Void}$.

The reason is that a value of type $\forall a.\,F\,a $ is supposed to work in the same way for every type $a$, including the Void type. For every type $a$ there must be a value of type $F\,a$. If $F \,\textrm{Void} \cong \textrm{Void}$ then we cannot have a value of type $F\,a$ for some $a$, which means that the type $\forall a.\,F\,a$ has no values (is void).

Now we apply this technique to the five cases (assuming that the fixed types $r$ and $s$ are not themselves Void). We find that setting $a = \textrm{Void}$ we get Void for the following types:

$$ \forall a.\, (a \to r) \to a $$

$$ \forall a.\, (a \to a) \to a $$

$$ \forall a.\, ((a \to r) \to s) \to a $$

It means that these three types are void (uninhabited).

The question about this type:

$$ F\, r = \forall a.\, ((a \to r) \to a) \to a $$

is much more complicated. It turns out that $ F\,r \cong r$. Here is a solution:

First, use the contravariant Yoneda identity to get:
$$ ((a \to r) \to a) \to a \cong \forall b.\, (b\to a)\to ((b \to r) \to a) \to a $$

This allows us to rewrite the type $F\,r$ equivalently as:

$$ F \, r = \forall a.\, \forall b.\, (b\to a)\to ((b \to r) \to a) \to a $$

Exchange the quantifiers and uncurry some arguments:

$$ F\,r = \forall b.\, \forall a.\, ((b + (b\to r))\to a)\to a $$

Use the covariant Yoneda identity:
$$ \forall a. \, (x \to a)\to a \cong x $$

and simplify $F\, r$ further:

$$ F\,r = \forall b.\, b + (b\to r) $$

Now use the "disjunctivity lemma" (see at the end of my answer to [Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?](https://cstheory.stackexchange.com/questions/53855/)) and simplify:

$$ F\, r = (\forall b.\, b) + (\forall b.\, b\to r) $$

By the Yoneda identity again, we simplify $\forall b. \, b \cong\mathrm{Void}$ and $\forall b.\, b\to r \cong \mathbb1 \to r\cong r$.
So, we have finally:
$$ F\, r \cong \mathrm{Void} + r \cong r$$

Simplifying the type $\forall a.\,((a\to a)\to a)\to a$ can be done via a similar derivation shown in my answer here: [Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?](https://cstheory.stackexchange.com/questions/53855/)


---

### Answer by username_2 on 2024-04-05. Score: 0

Another proof technique that is more intuitive [in my biased opinion](https://prl.khoury.northeastern.edu/blog/2017/06/05/syntactic-parametricity-strikes-again/) is to enumerate normal forms of System F terms of the given type.

The most interesting example among those five given is $\forall a. ((a \to r) \to a) \to a$.

1. A term (or derivation) of $\vdash \forall a. ((a \to r) \to a) \to a$ in $\beta\eta$-normal form must start with introduction rules. There is only one way forward.
2. An open term of $a : \star, x : (a \to r) \to a \vdash a$ in $\beta\eta$-normal form can only be an application of a variable (because a $\beta$-normal form is a head-normal form). There is only $x$, which expects one argument.
3. A term of $a : \star, x : \dots \to a \vdash (a \to r)$ in $\beta\eta$-normal form must start with an introduction rule.
4. Since there were no choices to be made in the previous steps, we have thus obtained a bijection between terms of $\vdash \forall a. ((a \to r) \to a)$ and terms of $a : \star, x : \dots \to a, y : a \vdash r$, which can be closed into terms of type $\forall a. (\dots \to a) \to a \to r$.
5. Concluding with standard argument by semantic parametricity, that is isomorphic to $r$.

> **Comments:**
> **username_0**: This is an interesting technique. I have seen that blog post by G. Scherer and yourself. But I still have questions about that technique. 1) At step 4 you still require a relational parametricity argument (or Yoneda's identity) to show that $\forall a.\,((a\to r)\to a)\to a\to r \cong r$? 2) Would that technique also apply to all other examples in my question and, in particular, to $\forall a.\,((a\to a)\to a)\to a)$? At some point I thought I was able to prove that there was only one term of that type, because I thought there was only one proof in normal form, but I was wrong about that.  
> **username_2**: 1. Yes, I don't know how to make that argument syntactically. My point is, in the cases where syntactic parametricity does apply, even if incomplete, it makes things simpler. 2. Yes. For $((a \to a) \to a) \to a$ I just haven't come up with a recipe to distinguish the normal forms thus enumerated, but at the very least, writing down the decision tree like I did makes it obvious that there are more than 2 normal forms. For $(a \to a) \to a$ you run into an infinite descent which implies there is no solution. And for the two others the enumeration terminates immediately.  
> **username_0**: What is the difficulty for $\forall a.\, (...)\to a \to r \cong r$? Is the syntactic technique unable to deal with fixed types (such as $r$ here)? I am getting an impression that the syntactic parametricity technique is good only for terms of the form $\forall a.\, P a$ where $P$ depends only on $a$ and contains no other types.  
> **username_2**: Now that I think about it in the semantic argument, you never say what the semantic model is. You basically postulate that it somehow internalizes many categorical concepts (notably that polymorphic functions satisfy naturality). But you can instantiate it with the syntactic model, so any "semantic parametricity" argument is actually also a syntactic parametricity argument.  
> **username_0**: To me, the important question is what techniques of derivation do we have for solving various problems. The question of model theory is not directly relevant. Suppose we implement a System F interpreter as a specific computer program. Then some kind of semantic model will exist in the computer. And, most likely, that model will be based on sets, because everything in a computer's memory is a set. Maybe theorists have trouble with set-theoretic models of polymorphic lambda calculus, but that only says that the theorists haven't done their job properly, because our program already works.  
> **username_0**: So, I'm quite interested to learn the syntactic parametricity techniques, if those techniques help me get the correct solution easier than other ways. In this case, I was able eventually to get the answer without any guessing just by using what you call the "semantic" parametricity.  

---

