Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?

Question

This question is about using relational parametricity to resolve practical questions in pure functional programming in System F.

Consider the following type of polymorphic functions:

$$T = \forall a. ( (a \to a) \to a ) \to a $$

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.

My initial hypothesis is that this type is equivalent to the unit type ($\mathbb1$). However, this may turn out to be wrong.

In any case, the type $T$ is certainly not void. There is a term $\phi : T$: $$\phi = \lambda(a: Type). \lambda\,(p:(a \to a) \to a). p \,\mathrm{id} $$

where "id" is the identity function, $ id = (\lambda\,(x: a). x)$.

Some other terms of type $T$ are:

$$ \phi =\lambda(a: Type). \lambda\,(p:(a \to a) \to a).\, p \,(\lambda\, \_. p\, \mathrm{id})$$

$$ \phi =\lambda(a: Type). \lambda\,(p:(a \to a) \to a).\, p \,(\lambda\, (x : a).\, p\, (\lambda\,_.\,x))$$

There seems to be infinitely many possible terms of that type, but it is not clear if they are all inequivalent, given parametricity constraints.

How to derive the type equivalence $T\cong\mathbb1$ or, if that is incorrect, another type equivalence rigorously?

I tried writing down a relational law satisfied by functions of the type $ T$ but it's complicated and I didn't figure out how to prove that there is only one value of that type.

The relational law should prove that, for any function $\phi : T$ and for any value $p : (a \to a)\to a$, the result of the application $\phi \,p$ is always equal to $p\, \mathrm{id}$.

The relational law of $\phi$ looks like this:

For any two types $a$, $b$, and for any relation $r:a\leftrightarrow b$ between values of types $a$ and $b$:

If two functions $p: (a \to a)\to a$ and $q: (b \to b)\to b$ are in a relation $s$ then the values $\phi\,p$ and $\phi\, q$ are in the relation $r$.

The relation $s$ is defined by: $p: (a \to a)\to a$ and $q: (b \to b)\to b$ are in $s$ if, for any $i: a\to a$ and $j: b\to b$ such that $i$ and $j$ are in the relation $t$, we will have the values $p\, i$ and $q \, j$ in the relation $r$.

The relation $t$ is defined by: $i: a\to a$ and $j: b\to b$ are in $t$ if, for any $x: a$ and $y: b$ such that $x$ and $y$ are in the relation $r$, we will have the values $i\, x$ and $j\,y$ are in the relation $r$.

This is a complicated set of conditions and it is not clear how to use them.

We can simplify these conditions if we choose the relation $r$ as a function: $(x, y)\in r$ if $f(x) = y$ with a fixed chosen function $f: a\to b$.

Then we obtain the following condition: For any $p: (a \to a)\to a$ and $q: (b \to b)\to b$ that are in relation $s$, we will have $f(\phi\,p) = \phi q$.

The relation $s$ is defined by: $p: (a \to a)\to a$ and $q: (b \to b)\to b$ are in $s$ if, for any $i: a\to a$ and $j: b\to b$ such that $f . i = j . f$, we will have $f(p (i)) = q(j)$.

This condition is somewhat simpler but I am still not able to use it to prove that any function $\phi: T$ is always of the form $\lambda\,p.\,p\,\mathrm{id}$. (That would be to prove that $T \cong\mathbb1$.)

Answer 1

Using syntactic methods, it's quite easy to see the correspondence between $\forall \alpha. ((\alpha \to \alpha) \to \alpha) \to \alpha$ and $1 + 2 + 3 + \dots$ You already had that intuition, and it can be turned into a formal argument in a more direct way than going through semantic parametricity.

Claim 1. In System F, the closed $\beta$-normal terms of type $\forall \alpha. ((\alpha \to \alpha) \to \alpha) \to \alpha$ are all of the form $\lambda f. f (\lambda x_1. f(\lambda x_2.\;\dots f(\lambda x_n. x_i)\dots))$, where $1 \le i \le n$.

The intuition comes from trying to write down some normal terms of that type by hand yourself. Proof of Claim 1 in the appendix below.

Claim 1 really describes a bijection between those normal terms and pairs of numbers $(n,i)$ where $i < n$. This can also be written as a dependent sum type $\sum_{1\le n}[n]$ where $[n] = \{1, \dots, n\}$. Hence "$1 + 2 + 3 + \dots$" And of course that is isomorphic to just $\mathbb{N}$.

The bijection in Claim 1 is a function on System F terms, a metaprogram. The next claim is that it is also definable as a program in System F.

While we're at it, we can avoid the burden of representing the dependent sum in "$(n,i) \in \sum_{1\le n} [n]$" in System F. With a change of variables $n = 1 + i + j$ and a switch to 0-indexing, the pair of indices $(i,j)$ now ranges over a simple product type $\mathbb{N}\times\mathbb{N}$.

Claim 2. There is a function $W$ definable in System F, of type $$W : \mathbb{N}\times\mathbb{N} \to (\forall \alpha. ((\alpha\to\alpha)\to\alpha)\to\alpha)$$ such that $$W(i,j) =_\beta \lambda f. f (\lambda x_0.\;\dots f(\lambda x_i.\;\dots f(\lambda x_{i+j}. x_i)\dots)\dots)$$

Proof. $W = \lambda(i,j). \mathrm{iter}\,i\,(\lambda y.f (\lambda \_.y))\, (f (\lambda x. \mathrm{iter}\,j\,(\lambda y.f(\lambda \_.y))\,x))$
where $\mathrm{iter}$ is the recursor of $\mathbb{N}$: $$\begin{align*}\mathrm{iter}&:\mathbb{N} \to (\alpha \to \alpha) \to \alpha \to \alpha\\ \mathrm{iter}\,0\,f\,x &= x\\\mathrm{iter}\,(1+n)\,f\,x &= f (\mathrm{iter}\,n\,f\,x)\end{align*}$$ □

Having enumerated $\beta$-normal terms is not the end of the story. How do we know that they are semantically distinct? We show that we can distinguish them inside System F:

Claim 3. There is a function $X$ (for "eXamine") definable in System F, of type $$X : (\forall \alpha. ((\alpha \to \alpha) \to \alpha) \to \alpha) \to \mathbb{N}\times\mathbb{N}$$ such that for every $(i,j)\in\mathbb{N}\times\mathbb{N}$, we can recover those indices out of $W(i,j)$ using $X$: $$X (W(i,j)) =_\beta (i, j)$$

The proof, including the definition of $X$, is too technical to be illuminating in prose, so here is a variant of it in Coq instead.

We now have the two directions of the isomorphism between $\forall \alpha. ((\alpha\to\alpha)\to\alpha)\to\alpha$ and $\mathbb{N}\times\mathbb{N}$ defined in System F. Those functions are mutually inverses modulo $\beta$-equivalence:

• $X (W(i,j)) =_\beta (i,j)$, for any closed terms $(i,j) \in \mathbb{N}\times\mathbb{N}$.
• $W (X t) =_\beta t$, for any closed term $t : \forall \alpha.((\alpha\to\alpha)\to\alpha)\to\alpha$.

Those imply the following contextual equivalences. This is mainly an excuse to write the isomorphism laws in pointfree form:

• $X \circ W =_\mathrm{ctx} \mathrm{id}_{\mathbb{N}\times\mathbb{N}}$
• $W \circ X =_\mathrm{ctx} \mathrm{id}_{\forall\alpha.((\alpha\to\alpha)\to\alpha)\to\alpha}$

---

On the one hand, I think this syntactic approach lets you make more precise claims, because I don't actually know what a denotational semantics of a polymorphic type looks like. On the other hand, a semantic argument seems more universal ("for all denotations (that satisfy some "parametricity" theorem)"), and can be easier to encode in a dependent type theory because you can just identify the denotations with the types of the host language. But you still have to be careful for the best results; for example, as Trebor noted in the comments of your other response, your non-disjunctivity lemma cannot be constructed in System F, so the resulting isomorphism as stated is an external construction (like the one in Claim 1).

---

Appendix

Proof of Claim 1. In System F, $\beta$-normal terms are necessarily lambdas over the application of a variable: $\lambda f. f M$, where $M$ is an open term subject to the typing judgement $\alpha : \star, f : (\alpha \to\alpha)\to\alpha \vdash M : \alpha \to \alpha$. You can keep expanding that way by hand to see the pattern. The following Lemma 1.a makes it formal. Refining $M = \lambda x_1. M'$, and applying Lemma 1.a with $n = 1$ concludes the proof of Claim 1. □

Lemma 1.a. $\beta$-normal terms $M$ of type $\alpha : \star, f : (\alpha\to\alpha)\to\alpha, x_1:\alpha, \dots, x_n:\alpha \vdash M : \alpha$ are of the form $f (\lambda x_{n+1}.\;\dots f(\lambda x_m. x_i)\dots)$ where $n \le m$ and $i \le m$.

Proof. By induction on $n$. Either $M$ is a variable, $M = x_i$ (concluding the proof with $m = n$). Or $M$ is an application of $f$, $M = f (\lambda x_{n+1}.N)$, and $N$ is of type $$\alpha : \star,f : (\alpha \to \alpha) \to \alpha, x_1 : \alpha,\dots x_{n+1} : \alpha \vdash N : \alpha$$ and we conclude by induction hypothesis. □

Answer 2

I claim that $T \cong \mathbb 1+\mathbb2+\mathbb3\,+\,…$. I will prove the type equivalence and then show what terms of type $T$ correspond to values of type $\mathbb 1+\mathbb2+\mathbb3\,+\,…$

The main idea is to transform $T$ to an equivalent type formulated as a Church encoding of the least fixpoint of some covariant type constructor, and then to simplify that fixpoint.

Step 1: use Yoneda

The contravariant Yoneda identity looks like this: if $G$ is a contravariant functor then: $$ G \, b \cong \forall r. (r \to b) \to G\, r $$

Use this identity with $G\, r = ((r \to b) \to b) \to b $ (considering $b$ to be a fixed type). We get: $$ G\, b = ((b \to b) \to b) \to b \cong \forall r.\, (r \to b) \to ((r \to b) \to b) \to b $$

Uncurry and combine the curried arguments into a co-product:

$$ (r \to b) \to ((r \to b) \to b) \to b \cong (r \to b)\times ((r \to b) \to b) \to b $$ $$ \cong (((r \to b) + r) \to b) \to b $$

Introduce a (covariant) functor $F\,r$ defined by: $$ F\, r \,x = (r \to x) + r $$ (This $F$ is not covariant in $r$ but that's okay, we will only need its covariance in $x$.)

Then: $$ (((r \to b) + r) \to b) \to b = (F\, r\, b \to b) \to b $$

Then we have finally obtained the type equivalence: $$ \forall b.\,((b \to b) \to b) \to b \cong \forall b.\,\forall r.\,(F\, r\, b \to b) \to b $$

Step 2: use the Church encoding

We can exchange the quantifiers in the last type:

$$\forall b.\,((b \to b) \to b) \to b \cong \forall r.\,\forall b.\,(F\, r\, b \to b) \to b $$

Now we notice that the type $\forall b.\,(H\, b \to b) \to b $ is the Church encoding of the least fixpoint of $H$ as long as $H\,b$ is covariant in $b$. Denote the least fixpoint by $\mu$, so: $$ \forall b.\,(H\, b \to b) \to b \cong \mu b.\, H \,b $$

Now we can write:

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

The fixpoint type $\mu b.\, (r \to b)+r$ is a type-level function of $r$ (neither covariant nor contravariant). Denote that function by $K$: $$ K\,r =\mu b.\,F\,r\,b = \mu b.\, (r \to b)+r$$

So far, we have proved that: $$T \cong \forall r.\,K\,r$$

Step 3: apply parametricity with $\forall r$

Because (as we defined) $K \, r = \mu b.\, (r \to b)+r$, we have the type equivalence $$K\,r\cong (r\to K\,r)+r$$ Substitute this into our last result: $$ T \cong \forall r.\,K\,r = \forall r.\,(r\to K\,r)+r$$

Under assumptions of parametricity, we have $$\forall r. \,P\, r+Q\,r \cong (\forall r. \, P \, r) + (\forall r.\, Q \, r)$$ (Use the "non-disjunctivity lemma" below and set $N\, r = \mathbb 1$. The type constructor $N$ is non-disjunctive. This is Example 1 in that section.)

So, we can write: $$ T \cong \forall r.\,K\,r = (\forall r.\,r\to K\,r) +(\forall r.\,r)$$

The second type is void ($\forall r.\,r = \mathbb 0$). So:

$$ T\cong \forall r.\,r\to K\,r $$

Expand the type $K\,r$ again: $$ T\cong \forall r.\,r\to K\,r \cong\forall r.\,r\to (r + (r \to K\,r)) $$

Parametricity constrains functions of type $\forall r.\,r \to (P\,r + Q\, r)$ because a function of that type cannot make decisions about whether to return the left or the right part of $P\, r + Q\, r$. So, $$\forall r.\,r \to (P\,r + Q\,r)\cong (\forall r.\, r \to P \,r )+(\forall r.\, r \to Q \,r ) $$ (Use the "non-disjunctivity lemma" below and set $N\, r = r$. The type constructor $N$ is non-disjunctive. This is Example 2 in that section.)

Then we have:

$$ \forall r.\,r\to (r + (r \to K\,r)) \cong (\forall r.\,r\to r) + (\forall r.\,r\to r\to K\,r) $$

The first term is simplified (via parametricity and Yoneda) as: $$\forall r.\, r\to r \cong \mathbb1$$

The second term is again expanded:

$$\forall r.\,r\times r \to K\,r = \forall r.\,r\times r \to (r + (r\to K\,r))$$

We again apply the parametricity-based reasoning (the "non-disjunctivity lemma" with $N \, r = r\times r$, Example 3) and find:

$$ \forall r.\,r\times r \to (r + (r\to K\,r)) \cong (\forall r.\,r\times r\to r) + (\forall r.\,r\times r \to r\to K\,r)$$

The first term is simplified via Yoneda as: $$\forall r.\,r\times r\to r \cong \mathbb 2$$

Instead of going on with this reasoning forever, use induction and summarize all the above by: $$T\cong \forall r.\,K\,r \cong \forall r.\,r + (r\to r) + (r\times r\to r) + (r\times r\times r\to r)\, +\, ...\cong \mathbb0 + \mathbb1 + \mathbb2 + \mathbb3 \,+\, ... $$

Step 4: what terms of type $T$ correspond to this

A value of type $\mathbb1 + \mathbb2 + \mathbb3 \,+\, ...$ is a coproduct with infinitely many parts. It is equivalent to a pair $(m, n)$ of integers such that $m \geq n\geq1$. The integer $m$ denotes the part of the coproduct, and the integer $n$ is a value of type $\mathbb m$ (that is, an integer between $1$ and $m$).

Given $(m, n)$, we want to write a lambda-term of type $T$. To do tha, we will reverse all the steps in the derivation of the type $\mathbb1 + \mathbb2 + \mathbb3 \,+\, ...$

To reverse the last step, we replace $\mathbb1 + \mathbb2 + \mathbb3 \,+\, ...$ by $$\forall r.\,(r\to r) + (r\times r\to r) + (r\times r\times r\to r)\, +\, ...$$ A value of that type is a function of type $$\forall r.\,\underline{r\,\times\, ...\,\times\, r}_{~~~~~m~times} \to r$$ with a specific $m\geq 1$. There are only $m$ functions of that type, numbered by $i$, where $1\leq i\leq m$. These functions are the standard projections $\pi_i$ that return the $i$-th value from the tuple of $m$ values. The function that corresponds to $(m, n)$ is $\pi_n$.

The next step is to go from the function $$\pi_n :\forall r.\,\underline{r\,\times\, ...\,\times\, r}_{~~~~~m~times} \to r$$
to a value of type $\forall r.\,K\,r$.

Curry the function $\pi_n$ and convert it into the equivalent function we call $\sigma_{m,n}$: $$\sigma_{m,n} : \forall r.\,\underline{r\,\to\, r\,\to\,...\,\to\, r}_{~~~~~m~times} \to r$$

The code of $\sigma_{m,n}$ will look like this: $$ \sigma_{m,n} \,r_1\, r_2\, ...\, r_m = r_n $$

Rewrite the type $K\,r = \mu b.\,r + (r\to b)$ as: $$K \, r = r + (r\to r + (r \to r + (...)))$$

Reversing the corresponding derivation step, we find that the function $\sigma_{m,n}$ corresponds to the following value of type $K\,r$ that we will call $k_{m,n}$: $$k _{m,n} = \mathrm{Right}(\lambda r_1.\,\mathrm{Right}(\lambda r_2.\,...\,\mathrm{Right}(\lambda r_m.\,\mathrm{Left}\,r_n)...) $$

Now we need to convert this into the Church encoding of the fixpoint, that is, to a value of type: $$ \forall b. (r + (r\to b) \to b)\to b $$ or equivalently: $$ \forall b. (r \to b) \to ((r\to b) \to b)\to b $$

A value of this type corresponding to $k_{m,n}$ is $c_{m,n}$ defined by the Church encoding of the constructors in the fixpoint type:

$$c_{m,n} \,(\mathrm{left}: r\to b )\, (\mathrm{right}: (r\to b)\to b) = \mathrm{right}(\lambda r_1.\,\mathrm{right}(\lambda r_2.\,...\,\mathrm{right}(\lambda r_m.\,\mathrm{left} \,r_n)...) $$

The last step is to set the types $r = b$ and substitute the identity function of type $b\to b$ instead of $\mathrm{left}$ and the argument $p: (b\to b)\to b$ instead of $\mathrm{right}$. This corresponds to using the Yoneda identity that maps a value of type $$ \forall r.\,(r \to b) \to ((r\to b) \to b)\to b$$ to a value of type $$ ((b\to b) \to b)\to b$$

The result is a term of type $T$:

$$t_{m,n} : T =\lambda(p: (b\to b)\to b).\, p(\lambda r_1.\,p(\lambda r_2.\,...\,p(\lambda r_m.\,r_n)...)$$

This concludes the solution.

The example terms shown in the question can be written as:

$$ t_{1,1} = \lambda(p: (b\to b)\to b).\, p(\lambda r_1.\, r_1) = \lambda p.\,p\,\mathrm{id}$$

$$t_{2,2} = \lambda(p: (b\to b)\to b).\, p(\lambda r_1.\,p(\lambda r_2.\, r_2)) = \lambda p.\,p (\lambda \_.\,p \,\mathrm{id}) $$

$$ t_{2,1} = \lambda(p: (b\to b)\to b).\, p(\lambda r_1.\,p(\lambda r_2.\, r_1)) = \lambda p.\,p (\lambda x.\,p(\lambda\_.\,x))$$

The non-disjunctivity lemma

A "unary" type constructor $N$ has a single type argument. We write that as a type application $N\, r$. The type constructor $N$ could have other type parameters but they are understood as fixed types, since we want to focus on $N$ as a type constructor with a single type argument.

Definition of "non-disjunctive type constructor"

A unary type constructor $N$ is called non-disjunctive if for any unary type constructors $P$, $Q$ the following type equivalence holds: $$ \forall r. \,N\, r\to (P\,r+Q\,r) \cong (\forall r.\,N\,r\to P\,r) + (\forall r.\,N\,r\to Q\,r) $$ The type constructors $N$, $P$, $Q$ are not necessarily covariant or contravariant.

To see the intuition for this name, consider that a function of type $N\, r\to P\,r+Q\,r$ must return a value of type $P\,r$ or a value of type $Q\,r$, that is, either the left or the right part of the disjunction $P\,r+Q\,r$. Could that decision depend on a given value of type $N\,r$? It could, if we could pattern match on a value of type $N\,r$. But if, say, $N\,r=\mathbb 1$ or $N\,r = r$ then we cannot pattern match on those values. Then a function of type $N\, r\to P\,r+Q\,r$ must hard-code the decision of returning either left or right parts for all inputs.

So, I say that a value of type $N\,r$ "carries no disjunctive information" (cannot be pattern matched). This is a property of $N$ that I call "non-disjunctivity". (This is my terminology, as I don't know an established name for this property.)

Some notation

The non-disjunctivity lemma says that a certain class of type constructors is non-disjunctive and gives examples of how to obtain type constructors of that class. It is based on relational parametricity considerations.

We need some notation to formulate that lemma.

Binary relations between values of types $a$ and $b$ are denoted by $ R:a\leftrightarrow b$.

If $R:a\leftrightarrow b$ is a relation then we write $(x,y)\in R$ if two values $x:a$ and $y:b$ are in the relation $R$.

Let us denote by $\bot: a\leftrightarrow b$ the empty relation (it never holds) and by $\top: A\leftrightarrow b$ the full relation (it always holds). So, for instance, we have: $$ \forall x:a.\,\forall y:b.\,(x,y)\in \top$$ $$ \forall x:a.\,\forall y:b.\,(x,y)\not\in \bot$$

We denote by "id" the identity relation, which is a relation of type $\forall a.\,a\leftrightarrow a$ such that $(x,y)\in \mathrm{id}$ if and only if $x=y$.

For any unary type constructor $N$, any relation $ R:a\leftrightarrow b$ can be lifted to a relation $ N\,R:N\,a\leftrightarrow N\,b$. This is quite similar to lifting a function $f:a\to b$ to a function $N\,f:N\,a\to N\,b$ except that a function can be lifted only if $N$ is covariant; but a relation can always be lifted (within System F or System F$\omega$), even if $N$ is neither covariant nor contravariant. The construction of relational lifting is standard and is similar to the construction of functional lifting; it proceeds by induction on the type structure of $N$.

Finally, the parametricity theorem for unary type constructors says that any "purely parametrically polymorphic" value $f:\forall a.\,F\,a$ (this covers any code written in System F or System F$\omega$) satisfies the relational naturality law:

$$ \forall a: \mathrm{Type}.\,\forall b: \mathrm{Type}.\, \forall R:a\leftrightarrow b.\, (f\, a, f\, b)\in F \,R $$

Remark:

Although I don't know any textbook or paper where the parametricity technique is explained clearly and in detail, surely this is standard material and someone can point out a good reference?

The non-disjunctivity lemma

A unary type constructor $N$ is non-disjunctive if $N$ is not identically void ($N\,r\not =\mathbb0$ for some $r$) and if for any types $a$ and $b$ such that $N\,a \not =\mathbb0$ and $N\,b \not =\mathbb0$ there exists a relation $R:a\leftrightarrow b$ for which $N\,R = \top$.

Proof.

The idea of the proof is that a type constructor that has a co-product at top level will never be able to lift any relation to a full relation, because of the relational lifting rules for co-products.

Choose types $a$, $b$ and a relation $R:a\leftrightarrow b$ satisfying the stated assumptions. Take any function $f:\forall r. \,N\, r\to P\,r+Q\,r$. Denote for brevity: $$F \,r = N\, r\to P\,r+Q\,r$$ $$G\,r = P\,r + Q\,r $$

Write the relational naturality law of $f$ with parameters $a$,$b$,$R$:

$$ (f\,a, f\,b)\in F \,R $$

Expand the relation $F\, R$ according to the rules of relational lifting for function types:

$$\forall x:N\,a.\,\forall y:N\,b.\, \mathrm{~if~} (x,y)\in N\, R \mathrm{~then~} (f\, a \,x, f\, b\, y)\in G\,R $$

By assumption, $N\,R=\top$ and so we will always have $(x,y)\in N\, R $. So, we can simplify the relational naturality law of $f$:

$$\forall x:N\,a.\,\forall y:N\,b.\, (f\, a \,x, f\, b\, y)\in G\,R $$

But $G\,r$ is a co-product type. Apply the rules of relational lifting for co-products. The law of $f$ becomes a disjunction of two conditions:

$$\forall x:N\,a.\,\forall y:N\,b.\, \mathrm{~either~} f\, a \,x = \mathrm{Left}\,p_1 \mathrm{~and~} f\, b\, y = \mathrm{Left}\,p_2 \mathrm{~and~}(p_1,p_2)\in P\,R \mathrm{~or~} f\, a \,x = \mathrm{Right}\,q_1 \mathrm{~and~} f\, b\, y = \mathrm{Right}\,q_2 \mathrm{~and~}(q_1,q_2)\in Q\,R $$

By assumption, the types $N\,a$ and $N\,b$ are not void, so we may fix a specific value $x_0:N\,a$. Then $f\,a\,x_0$ is in either "Left" or "Right" part of the co-product $P\,a+Q\,a$. Suppose it is a "Left" (the proof will be analogous if it is a "Right"). Then denote $p_0 : P \,a = f \,a\,x_0$ and simplify the above condition to:

$$ \forall b:\mathrm{Type}.\,\forall y:N\,b.\, f\, b\, y = \mathrm{Left}\,p_2 \mathrm{~and~}(p_0,p_2)\in P\,R $$

Incidentally, this is the relational naturality law for functions of type $\forall r.\, N\,r\to P\,r$ if we substitute $x_0$ and $a$ into that law.

So, it follows that $f\,b\,y$ is also in the "Left" part for all $y$ (and for all types $b$).

So, parametricity enforces that the function $f$ always returns a "Left" for all inputs of all types, as long as $f$ returns a "Left" for just one value $x_0$ of just one type $a$. And parametricity also enforces the same law on functions of type $\forall r.\, N\,r\to P\,r$.

We conclude that the type of functions $f:\forall r.\, N\,r\to P\,r + Q\,r$ such that there exists $x_0:N\,a$ with $f\,a\,x_0 = \mathrm{Left}\,p_0$ are isomorphic to the type $\forall r.\, N\,r\to P\,r$.

Similarly for the "Right" variant. If $f$ returns a "Right" even just for one type $a$ and for one input $x_0:N\,a$ then $f$ always returns a "Right".

Now we can demonstrate an isomorphism between types $$\forall r.\, N\,r\to P\,r+Q\,r$$ and $$(\forall r.\, N\,r\to P\,r)+\forall r.\, N\,r\to Q\,r$$

A value of the latter type is either a "Left" or a "Right". Suppose it is a "Left" (the consideration will be analogous if it is a "Right"). Then it is a $\mathrm{Left}\,k$ for some $k: \forall r.\, N\,r\to P\,r$. Also, $k$ satisfies the relational naturality law for functions of type $\forall r.\, N\,r\to P\,r$. The isomorphism maps $k$ to a function $f$ of type $\forall r.\, N\,r\to P\,r + Q\,r$ that always returns a $\mathrm{Left}\,(P\,r)$. We define $f$ by: $$f \, r\, x = \mathrm{Left}\,(k\,r\,x)$$ The function $f$ satisfies its relational naturality law because it's equivalent to that of $k$, as we have seen.

So, the set of all purely parametric $k$ of type "Left" is in a one-to-one correspondence with the set of all purely parametric $f$ that always return "Left".

Similarly, the set of all purely parametric $k$ of type "Right" is in a one-to-one correspondence with the set of all purely parametric $f$ that always return "Right".

We have shown that there are no $f$ that sometimes return "Left" and sometimes return "Right". So, the entire type $\forall r.\, N\,r\to P\,r+Q\,r$ is in a one-to-one correspondence with the entire type $(\forall r.\, N\,r\to P\,r)+\forall r.\, N\,r\to Q\,r$.

Q.E.D.

Examples of non-disjunctive type constructors

To show that a type constructor $N$ is non-disjunctive, we just need to give an example of a relation $R$ that is lifted by $N$ to a full relation ($N\,R=\top$). The rest follows from the non-disjunctivity lemma.

Here are some examples:

1. The constant unit type constructor.

Let $N\,r = \mathbb 1$, then any relation $R:a\leftrightarrow b$ is lifted to $N\,R = \mathrm{id}$. But the identity relation on the unit type is a full relation (the unit type has only one value).

2. The identity functor.

Let $N\,r = r$, then lifting is trivial ($N\,R = R$ for any relation $R$). So, the full relation is lifted again to the full relation.

3. A function from any type to a non-disjunctive type constructor.

Let $N\,r = L\, r\to M\,r$ where $M$ is non-disjunctive. We want to show that there exists some $R$ such that $N\,R = \top$.

We know that there exists $R$ such that $M\,R=\top$; the same $R$ will do, as we now show. Write the relational naturality law for functions $f$ of type $N\,r$. Values $f\,a$ and $f\,b$ are in the relation $N \,R$ when: $$ \forall x:L\,a. \forall y:L\,b. \mathrm{~if~} (x,y)\in L\,R \mathrm{~then~} (f\,a\,x, f\,b\,y)\in M\,R$$

This is a conditional statement whose consequence is always true. So, the statement is also always true, so $f\,a$ and $f\,b$ are always in the relation $N\,R$. It means that $N\,R=\top$.

A consequence is that $N\,r = \underline{r\,\times \,r\,\times\, ...\,\times\,r}_{~~~~~n~times} = \mathbb n\to r$ is non-disjunctive.

Also note that $L$ could be any type constructor, including a co-product, but it is not at top level in $L\, r\to M\,r$ and so $N$ is still non-disjunctive.

4. A function from $r$ to any type constructor.

Let $N\,r = r\to M\,r$ where $M$ is any type constructor. Take $R=\bot$ and lift to $N$. Then $f\,a$ and $f\,b$ are in the relation $N\,R$ when:

$$\forall x:a.\, \forall y: b.\,\mathrm{~if~} (x, y)\in R \mathrm{~then~} (f\, a\, x, f\, b\, y) \in M \,R$$

This is a conditional statement whose premise is always false as $R=\bot$ and $(x,y)\not\in \bot $ for any $x$, $y$. So, the conditional statement is always true. It means that $f\,a$ and $f\,b$ are always in the relation $N\,R$; that is, $N\,R=\top$.

Example: List Nat

Using the techniques developed here, we can prove the following type equivalence:

$$ \mathrm{List}\, \mathrm{Nat} = \mathbb 1 + \mathrm{Nat} + \mathrm{Nat} \times \mathrm{Nat} \,+ \, ...$$ $$ \cong (\mathbb 0\to \mathrm{Nat}) + (\mathbb 1 \to \mathrm{Nat}) + (\mathbb 2 \to \mathrm{Nat}) \,+\, ... $$ $$\cong (\mathbb 0\to \forall a.\,(a\to a)\to(a \to a)) + (\mathbb 1\to \forall a.\,(a\to a)\to(a \to a)) + (\mathbb 2\to \forall a.\,(a\to a)\to(a \to a)) \,+\, ... $$ $$\cong \forall a.\, (\mathbb 0\to (a\to a)\to(a \to a)) + (\mathbb 1\to (a\to a)\to(a \to a)) + (\mathbb 2\to (a\to a)\to(a \to a)) \,+\, ... $$ $$\cong \forall a.\, (a \to a) + ( (a\to a)\to(a \to a)) + ((a\to a)\to (a\to a)\to(a \to a)) \,+\, ... $$

The type constructor $N\, a = a \to a$ is non-disjunctive (via Example 2 and Example 3 above). So, we can rewrite the type as:

$$ \forall a.\, N\,a +( N\,a\to N\,a) + (N\,a\to N\,a\to N\,a) \,+\, ... $$ $$\cong \forall a.\, N\,a + ( N\,a\to (N\,a + (N\,a\to (N\,a\,+\, ...))...) $$

The last type can be written as $\forall a.\, K\, a$ where we define $K$ recursively as: $$K\, a = (a \to a) + ((a \to a) \to K\, a) $$

or $$K\, a = \mu b.\,(a \to a) + ((a \to a) \to b)$$

This is the least fixpoint of a positive type constructor. So, it can be rewritten via the Church encoding:

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

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

Finally, imposing the quantifier $\forall a$, we get the type equivalence:

$$\mathrm{List}\, \mathrm{Nat} \cong \forall a.\,\forall b.\, ((a \to a) \to b)\to ((a \to a) \to b) \to b)\to b$$

Answer 3

They are inequivalent. Let's number the three $\phi$ you listed as $\phi_1, \phi_2, \phi_3$. Then $\phi_1 \mathbb N (\lambda f. f(0)+1) = 1$, while $\phi_2, \phi_3$ both give the result $2$. Therefore they are observationally inequivalent, implying that in all reasonable sense of equivalence (syntactic, beta, beta-eta, denotational, etc.) they must be inequivalent. You can construct infinitely many different terms.

This type is very messy and does not admit simplifications. It's almost the least fixedpoint $\mu X. (X \to X)$ (except that it isn't, because of positivity issues). Or in Haskell notation, data Term = Lam (Term -> Term). You can fit the entire untyped lambda calculus inside of this type! Your $\phi_1$ translates to Lam \x -> x, so it's the encoding of the UTLC term $\lambda x. x$; and $\phi_2$ is Lam \x -> Lam \y -> y, so it encodes the UTLC term $K$, and your $\phi_3$ encodes $KI$.