<p>The solution was suggested in a comment by @DanDoel.</p>
<p>Flip the first two curried arguments in the type:</p>
<p><span class="math-container">$$\forall a.\,((a\rightarrow r)\rightarrow s) \rightarrow(a\rightarrow r)\rightarrow s $$</span></p>
<p>and obtain an isomorphic type:</p>
<p><span class="math-container">$$ \forall a. (a\rightarrow r)\rightarrow ((a \rightarrow r)\rightarrow s)\rightarrow s $$</span></p>
<p>Now this type is in the form <span class="math-container">$\forall a.(a\rightarrow r)\rightarrow F\,a$</span> where <span class="math-container">$F$</span> is a contravariant functor:</p>
<p><span class="math-container">$$ F\,a \overset{\textrm{def}}{=} ((a \rightarrow r)\rightarrow s)\rightarrow s  $$</span></p>
<p>By the contravariant Yoneda lemma, the type is equivalent to <span class="math-container">$F\,r$</span>.</p>
<p>So, we obtain the type equivalence:</p>
<p><span class="math-container">$$ \forall a.\,((a\rightarrow r)\rightarrow s) \rightarrow(a\rightarrow r)\rightarrow s  \cong  ((r \rightarrow r)\rightarrow s)\rightarrow s  $$</span></p>

CC BY-SA 4.0
2022-09-29T10:29:20.727Z
2022-09-29T10:29:20.727Z
winitzki
<p>This question 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 \rightarrow r)  \rightarrow r) \rightarrow ((a \rightarrow r) \rightarrow r) $$</span></p>
<p>and</p>
<p><span class="math-container">$$ \forall a.\, ((a \rightarrow r)  \rightarrow s) \rightarrow ((a \rightarrow r) \rightarrow s) $$</span></p>
<p>where <span class="math-container">$s$</span> and <span class="math-container">$r$</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. In particular, all functions of the above types will be natural transformations.</p>
<p>It appears that the last type is equivalent to a pair of functions <span class="math-container">$ (r \rightarrow r, s \rightarrow s) $</span>. But I don't know how to derive that type equivalence rigorously, and it is not clearly the correct type equivalence that one expects here.</p>
<p>As an example where a similar question can be answered straightforwardly, consider the type <span class="math-container">$\forall a.\, (a \rightarrow r) \rightarrow (a \rightarrow s)$</span>.</p>
<p>The type <span class="math-container">$\forall a.\, (a \rightarrow r) \rightarrow (a \rightarrow s)$</span> can be simplified to <span class="math-container">$r \rightarrow s$</span> by using the (contravariant) Yoneda lemma:</p>
<p><span class="math-container">$$ \forall a. (a \rightarrow t) \rightarrow (F\, a) \cong F\, t \quad \textrm{where } F \textrm { is a contravariant functor} $$</span></p>
<p>if we set <span class="math-container">$F\,x \overset{def}{=} x\rightarrow s $</span>.</p>
<p>The Yoneda lemma may be used here because we assume that all values are pure lambda terms from System F. Then, by parametricity theorems of Reynolds and Wadler, all functions of type <span class="math-container">$\forall a. (a \rightarrow r) \rightarrow (a \rightarrow s)$</span> are natural transformations (their naturality law is a &quot;free theorem&quot; in the terminology of Wadler). So, the Yoneda lemma applies.</p>
<p>We may also use the relational parametricity theorems directly to derive this type equivalence:</p>
<p><span class="math-container">$$ \forall a.\, (a \rightarrow r) \rightarrow (a \rightarrow s) \cong r \rightarrow s $$</span></p>
<p>Without the Yoneda lemma, we need a longer and more complicated proof, but we will still need to begin by deriving the naturality law and to proceed from there, in order to show that each function of type <span class="math-container">$\forall a.\, (a \rightarrow r) \rightarrow (a \rightarrow s)$</span> is expressed via a unique function of type <span class="math-container">$s \rightarrow r$</span>.</p>
<p><s>However, the Yoneda lemma does not apply to the types shown at the beginning.</s> (See solution below.)</p>
<p>Relational parametricity theorems can be used to simplify certain types containing universal quantifiers. However, it is never obvious how to use relational parametricity when the Yoneda lemma cannot be used. I don't seem to find a good trick to resolve this and similar questions about quantified types of the form <span class="math-container">$\forall a. (a \rightarrow r) \rightarrow s$</span>.</p>

CC BY-SA 4.0
2022-09-27T22:15:06.080Z
$∀ a. ((a → r) → s) → ((a → r) → s)$ is isomorphic to $∀ a. (a → r) → ((a → r) → s) → s$. $(a → r) → s$ is covariant in $a$, so $((a → r) → s) → s$ is contravariant in $a$. Now the contravariant Yoneda lemma can be used, no?
Dan Doel
CC BY-SA 4.0
2022-09-29T09:05:09.890Z
@DanDoel Yes indeed, thank you! I did not think about using this trick. Then the contravariant Yoneda lemma can be used and we get $((r \rightarrow r) \rightarrow s)\rightarrow s$. I will write up an answer to my question.
winitzki
CC BY-SA 4.0
2022-09-29T09:14:20.623Z
@DanDoel I have a few other questions where I don't see how to use Yoneda. Here are examples: $\forall a.\,((a\rightarrow a)\rightarrow a)\rightarrow a$ and $\forall a.\,((a\rightarrow r)\rightarrow a)\rightarrow a$. Please let me know if you have any ideas here. Is it worth writing up another question? In a simpler case, I can prove that $\forall a.\,(a\rightarrow a)\rightarrow a\cong Void$ by ad hoc arguments via relational parametricity and strong dinaturality. More generally, I can show that $\forall a. (a\rightarrow a)\rightarrow F\,a\cong F\,Void$ if $F$ is a covariant functor.
winitzki
<functional-programming><typed-lambda-calculus><parametricity>
Can we use relational parametricity to simplify the type $\forall a. ( (a \to r) \to r ) \to (a \to r) \to r$?
winitzki
# Can we use relational parametricity to simplify the type $\forall a. ( (a \to r) \to r ) \to (a \to r) \to r$?

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

This question 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 \rightarrow r) \rightarrow r) \rightarrow ((a \rightarrow r) \rightarrow r) $$

and

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

where $s$ and $r$ 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. In particular, all functions of the above types will be natural transformations.

It appears that the last type is equivalent to a pair of functions $ (r \rightarrow r, s \rightarrow s) $. But I don't know how to derive that type equivalence rigorously, and it is not clearly the correct type equivalence that one expects here.

As an example where a similar question can be answered straightforwardly, consider the type $\forall a.\, (a \rightarrow r) \rightarrow (a \rightarrow s)$.

The type $\forall a.\, (a \rightarrow r) \rightarrow (a \rightarrow s)$ can be simplified to $r \rightarrow s$ by using the (contravariant) Yoneda lemma:

$$ \forall a. (a \rightarrow t) \rightarrow (F\, a) \cong F\, t \quad \textrm{where } F \textrm { is a contravariant functor} $$

if we set $F\,x \overset{def}{=} x\rightarrow s $.

The Yoneda lemma may be used here because we assume that all values are pure lambda terms from System F. Then, by parametricity theorems of Reynolds and Wadler, all functions of type $\forall a. (a \rightarrow r) \rightarrow (a \rightarrow s)$ are natural transformations (their naturality law is a "free theorem" in the terminology of Wadler). So, the Yoneda lemma applies.

We may also use the relational parametricity theorems directly to derive this type equivalence:

$$ \forall a.\, (a \rightarrow r) \rightarrow (a \rightarrow s) \cong r \rightarrow s $$

Without the Yoneda lemma, we need a longer and more complicated proof, but we will still need to begin by deriving the naturality law and to proceed from there, in order to show that each function of type $\forall a.\, (a \rightarrow r) \rightarrow (a \rightarrow s)$ is expressed via a unique function of type $s \rightarrow r$.

~~However, the Yoneda lemma does not apply to the types shown at the beginning.~~ (See solution below.)

Relational parametricity theorems can be used to simplify certain types containing universal quantifiers. However, it is never obvious how to use relational parametricity when the Yoneda lemma cannot be used. I don't seem to find a good trick to resolve this and similar questions about quantified types of the form $\forall a. (a \rightarrow r) \rightarrow s$.

**Tags:** functional-programming, typed-lambda-calculus, parametricity
> **Comments:**
> **username_1**: $∀ a. ((a → r) → s) → ((a → r) → s)$ is isomorphic to $∀ a. (a → r) → ((a → r) → s) → s$. $(a → r) → s$ is covariant in $a$, so $((a → r) → s) → s$ is contravariant in $a$. Now the contravariant Yoneda lemma can be used, no?  
> **username_0**: @DanDoel Yes indeed, thank you! I did not think about using this trick. Then the contravariant Yoneda lemma can be used and we get $((r \rightarrow r) \rightarrow s)\rightarrow s$. I will write up an answer to my question.  
> **username_0**: @DanDoel I have a few other questions where I don't see how to use Yoneda. Here are examples: $\forall a.\,((a\rightarrow a)\rightarrow a)\rightarrow a$ and $\forall a.\,((a\rightarrow r)\rightarrow a)\rightarrow a$. Please let me know if you have any ideas here. Is it worth writing up another question? In a simpler case, I can prove that $\forall a.\,(a\rightarrow a)\rightarrow a\cong Void$ by ad hoc arguments via relational parametricity and strong dinaturality. More generally, I can show that $\forall a. (a\rightarrow a)\rightarrow F\,a\cong F\,Void$ if $F$ is a covariant functor.  

---

## 1 answers

### Answer by username_0 on 2022-09-29. Score: 1 | Accepted answer

The solution was suggested in a comment by @DanDoel.

Flip the first two curried arguments in the type:

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

and obtain an isomorphic type:

$$ \forall a. (a\rightarrow r)\rightarrow ((a \rightarrow r)\rightarrow s)\rightarrow s $$

Now this type is in the form $\forall a.(a\rightarrow r)\rightarrow F\,a$ where $F$ is a contravariant functor:

$$ F\,a \overset{\textrm{def}}{=} ((a \rightarrow r)\rightarrow s)\rightarrow s $$

By the contravariant Yoneda lemma, the type is equivalent to $F\,r$.

So, we obtain the type equivalence:

$$ \forall a.\,((a\rightarrow r)\rightarrow s) \rightarrow(a\rightarrow r)\rightarrow s \cong ((r \rightarrow r)\rightarrow s)\rightarrow s $$


---

