3
$\begingroup$

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$.

$\endgroup$
3
  • 3
    $\begingroup$ $∀ 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? $\endgroup$
    – Dan Doel
    Sep 27, 2022 at 22:15
  • $\begingroup$ @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. $\endgroup$
    – winitzki
    Sep 29, 2022 at 9:05
  • $\begingroup$ @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. $\endgroup$
    – winitzki
    Sep 29, 2022 at 9:14

1 Answer 1

1
$\begingroup$

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 $$

$\endgroup$

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.