<p>I claim that <span class="math-container">$T \cong \mathbb 1+\mathbb2+\mathbb3\,+\,…$</span>. I will prove the type equivalence and then show what terms of type <span class="math-container">$T$</span> correspond to values of type  <span class="math-container">$\mathbb 1+\mathbb2+\mathbb3\,+\,…$</span></p>
<p>The main idea is to transform <span class="math-container">$T$</span> to an equivalent type formulated as a Church encoding of the least fixpoint of some covariant type constructor, and then to simplify that fixpoint.</p>
<h1>Step 1: use Yoneda</h1>
<p>The contravariant Yoneda identity looks like this: if <span class="math-container">$G$</span> is a contravariant functor then:
<span class="math-container">$$ G \, b \cong \forall r. (r \to b) \to G\, r   $$</span></p>
<p>Use this identity with <span class="math-container">$G\, r = ((r \to b) \to b) \to b $</span> (considering <span class="math-container">$b$</span> to be a fixed type). We get:
<span class="math-container">$$ G\, b = ((b \to b) \to b) \to b \cong \forall r.\, (r \to b) \to ((r \to b) \to b) \to b $$</span></p>
<p>Uncurry and combine the curried arguments into a co-product:</p>
<p><span class="math-container">$$ (r \to b) \to ((r \to b) \to b) \to b \cong (r \to b)\times ((r \to b) \to b) \to b $$</span> <span class="math-container">$$ \cong (((r \to b) + r) \to b) \to b  $$</span></p>
<p>Introduce a (covariant) functor <span class="math-container">$F\,r$</span> defined by:
<span class="math-container">$$ F\, r \,x = (r \to x) + r $$</span>
(This <span class="math-container">$F$</span> is not covariant in <span class="math-container">$r$</span> but that's okay, we will only need its covariance in <span class="math-container">$x$</span>.)</p>
<p>Then:
<span class="math-container">$$ (((r \to b) + r) \to b) \to b = (F\, r\, b \to b) \to b $$</span></p>
<p>Then we have finally obtained the type equivalence:
<span class="math-container">$$ \forall b.\,((b \to b) \to b) \to b \cong  \forall b.\,\forall r.\,(F\, r\, b \to b) \to b  $$</span></p>
<h1>Step 2: use the Church encoding</h1>
<p>We can exchange the quantifiers in the last type:</p>
<p><span class="math-container">$$\forall b.\,((b \to b) \to b) \to b \cong  \forall r.\,\forall b.\,(F\, r\, b \to b) \to b  $$</span></p>
<p>Now we notice that the type <span class="math-container">$\forall b.\,(H\, b \to b) \to b $</span> is the Church encoding of the least fixpoint of <span class="math-container">$H$</span> as long as <span class="math-container">$H\,b$</span> is covariant in <span class="math-container">$b$</span>. Denote the least fixpoint by <span class="math-container">$\mu$</span>, so:
<span class="math-container">$$ \forall b.\,(H\, b \to b) \to b  \cong \mu b.\, H \,b $$</span></p>
<p>Now we can write:</p>
<p><span class="math-container">$$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 $$</span></p>
<p>The fixpoint type <span class="math-container">$\mu b.\, (r \to b)+r$</span> is a type-level function of <span class="math-container">$r$</span> (neither covariant nor contravariant). Denote that function by <span class="math-container">$K$</span>:
<span class="math-container">$$ K\,r =\mu b.\,F\,r\,b = \mu b.\, (r \to b)+r$$</span></p>
<p>So far, we have proved that: <span class="math-container">$$T \cong \forall r.\,K\,r$$</span></p>
<h1>Step 3: apply parametricity with <span class="math-container">$\forall r$</span></h1>
<p>Because (as we defined) <span class="math-container">$K \, r = \mu b.\, (r \to b)+r$</span>, we have the type equivalence <span class="math-container">$$K\,r\cong (r\to K\,r)+r$$</span> Substitute this into our last result:
<span class="math-container">$$ T \cong \forall r.\,K\,r = \forall r.\,(r\to K\,r)+r$$</span></p>
<p>Under assumptions of parametricity, we have <span class="math-container">$$\forall r. \,P\, r+Q\,r \cong (\forall r. \, P \, r) + (\forall r.\, Q \, r)$$</span> (Use the &quot;non-disjunctivity lemma&quot; below and set <span class="math-container">$N\, r = \mathbb 1$</span>. The type constructor <span class="math-container">$N$</span> is non-disjunctive. This is Example 1 in that section.)</p>
<p>So, we can write:
<span class="math-container">$$ T \cong \forall r.\,K\,r = (\forall r.\,r\to K\,r) +(\forall r.\,r)$$</span></p>
<p>The second type is void (<span class="math-container">$\forall r.\,r = \mathbb 0$</span>). So:</p>
<p><span class="math-container">$$ T\cong \forall r.\,r\to K\,r $$</span></p>
<p>Expand the type <span class="math-container">$K\,r$</span> again:
<span class="math-container">$$ T\cong \forall r.\,r\to K\,r \cong\forall r.\,r\to (r + (r \to K\,r)) $$</span></p>
<p>Parametricity constrains functions of type <span class="math-container">$\forall r.\,r \to (P\,r + Q\, r)$</span> because a function of that type cannot make decisions about whether to return the left or the right part of <span class="math-container">$P\, r + Q\, r$</span>. So, <span class="math-container">$$\forall r.\,r \to (P\,r + Q\,r)\cong (\forall r.\, r \to P \,r )+(\forall r.\, r \to Q \,r ) $$</span> (Use the &quot;non-disjunctivity lemma&quot; below and set <span class="math-container">$N\, r = r$</span>. The type constructor <span class="math-container">$N$</span> is non-disjunctive. This is Example 2 in that section.)</p>
<p>Then we have:</p>
<p><span class="math-container">$$  \forall r.\,r\to (r + (r \to K\,r)) \cong (\forall r.\,r\to r) + (\forall r.\,r\to r\to K\,r) $$</span></p>
<p>The first term is simplified (via parametricity and Yoneda) as: <span class="math-container">$$\forall r.\, r\to r \cong \mathbb1$$</span></p>
<p>The second term is again expanded:</p>
<p><span class="math-container">$$\forall r.\,r\times r \to K\,r = \forall r.\,r\times r \to (r + (r\to K\,r))$$</span></p>
<p>We again apply the parametricity-based reasoning (the &quot;non-disjunctivity lemma&quot; with <span class="math-container">$N \, r = r\times r$</span>, Example 3) and find:</p>
<p><span class="math-container">$$ \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)$$</span></p>
<p>The first term is simplified via Yoneda as: <span class="math-container">$$\forall r.\,r\times r\to r \cong \mathbb 2$$</span></p>
<p>Instead of going on with this reasoning forever, use induction and summarize all the above by:
<span class="math-container">$$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 \,+\, ... $$</span></p>
<h1>Step 4: what terms of type <span class="math-container">$T$</span> correspond to this</h1>
<p>A value of type <span class="math-container">$\mathbb1 + \mathbb2 + \mathbb3 \,+\, ...$</span> is a coproduct with infinitely many parts. It is equivalent to a pair <span class="math-container">$(m, n)$</span> of integers such that <span class="math-container">$m \geq n\geq1$</span>. The integer <span class="math-container">$m$</span> denotes the part of the coproduct, and the integer <span class="math-container">$n$</span> is a value of type <span class="math-container">$\mathbb m$</span> (that is, an integer between <span class="math-container">$1$</span> and <span class="math-container">$m$</span>).</p>
<p>Given <span class="math-container">$(m, n)$</span>, we want to write a lambda-term of type <span class="math-container">$T$</span>. To do tha, we will reverse all the steps in the derivation of the type <span class="math-container">$\mathbb1 + \mathbb2 + \mathbb3 \,+\, ...$</span></p>
<p>To reverse the last step, we replace <span class="math-container">$\mathbb1 + \mathbb2 + \mathbb3 \,+\, ...$</span> by <span class="math-container">$$\forall r.\,(r\to r) + (r\times r\to r) + (r\times r\times r\to r)\, +\, ...$$</span>
A value of that type is a function of type <span class="math-container">$$\forall r.\,\underline{r\,\times\, ...\,\times\, r}_{~~~~~m~times} \to r$$</span> with a specific <span class="math-container">$m\geq 1$</span>. There are only <span class="math-container">$m$</span> functions of that type, numbered by <span class="math-container">$i$</span>, where <span class="math-container">$1\leq i\leq m$</span>. These functions are the standard projections <span class="math-container">$\pi_i$</span> that return the <span class="math-container">$i$</span>-th value from the tuple of <span class="math-container">$m$</span> values. The function that corresponds to <span class="math-container">$(m, n)$</span> is <span class="math-container">$\pi_n$</span>.</p>
<p>The next step is to go from the function <span class="math-container">$$\pi_n :\forall r.\,\underline{r\,\times\, ...\,\times\, r}_{~~~~~m~times} \to r$$</span><br />
to a value of type <span class="math-container">$\forall r.\,K\,r$</span>.</p>
<p>Curry the function <span class="math-container">$\pi_n$</span> and convert it into the equivalent function we call <span class="math-container">$\sigma_{m,n}$</span>: <span class="math-container">$$\sigma_{m,n} : \forall r.\,\underline{r\,\to\, r\,\to\,...\,\to\, r}_{~~~~~m~times} \to r$$</span></p>
<p>The code of <span class="math-container">$\sigma_{m,n}$</span> will look like this:
<span class="math-container">$$ \sigma_{m,n} \,r_1\, r_2\, ...\, r_m = r_n $$</span></p>
<p>Rewrite the type <span class="math-container">$K\,r  = \mu b.\,r + (r\to b)$</span> as: <span class="math-container">$$K \, r = r + (r\to r + (r \to r + (...)))$$</span></p>
<p>Reversing the corresponding derivation step, we find that the function <span class="math-container">$\sigma_{m,n}$</span> corresponds to the following value of type <span class="math-container">$K\,r$</span> that we will call <span class="math-container">$k_{m,n}$</span>:
<span class="math-container">$$k _{m,n} = \mathrm{Right}(\lambda r_1.\,\mathrm{Right}(\lambda r_2.\,...\,\mathrm{Right}(\lambda r_m.\,\mathrm{Left}\,r_n)...) $$</span></p>
<p>Now we need to convert this into the Church encoding of the fixpoint, that is, to a value of type:
<span class="math-container">$$ \forall b. (r + (r\to b) \to b)\to b $$</span>
or equivalently:
<span class="math-container">$$ \forall b. (r \to b) \to  ((r\to b) \to b)\to b $$</span></p>
<p>A value of this type corresponding to <span class="math-container">$k_{m,n}$</span> is <span class="math-container">$c_{m,n}$</span> defined by the Church encoding of the constructors in the fixpoint type:</p>
<p><span class="math-container">$$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)...)
$$</span></p>
<p>The last step is to set the types <span class="math-container">$r = b$</span> and substitute the identity function of type <span class="math-container">$b\to b$</span> instead of <span class="math-container">$\mathrm{left}$</span> and the argument <span class="math-container">$p: (b\to b)\to b$</span> instead of <span class="math-container">$\mathrm{right}$</span>. This corresponds to using the Yoneda identity that maps a value of type
<span class="math-container">$$ \forall r.\,(r \to b) \to  ((r\to b) \to b)\to b$$</span>
to a value of type
<span class="math-container">$$ ((b\to b) \to b)\to b$$</span></p>
<p>The result is a term of type <span class="math-container">$T$</span>:</p>
<p><span class="math-container">$$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)...)$$</span></p>
<p>This concludes the solution.</p>
<p>The example terms shown in the question can be written as:</p>
<p><span class="math-container">$$ t_{1,1} = \lambda(p: (b\to b)\to b).\,  p(\lambda r_1.\, r_1) = \lambda p.\,p\,\mathrm{id}$$</span></p>
<p><span class="math-container">$$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}) $$</span></p>
<p><span class="math-container">$$ 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))$$</span></p>
<h1>The non-disjunctivity lemma</h1>
<p>A &quot;unary&quot; type constructor <span class="math-container">$N$</span> has a single type argument. We write that as a type application <span class="math-container">$N\, r$</span>. The type constructor <span class="math-container">$N$</span> could have other type parameters but they are understood as fixed types, since we want to focus on <span class="math-container">$N$</span> as a type constructor with a single type argument.</p>
<h2>Definition of &quot;non-disjunctive type constructor&quot;</h2>
<p>A unary type constructor <span class="math-container">$N$</span> is called <b>non-disjunctive</b> if for any unary type constructors <span class="math-container">$P$</span>, <span class="math-container">$Q$</span> the following type equivalence holds:
<span class="math-container">$$ \forall r. \,N\, r\to (P\,r+Q\,r) \cong (\forall r.\,N\,r\to P\,r) + (\forall r.\,N\,r\to Q\,r) $$</span>
The type constructors <span class="math-container">$N$</span>, <span class="math-container">$P$</span>, <span class="math-container">$Q$</span> are not necessarily covariant or contravariant.</p>
<p>To see the intuition for this name, consider that a function of type <span class="math-container">$N\, r\to P\,r+Q\,r$</span> must return a value of type <span class="math-container">$P\,r$</span> or a value of type <span class="math-container">$Q\,r$</span>, that is, either the left or the right part of the disjunction <span class="math-container">$P\,r+Q\,r$</span>. Could that decision depend on a given value of type <span class="math-container">$N\,r$</span>? It could, if we could pattern match on a value of type <span class="math-container">$N\,r$</span>. But if, say, <span class="math-container">$N\,r=\mathbb 1$</span> or <span class="math-container">$N\,r = r$</span> then we cannot pattern match on those values. Then a function of type <span class="math-container">$N\, r\to P\,r+Q\,r$</span> must  hard-code the decision of returning either left or right parts for all inputs.</p>
<p>So, I say that a value of type <span class="math-container">$N\,r$</span> &quot;carries no disjunctive information&quot; (cannot be pattern matched). This is a property of <span class="math-container">$N$</span> that I call &quot;non-disjunctivity&quot;. (This is my terminology, as I don't know an established name for this property.)</p>
<h2>Some notation</h2>
<p>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.</p>
<p>We need some notation to formulate that lemma.</p>
<p>Binary relations between values of types <span class="math-container">$a$</span> and <span class="math-container">$b$</span> are denoted by <span class="math-container">$  R:a\leftrightarrow b$</span>.</p>
<p>If <span class="math-container">$R:a\leftrightarrow b$</span> is a relation then we write <span class="math-container">$(x,y)\in R$</span> if  two values <span class="math-container">$x:a$</span> and <span class="math-container">$y:b$</span> are in the relation <span class="math-container">$R$</span>.</p>
<p>Let us denote by <span class="math-container">$\bot: a\leftrightarrow b$</span> the <b>empty relation</b> (it never holds) and by <span class="math-container">$\top: A\leftrightarrow b$</span> the <b>full relation</b> (it always holds). So, for instance, we have:
<span class="math-container">$$ \forall x:a.\,\forall y:b.\,(x,y)\in \top$$</span>
<span class="math-container">$$ \forall x:a.\,\forall y:b.\,(x,y)\not\in \bot$$</span></p>
<p>We denote by &quot;id&quot; the identity relation, which is a relation of type <span class="math-container">$\forall a.\,a\leftrightarrow a$</span> such that <span class="math-container">$(x,y)\in \mathrm{id}$</span> if and only if <span class="math-container">$x=y$</span>.</p>
<p>For any unary type constructor <span class="math-container">$N$</span>, any relation <span class="math-container">$  R:a\leftrightarrow b$</span> can be lifted to a relation <span class="math-container">$  N\,R:N\,a\leftrightarrow N\,b$</span>. This is quite similar to lifting a function <span class="math-container">$f:a\to b$</span> to a function <span class="math-container">$N\,f:N\,a\to N\,b$</span> except that a function can be lifted only if <span class="math-container">$N$</span> is covariant; but a relation can always be lifted (within System F or System F<span class="math-container">$\omega$</span>), even if <span class="math-container">$N$</span> 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 <span class="math-container">$N$</span>.</p>
<p>Finally, the parametricity theorem for unary type constructors says that any &quot;purely parametrically polymorphic&quot; value  <span class="math-container">$f:\forall a.\,F\,a$</span> (this covers any code written in System F or System F<span class="math-container">$\omega$</span>) satisfies the relational naturality law:</p>
<p><span class="math-container">$$ \forall a: \mathrm{Type}.\,\forall b: \mathrm{Type}.\, \forall R:a\leftrightarrow b.\, (f\, a, f\, b)\in F \,R $$</span></p>
<p>Remark:</p>
<p>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?</p>
<h2>The non-disjunctivity lemma</h2>
<p>A unary type constructor <span class="math-container">$N$</span> is non-disjunctive if <span class="math-container">$N$</span> is not identically void (<span class="math-container">$N\,r\not =\mathbb0$</span> for some <span class="math-container">$r$</span>) and if for any types <span class="math-container">$a$</span> and <span class="math-container">$b$</span> such that <span class="math-container">$N\,a \not =\mathbb0$</span> and <span class="math-container">$N\,b \not =\mathbb0$</span> there exists a relation <span class="math-container">$R:a\leftrightarrow b$</span> for which <span class="math-container">$N\,R = \top$</span>.</p>
<p>Proof.</p>
<p>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.</p>
<p>Choose types <span class="math-container">$a$</span>, <span class="math-container">$b$</span> and a relation <span class="math-container">$R:a\leftrightarrow b$</span> satisfying the stated assumptions. Take any function <span class="math-container">$f:\forall r. \,N\, r\to P\,r+Q\,r$</span>. Denote for brevity: <span class="math-container">$$F \,r = N\, r\to P\,r+Q\,r$$</span> <span class="math-container">$$G\,r = P\,r + Q\,r $$</span></p>
<p>Write the relational naturality law of <span class="math-container">$f$</span> with parameters <span class="math-container">$a$</span>,<span class="math-container">$b$</span>,<span class="math-container">$R$</span>:</p>
<p><span class="math-container">$$ (f\,a, f\,b)\in F \,R $$</span></p>
<p>Expand the relation <span class="math-container">$F\, R$</span> according to the rules of relational lifting for function types:</p>
<p><span class="math-container">$$\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 $$</span></p>
<p>By assumption, <span class="math-container">$N\,R=\top$</span> and so we will always have <span class="math-container">$(x,y)\in N\, R $</span>. So, we can simplify the relational naturality law of <span class="math-container">$f$</span>:</p>
<p><span class="math-container">$$\forall x:N\,a.\,\forall y:N\,b.\,   (f\, a \,x, f\, b\, y)\in G\,R $$</span></p>
<p>But <span class="math-container">$G\,r$</span> is a co-product type. Apply the rules of relational lifting for co-products. The law of <span class="math-container">$f$</span> becomes a disjunction of two conditions:</p>
<p><span class="math-container">$$\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 $$</span></p>
<p>By assumption, the types <span class="math-container">$N\,a$</span> and <span class="math-container">$N\,b$</span> are not void, so we may fix a specific value <span class="math-container">$x_0:N\,a$</span>. Then <span class="math-container">$f\,a\,x_0$</span>  is in either &quot;Left&quot; or &quot;Right&quot; part of the co-product <span class="math-container">$P\,a+Q\,a$</span>. Suppose it is a &quot;Left&quot; (the proof will be analogous if it is a &quot;Right&quot;). Then denote <span class="math-container">$p_0 : P \,a = f \,a\,x_0$</span> and simplify the above condition to:</p>
<p><span class="math-container">$$ \forall b:\mathrm{Type}.\,\forall y:N\,b.\,   f\, b\, y = \mathrm{Left}\,p_2 \mathrm{~and~}(p_0,p_2)\in P\,R   $$</span></p>
<p>Incidentally, this is the relational naturality law for functions of type <span class="math-container">$\forall r.\, N\,r\to P\,r$</span> if we substitute <span class="math-container">$x_0$</span> and <span class="math-container">$a$</span> into that law.</p>
<p>So, it follows that <span class="math-container">$f\,b\,y$</span> is also in the &quot;Left&quot; part for all <span class="math-container">$y$</span> (and for all types <span class="math-container">$b$</span>).</p>
<p>So, parametricity enforces that the function <span class="math-container">$f$</span> always returns a &quot;Left&quot; for all inputs of all types, as long as <span class="math-container">$f$</span> returns a &quot;Left&quot; for just one value <span class="math-container">$x_0$</span> of just one type <span class="math-container">$a$</span>. And parametricity also enforces the same law on functions of type <span class="math-container">$\forall r.\, N\,r\to P\,r$</span>.</p>
<p>We conclude that the type of functions  <span class="math-container">$f:\forall r.\, N\,r\to P\,r + Q\,r$</span> such that there exists <span class="math-container">$x_0:N\,a$</span> with <span class="math-container">$f\,a\,x_0 = \mathrm{Left}\,p_0$</span> are isomorphic to the type <span class="math-container">$\forall r.\, N\,r\to P\,r$</span>.</p>
<p>Similarly for the &quot;Right&quot; variant. If <span class="math-container">$f$</span> returns a &quot;Right&quot; even just for one type <span class="math-container">$a$</span> and for one input <span class="math-container">$x_0:N\,a$</span> then <span class="math-container">$f$</span> always returns a &quot;Right&quot;.</p>
<p>Now we can demonstrate an isomorphism between types <span class="math-container">$$\forall r.\, N\,r\to P\,r+Q\,r$$</span> and <span class="math-container">$$(\forall r.\, N\,r\to P\,r)+\forall r.\, N\,r\to Q\,r$$</span></p>
<p>A value of the latter type is either a &quot;Left&quot; or a &quot;Right&quot;. Suppose it is a &quot;Left&quot; (the consideration will be analogous if it is a &quot;Right&quot;). Then it is a <span class="math-container">$\mathrm{Left}\,k$</span> for some <span class="math-container">$k: \forall r.\, N\,r\to P\,r$</span>. Also, <span class="math-container">$k$</span> satisfies the relational naturality law for functions of type <span class="math-container">$\forall r.\, N\,r\to P\,r$</span>. The isomorphism maps <span class="math-container">$k$</span> to a function <span class="math-container">$f$</span> of type <span class="math-container">$\forall r.\, N\,r\to P\,r + Q\,r$</span> that always returns a <span class="math-container">$\mathrm{Left}\,(P\,r)$</span>. We define <span class="math-container">$f$</span> by:
<span class="math-container">$$f \, r\, x = \mathrm{Left}\,(k\,r\,x)$$</span>
The function <span class="math-container">$f$</span> satisfies its relational naturality law because it's equivalent to that of <span class="math-container">$k$</span>, as we have seen.</p>
<p>So, the set of all purely parametric <span class="math-container">$k$</span> of type &quot;Left&quot; is in a one-to-one correspondence with the set of all purely parametric <span class="math-container">$f$</span> that always return &quot;Left&quot;.</p>
<p>Similarly,  the set of all purely parametric <span class="math-container">$k$</span> of type &quot;Right&quot; is in a one-to-one correspondence with the set of all purely parametric <span class="math-container">$f$</span> that always return &quot;Right&quot;.</p>
<p>We have shown that there are no <span class="math-container">$f$</span> that sometimes return &quot;Left&quot; and sometimes return &quot;Right&quot;. So, the entire type <span class="math-container">$\forall r.\, N\,r\to P\,r+Q\,r$</span> is in a one-to-one correspondence with the entire type <span class="math-container">$(\forall r.\, N\,r\to P\,r)+\forall r.\, N\,r\to Q\,r$</span>.</p>
<p>Q.E.D.</p>
<h2>Examples of non-disjunctive type constructors</h2>
<p>To show that a type constructor <span class="math-container">$N$</span> is non-disjunctive, we just need to give an example of a relation <span class="math-container">$R$</span> that is lifted by <span class="math-container">$N$</span> to a full relation (<span class="math-container">$N\,R=\top$</span>). The rest follows from the non-disjunctivity lemma.</p>
<p>Here are some examples:</p>
<ol>
<li>The constant unit type constructor.</li>
</ol>
<p>Let <span class="math-container">$N\,r = \mathbb 1$</span>, then any relation <span class="math-container">$R:a\leftrightarrow b$</span> is lifted to <span class="math-container">$N\,R = \mathrm{id}$</span>. But the identity relation on the unit type is a full relation (the unit type has only one value).</p>
<ol start="2">
<li>The identity functor.</li>
</ol>
<p>Let <span class="math-container">$N\,r = r$</span>, then lifting is trivial (<span class="math-container">$N\,R = R$</span> for any relation <span class="math-container">$R$</span>). So, the full relation is lifted again to the full relation.</p>
<ol start="3">
<li>A function from any type to a non-disjunctive type constructor.</li>
</ol>
<p>Let <span class="math-container">$N\,r = L\, r\to M\,r$</span> where <span class="math-container">$M$</span> is non-disjunctive. We want to show that there exists some <span class="math-container">$R$</span> such that <span class="math-container">$N\,R = \top$</span>.</p>
<p>We know that there exists <span class="math-container">$R$</span> such that <span class="math-container">$M\,R=\top$</span>; the same <span class="math-container">$R$</span> will do, as we now show. Write the relational naturality law for functions <span class="math-container">$f$</span> of type <span class="math-container">$N\,r$</span>. Values <span class="math-container">$f\,a$</span> and <span class="math-container">$f\,b$</span> are in the relation <span class="math-container">$N \,R$</span> when:
<span class="math-container">$$ \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$$</span></p>
<p>This is a conditional statement whose consequence is always true. So, the statement is also always true, so <span class="math-container">$f\,a$</span> and <span class="math-container">$f\,b$</span> are always in the relation <span class="math-container">$N\,R$</span>. It means that <span class="math-container">$N\,R=\top$</span>.</p>
<p>A consequence is that <span class="math-container">$N\,r = \underline{r\,\times \,r\,\times\, ...\,\times\,r}_{~~~~~n~times} = \mathbb n\to r$</span> is non-disjunctive.</p>
<p>Also note that <span class="math-container">$L$</span> could be any type constructor, including a co-product, but it is not at top level in <span class="math-container">$L\, r\to M\,r$</span> and so <span class="math-container">$N$</span> is still non-disjunctive.</p>
<ol start="4">
<li>A function from <span class="math-container">$r$</span> to any type constructor.</li>
</ol>
<p>Let <span class="math-container">$N\,r = r\to M\,r$</span> where <span class="math-container">$M$</span> is any type constructor. Take <span class="math-container">$R=\bot$</span> and lift to <span class="math-container">$N$</span>. Then <span class="math-container">$f\,a$</span> and <span class="math-container">$f\,b$</span> are in the relation <span class="math-container">$N\,R$</span> when:</p>
<p><span class="math-container">$$\forall x:a.\, \forall y: b.\,\mathrm{~if~} (x, y)\in R   \mathrm{~then~} (f\, a\, x, f\, b\, y) \in M \,R$$</span></p>
<p>This is a conditional statement whose premise is always false as <span class="math-container">$R=\bot$</span> and <span class="math-container">$(x,y)\not\in \bot $</span> for any <span class="math-container">$x$</span>, <span class="math-container">$y$</span>. So, the conditional statement is always true. It means that <span class="math-container">$f\,a$</span> and <span class="math-container">$f\,b$</span> are always in the relation <span class="math-container">$N\,R$</span>; that is, <span class="math-container">$N\,R=\top$</span>.</p>
<h1>Example: List Nat</h1>
<p>Using the techniques developed here, we can prove the following type equivalence:</p>
<p><span class="math-container">$$ \mathrm{List}\, \mathrm{Nat} = \mathbb 1 + \mathrm{Nat} + \mathrm{Nat} \times \mathrm{Nat}  \,+ \, ...$$</span>
<span class="math-container">$$ \cong (\mathbb 0\to \mathrm{Nat}) + (\mathbb 1 \to \mathrm{Nat})  + (\mathbb 2 \to \mathrm{Nat}) \,+\, ... $$</span>
<span class="math-container">$$\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))   \,+\, ...
$$</span>
<span class="math-container">$$\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))   \,+\, ...
$$</span>
<span class="math-container">$$\cong \forall a.\, (a \to a) +
  (   (a\to a)\to(a \to a)) +
  ((a\to a)\to  (a\to a)\to(a \to a))   \,+\, ...
$$</span></p>
<p>The type constructor <span class="math-container">$N\, a = a \to a$</span> is non-disjunctive (via Example 2 and Example 3 above). So, we can rewrite the type as:</p>
<p><span class="math-container">$$ \forall a.\, N\,a +(   N\,a\to N\,a) +
  (N\,a\to  N\,a\to N\,a)   \,+\, ... $$</span>
<span class="math-container">$$\cong \forall a.\, N\,a +
  (   N\,a\to (N\,a +
  (N\,a\to  (N\,a\,+\, ...))...)
$$</span></p>
<p>The last type can be written as <span class="math-container">$\forall a.\, K\, a$</span> where we define <span class="math-container">$K$</span> recursively as:
<span class="math-container">$$K\, a = (a \to a) + ((a \to a) \to K\, a) $$</span></p>
<p>or <span class="math-container">$$K\, a = \mu b.\,(a \to a) + ((a \to a) \to b)$$</span></p>
<p>This is the least fixpoint of a positive type constructor. So, it can be rewritten via the Church encoding:</p>
<p><span class="math-container">$$K\, a = \forall b.\, (((a \to a) + ((a \to a) \to b)) \to b)\to b$$</span></p>
<p><span class="math-container">$$\cong \forall b.\, ((a \to a) \to b)\to  ((a \to a) \to b) \to b)\to b$$</span></p>
<p>Finally, imposing the quantifier <span class="math-container">$\forall a$</span>, we get the type equivalence:</p>
<p><span class="math-container">$$\mathrm{List}\, \mathrm{Nat} \cong \forall a.\,\forall b.\, ((a \to a) \to b)\to  ((a \to a) \to b) \to b)\to b$$</span></p>

CC BY-SA 4.0
2024-02-03T20:02:09.833Z
To write the term, you just repeat $p (\lambda x.$ nesting $m$ times, and then pick the $n$-th variable in the end.
Trebor
CC BY-SA 4.0
2024-02-03T20:55:14.703Z
@Trebor Yes, this looks right. I will write up the solution.
winitzki
CC BY-SA 4.0
2024-02-04T08:13:20.333Z
Although, in what sense is $\forall x. F x + G x$ equivalent to $(\forall x. F x) + (\forall x. G x)$? You can write a function in one way but not the other. Maybe you can prove that the function is observationally an injection and a surjection?
Trebor
CC BY-SA 4.0
2024-02-04T11:27:13.880Z
@Trebor This is a nontrivial type equivalence that holds only under assumptions of parametricity. Similarly $\forall r.\,r\to F\,r + G\, r = (\forall r.\, r\to F\, r) + (\forall r.\,r\to G\,r)$ holds only due to parametricity. Perhaps I need to write this out in detail.
winitzki
CC BY-SA 4.0
2024-02-04T13:12:49.100Z
Well it's different from other instances of parametricity-induced equivalences. $\forall r. r \to r$ is isomorphic to Unit and I can write down that isomorphism. I just need parametricity to prove the relevant equalities. Here I can't even write the function without appealing to some parametricity argument.
Trebor
CC BY-SA 4.0
2024-02-04T17:40:50.010Z
@Trebor I think we can just write one direction of the isomorphism and then prove, using parametricity, that all fully parametric functions of type $\forall r.\,r\to F\,r + G\,r$ are in the image of that isomorphism.
winitzki
CC BY-SA 4.0
2024-02-05T13:19:32.693Z
This deserves to be a blog post or something. Some of the long formulas overflows to the right in stackexchange. (+1)
Trebor
CC BY-SA 4.0
2024-02-05T13:23:57.080Z
A remaining question (maybe ask a new one) is, why is it more "natural" to say that the type equals (1 + 2 + ...) than (1 + 1 + ...), since there are isomorphisms between these two types? Perhaps the "seven trees in one" paper can be applied here...
Trebor
CC BY-SA 4.0
2024-02-27T15:33:33.073Z
@Trebor The structure of the type (1 + 2 + 3 + ...) directly describes the various $\lambda$-terms corresponding to the type $\forall a.\,((a\to a)\to a)\to a$. If you write 1 + 1 + 1 + ... then you lose that structure.
winitzki
CC BY-SA 4.0
2024-02-03T19:40:52.500Z
2024-02-07T08:39:58.483Z
2024-02-07T08:39:58.483Z
winitzki
<p>Using syntactic methods, it's quite easy to see the correspondence between <span class="math-container">$\forall \alpha. ((\alpha \to \alpha) \to \alpha) \to \alpha$</span> and <span class="math-container">$1 + 2 + 3 + \dots$</span> You already had that intuition, and it can be turned into a formal argument in a more direct way than going through semantic parametricity.</p>
<p><strong>Claim 1.</strong> In System F, the closed <span class="math-container">$\beta$</span>-normal terms of type <span class="math-container">$\forall \alpha. ((\alpha \to \alpha) \to \alpha) \to \alpha$</span> are all of the form <span class="math-container">$\lambda f. f (\lambda x_1. f(\lambda x_2.\;\dots f(\lambda x_n. x_i)\dots))$</span>, where <span class="math-container">$1 \le i \le n$</span>.</p>
<p>The intuition comes from trying to write down some normal terms of that type by hand yourself. Proof of <strong>Claim 1</strong> in the appendix below.</p>
<p><strong>Claim 1</strong> really describes a bijection between those normal terms and pairs of numbers <span class="math-container">$(n,i)$</span> where <span class="math-container">$i &lt; n$</span>. This can also be written as a dependent sum type <span class="math-container">$\sum_{1\le n}[n]$</span> where <span class="math-container">$[n] = \{1, \dots, n\}$</span>. Hence &quot;<span class="math-container">$1 + 2 + 3 + \dots$</span>&quot; And of course that is isomorphic to just <span class="math-container">$\mathbb{N}$</span>.</p>
<p>The bijection in <strong>Claim 1</strong> is a function <em>on</em> System F terms, a <em>metaprogram</em>. The next claim is that it is also definable as a program <em>in</em> System F.</p>
<p>While we're at it, we can avoid the burden of representing the dependent sum in &quot;<span class="math-container">$(n,i) \in \sum_{1\le n} [n]$</span>&quot; in System F. With a change of variables <span class="math-container">$n = 1 + i + j$</span> and a switch to 0-indexing, the pair of indices <span class="math-container">$(i,j)$</span> now ranges over a simple product type <span class="math-container">$\mathbb{N}\times\mathbb{N}$</span>.</p>
<p><strong>Claim 2.</strong> There is a function <span class="math-container">$W$</span> definable in System F, of type <span class="math-container">$$W : \mathbb{N}\times\mathbb{N} \to (\forall \alpha. ((\alpha\to\alpha)\to\alpha)\to\alpha)$$</span> such that <span class="math-container">$$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)$$</span></p>
<p><strong>Proof.</strong> <span class="math-container">$W = \lambda(i,j). \mathrm{iter}\,i\,(\lambda y.f (\lambda \_.y))\, (f (\lambda x. \mathrm{iter}\,j\,(\lambda y.f(\lambda \_.y))\,x))$</span><br />
where <span class="math-container">$\mathrm{iter}$</span> is the recursor of <span class="math-container">$\mathbb{N}$</span>: <span class="math-container">$$\begin{align*}\mathrm{iter}&amp;:\mathbb{N} \to (\alpha \to \alpha) \to \alpha \to \alpha\\ \mathrm{iter}\,0\,f\,x &amp;= x\\\mathrm{iter}\,(1+n)\,f\,x &amp;= f (\mathrm{iter}\,n\,f\,x)\end{align*}$$</span> □</p>
<p>Having enumerated <span class="math-container">$\beta$</span>-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:</p>
<p><strong>Claim 3.</strong> There is a function <span class="math-container">$X$</span> (for &quot;eXamine&quot;) definable in System F, of type <span class="math-container">$$X : (\forall \alpha. ((\alpha \to \alpha) \to \alpha) \to \alpha) \to \mathbb{N}\times\mathbb{N}$$</span> such that for every <span class="math-container">$(i,j)\in\mathbb{N}\times\mathbb{N}$</span>, we can recover those indices out of <span class="math-container">$W(i,j)$</span> using <span class="math-container">$X$</span>: <span class="math-container">$$X (W(i,j)) =_\beta (i, j)$$</span></p>
<p>The proof, including the definition of <span class="math-container">$X$</span>, is too technical to be illuminating in prose, so <a href="https://gist.github.com/Lysxia/a2d73f3bbf2480b0d47c40d1304078a3" rel="nofollow noreferrer">here is a variant of it in Coq instead</a>.</p>
<p>We now have the two directions of the isomorphism between <span class="math-container">$\forall \alpha. ((\alpha\to\alpha)\to\alpha)\to\alpha$</span> and <span class="math-container">$\mathbb{N}\times\mathbb{N}$</span> defined in System F. Those functions are mutually inverses modulo <span class="math-container">$\beta$</span>-equivalence:</p>
<ul>
<li><span class="math-container">$X (W(i,j)) =_\beta (i,j)$</span>, for any closed terms <span class="math-container">$(i,j) \in \mathbb{N}\times\mathbb{N}$</span>.</li>
<li><span class="math-container">$W (X t) =_\beta t$</span>, for any closed term <span class="math-container">$t : \forall \alpha.((\alpha\to\alpha)\to\alpha)\to\alpha$</span>.</li>
</ul>
<p>Those imply the following contextual equivalences. This is mainly an excuse to write the isomorphism laws in pointfree form:</p>
<ul>
<li><span class="math-container">$X \circ W =_\mathrm{ctx} \mathrm{id}_{\mathbb{N}\times\mathbb{N}}$</span></li>
<li><span class="math-container">$W \circ X =_\mathrm{ctx} \mathrm{id}_{\forall\alpha.((\alpha\to\alpha)\to\alpha)\to\alpha}$</span></li>
</ul>
<hr />
<p>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 (&quot;for all denotations (that satisfy some &quot;parametricity&quot; theorem)&quot;), 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 <strong>Claim 1</strong>).</p>
<hr />
<h3>Appendix</h3>
<p><strong>Proof of Claim 1.</strong> In System F, <span class="math-container">$\beta$</span>-normal terms are necessarily lambdas over the application of a variable: <span class="math-container">$\lambda f. f M$</span>, where <span class="math-container">$M$</span> is an open term subject to the typing judgement <span class="math-container">$\alpha : \star, f : (\alpha \to\alpha)\to\alpha \vdash M : \alpha \to \alpha$</span>. You can keep expanding that way by hand to see the pattern. The following <strong>Lemma 1.a</strong> makes it formal. Refining <span class="math-container">$M = \lambda x_1. M'$</span>, and applying <strong>Lemma 1.a</strong> with <span class="math-container">$n = 1$</span> concludes the proof of <strong>Claim 1</strong>. □</p>
<p><strong>Lemma 1.a.</strong> <span class="math-container">$\beta$</span>-normal terms <span class="math-container">$M$</span> of type <span class="math-container">$\alpha : \star, f : (\alpha\to\alpha)\to\alpha, x_1:\alpha, \dots, x_n:\alpha \vdash M : \alpha$</span> are of the form <span class="math-container">$f (\lambda x_{n+1}.\;\dots f(\lambda x_m. x_i)\dots)$</span> where <span class="math-container">$n \le m$</span> and <span class="math-container">$i \le m$</span>.</p>
<p><strong>Proof.</strong> By induction on <span class="math-container">$n$</span>. Either <span class="math-container">$M$</span> is a variable, <span class="math-container">$M = x_i$</span> (concluding the proof with <span class="math-container">$m = n$</span>). Or <span class="math-container">$M$</span> is an application of <span class="math-container">$f$</span>, <span class="math-container">$M = f (\lambda x_{n+1}.N)$</span>, and <span class="math-container">$N$</span> is of type <span class="math-container">$$\alpha : \star,f : (\alpha \to \alpha) \to \alpha, x_1 : \alpha,\dots x_{n+1} : \alpha \vdash N : \alpha$$</span> and we conclude by induction hypothesis. □</p>

CC BY-SA 4.0
2024-04-11T00:52:17.173Z
2024-04-11T00:52:17.173Z
Li-yao Xia
<p>They are inequivalent. Let's number the three <span class="math-container">$\phi$</span> you listed as <span class="math-container">$\phi_1, \phi_2, \phi_3$</span>. Then <span class="math-container">$\phi_1 \mathbb N (\lambda f. f(0)+1) = 1$</span>, while <span class="math-container">$\phi_2, \phi_3$</span> both give the result <span class="math-container">$2$</span>. 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.</p>
<p>This type is very messy and does not admit simplifications. It's almost the least fixedpoint <span class="math-container">$\mu X. (X \to X)$</span> (except that it isn't, because of positivity issues). Or in Haskell notation, <code>data Term = Lam (Term -&gt; Term)</code>. You can fit the entire untyped lambda calculus inside of this type! Your <span class="math-container">$\phi_1$</span> translates to <code>Lam \x -&gt; x</code>, so it's the encoding of the UTLC term <span class="math-container">$\lambda x. x$</span>; and <span class="math-container">$\phi_2$</span> is <code>Lam \x -&gt; Lam \y -&gt; y</code>, so it encodes the UTLC term <span class="math-container">$K$</span>, and your <span class="math-container">$\phi_3$</span> encodes <span class="math-container">$KI$</span>.</p>

CC BY-SA 4.0
2024-02-03T15:55:53.487Z
I found a way to rewrite the type $T$ using Yoneda and Church encoding as a least fixpoint of a positive type. See my answer here https://stackoverflow.com/questions/61444425/is-there-a-non-identity-monad-morphism-m-m-that-is-monadically-natural-in-m/77926520 The equivalent type is ∀(b: Type). µ r. b + (b → r)  or another equivalent form is ∀(b: Type). µ r. b → (b + r). But I'm still not able to simplify this rigorously to anything like Nat. My current hypothesis is that this type is equivalent to Nat.
winitzki
CC BY-SA 4.0
2024-02-03T15:59:49.950Z
Here's what I'm trying to do. Denote R b =  µ r. b → (b + r). Then R b = b → (b + R b). Now we need to use parametricity somehow to show that the type ∀b. b → (b + R b) must be equivalent to ∀b. (b → b) + (b → R b). I expect this to be true because a function of type ∀b. b → (b + R b) cannot decide to return the left or the right part of b + R b depending on an argument of type b. That kind of function must hard-code the decision to return  the left or the right part of b + R b. Then we have ∀b. (b → b) + ∀b. (b → R b). This is just 1 + R 1. But R 1 = Nat. So, we get 1 + Nat and that's Nat.
winitzki
CC BY-SA 4.0
2024-02-03T16:52:28.203Z
@winitzki It's a bit much to follow. What's the isomorphism between the type in this question and the starting point of your comment? If I follow correctly, this isomorphism is just counting how many times you use the `p : (a -> a) -> a`?
Trebor
CC BY-SA 4.0
2024-02-03T16:58:35.750Z
No it cannot be the case, because `p x = x(x 1) + 1` separates $\phi_2$ and $\phi_3$. What is it then?
Trebor
CC BY-SA 4.0
2024-02-03T17:15:35.660Z
I don't yet understand if really $T = \mathrm{Nat}$ and if so, what is the meaning of $\phi_1$, $\phi_2$, $\phi_3$. There are terms of type $T$ that use $p$ in different ways, it cannot be just the counting of how many times $p$ is applied. Let me try to write my answer with more details, although I'm not actually sure it's correct.
winitzki
CC BY-SA 4.0
2024-02-03T19:42:32.613Z
My reasoning about R 1 and T = Nat was incorrect. Now I believe that T = 1 + 2 + 3 + ... rather than T = Nat = 1 + 1 + 1 + ..., so have written my attempt at an answer but I'm still not sure how to write lambda-terms that correspond to various possibilities.
winitzki
CC BY-SA 4.0
2024-02-05T13:13:20.603Z
I revised my answer and added a full proof. By the way, do you know how to simplify $\mu X. \,X\to X$? Is it equivalent to $T$? It seems we can write terms of the form $\lambda x_1.\,\lambda x_2.\,...\,\lambda x_m.\, x_n$ as we do for $T$. Can we write any other, inequivalent terms of type $\mu X. \,X\to X$?
winitzki
CC BY-SA 4.0
2024-02-05T13:17:55.157Z
@winitzki No, this type breaks normalization since you can encode general recursion in it. Consider $(\lambda x. \textsf{unroll}\,x\,x)(\textsf{roll}(\lambda x. \textsf{unroll}\,x\,x))$, where $\textsf{roll} : (C \to C) \to C$ is the constructor, and $\textsf{unroll}$ the destructor.
Trebor
CC BY-SA 4.0
2024-02-03T12:22:11.060Z
2024-02-03T12:40:23.773Z
2024-02-03T12:40:23.773Z
Trebor
<p>This question is about using relational parametricity to resolve practical questions in pure functional programming in System F.</p>
<p>Consider the following type  of polymorphic functions:</p>
<p><span class="math-container">$$T = \forall a. ( (a \to a) \to a ) \to a $$</span></p>
<p>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>
<p>My initial hypothesis is that this type is equivalent to the unit type (<span class="math-container">$\mathbb1$</span>). However, this may turn out to be wrong.</p>
<p>In any case, the type <span class="math-container">$T$</span> is certainly not void. There is a term <span class="math-container">$\phi : T$</span>:
<span class="math-container">$$\phi = \lambda(a: Type). \lambda\,(p:(a \to a) \to a). p \,\mathrm{id} $$</span></p>
<p>where &quot;id&quot; is the identity function, <span class="math-container">$ id = (\lambda\,(x: a). x)$</span>.</p>
<p>Some other terms of type <span class="math-container">$T$</span> are:</p>
<p><span class="math-container">$$ \phi =\lambda(a: Type). \lambda\,(p:(a \to a) \to a).\, p \,(\lambda\, \_. p\, \mathrm{id})$$</span></p>
<p><span class="math-container">$$ \phi =\lambda(a: Type). \lambda\,(p:(a \to a) \to a).\, p \,(\lambda\, (x : a).\, p\,  (\lambda\,_.\,x))$$</span></p>
<p>There seems to be infinitely many possible terms of that type, but it is not clear if they are all inequivalent, given parametricity constraints.</p>
<p>How to derive the type equivalence <span class="math-container">$T\cong\mathbb1$</span> or, if that is incorrect, another type equivalence rigorously?</p>
<p>I tried writing down a relational law satisfied by functions of the   type <span class="math-container">$ T$</span> but it's complicated and I didn't figure out how to prove that there is only one value of that type.</p>
<p>The relational law should prove that, for any function <span class="math-container">$\phi : T$</span> and for any value <span class="math-container">$p : (a \to a)\to a$</span>, the result of the application <span class="math-container">$\phi \,p$</span> is always equal to <span class="math-container">$p\, \mathrm{id}$</span>.</p>
<p>The relational law of <span class="math-container">$\phi$</span> looks like this:</p>
<p>For any two types <span class="math-container">$a$</span>, <span class="math-container">$b$</span>, and for any relation <span class="math-container">$r:a\leftrightarrow b$</span> between values of types <span class="math-container">$a$</span> and <span class="math-container">$b$</span>:</p>
<p>If two functions <span class="math-container">$p: (a \to a)\to a$</span> and <span class="math-container">$q: (b \to b)\to b$</span> are in a relation <span class="math-container">$s$</span> then the values <span class="math-container">$\phi\,p$</span> and <span class="math-container">$\phi\, q$</span> are in the relation <span class="math-container">$r$</span>.</p>
<p>The relation <span class="math-container">$s$</span> is defined by: <span class="math-container">$p: (a \to a)\to a$</span> and <span class="math-container">$q: (b \to b)\to b$</span> are in <span class="math-container">$s$</span> if, for any <span class="math-container">$i: a\to a$</span> and <span class="math-container">$j: b\to b$</span> such that <span class="math-container">$i$</span> and <span class="math-container">$j$</span> are in the relation <span class="math-container">$t$</span>, we will have the values <span class="math-container">$p\, i$</span> and <span class="math-container">$q \, j$</span> in the relation <span class="math-container">$r$</span>.</p>
<p>The relation <span class="math-container">$t$</span> is defined by: <span class="math-container">$i: a\to a$</span> and <span class="math-container">$j: b\to b$</span>  are in <span class="math-container">$t$</span> if, for any <span class="math-container">$x: a$</span> and <span class="math-container">$y: b$</span> such that <span class="math-container">$x$</span> and <span class="math-container">$y$</span> are in the relation <span class="math-container">$r$</span>, we will have the values <span class="math-container">$i\, x$</span> and <span class="math-container">$j\,y$</span> are in the relation <span class="math-container">$r$</span>.</p>
<p>This is a complicated set of conditions and it is not clear how to use them.</p>
<p>We can simplify these conditions if we choose the relation <span class="math-container">$r$</span> as a function: <span class="math-container">$(x, y)\in r$</span> if <span class="math-container">$f(x) = y$</span> with a fixed chosen function <span class="math-container">$f: a\to b$</span>.</p>
<p>Then we obtain the following condition: For any <span class="math-container">$p: (a \to a)\to a$</span> and <span class="math-container">$q: (b \to b)\to b$</span> that are in relation <span class="math-container">$s$</span>, we will have <span class="math-container">$f(\phi\,p) = \phi q$</span>.</p>
<p>The relation <span class="math-container">$s$</span> is defined by: <span class="math-container">$p: (a \to a)\to a$</span> and <span class="math-container">$q: (b \to b)\to b$</span> are in <span class="math-container">$s$</span> if, for any <span class="math-container">$i: a\to a$</span> and <span class="math-container">$j: b\to b$</span> such that <span class="math-container">$f . i = j . f$</span>, we will have <span class="math-container">$f(p (i)) = q(j)$</span>.</p>
<p>This condition is somewhat simpler but I am still not able to use it to prove that any function <span class="math-container">$\phi: T$</span> is always of the form <span class="math-container">$\lambda\,p.\,p\,\mathrm{id}$</span>. (That would be to prove that <span class="math-container">$T \cong\mathbb1$</span>.)</p>

<type-theory><functional-programming><typed-lambda-calculus><parametricity>
Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?
winitzki
# Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?

(Asked by: username_0 on 2024-02-02)

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

**Tags:** type-theory, functional-programming, typed-lambda-calculus, parametricity

---

## 3 answers

### Answer by username_0 on 2024-02-03. Score: 2 | Accepted answer

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

> **Comments:**
> **username_1**: To write the term, you just repeat $p (\lambda x.$ nesting $m$ times, and then pick the $n$-th variable in the end.  
> **username_0**: @Trebor Yes, this looks right. I will write up the solution.  
> **username_1**: Although, in what sense is $\forall x. F x + G x$ equivalent to $(\forall x. F x) + (\forall x. G x)$? You can write a function in one way but not the other. Maybe you can prove that the function is observationally an injection and a surjection?  
> **username_0**: @Trebor This is a nontrivial type equivalence that holds only under assumptions of parametricity. Similarly $\forall r.\,r\to F\,r + G\, r = (\forall r.\, r\to F\, r) + (\forall r.\,r\to G\,r)$ holds only due to parametricity. Perhaps I need to write this out in detail.  
> **username_1**: Well it's different from other instances of parametricity-induced equivalences. $\forall r. r \to r$ is isomorphic to Unit and I can write down that isomorphism. I just need parametricity to prove the relevant equalities. Here I can't even write the function without appealing to some parametricity argument.  
> **username_0**: @Trebor I think we can just write one direction of the isomorphism and then prove, using parametricity, that all fully parametric functions of type $\forall r.\,r\to F\,r + G\,r$ are in the image of that isomorphism.  
> **username_1**: This deserves to be a blog post or something. Some of the long formulas overflows to the right in stackexchange. (+1)  
> **username_1**: A remaining question (maybe ask a new one) is, why is it more "natural" to say that the type equals (1 + 2 + ...) than (1 + 1 + ...), since there are isomorphisms between these two types? Perhaps the "seven trees in one" paper can be applied here...  
> **username_0**: @Trebor The structure of the type (1 + 2 + 3 + ...) directly describes the various $\lambda$-terms corresponding to the type $\forall a.\,((a\to a)\to a)\to a$. If you write 1 + 1 + 1 + ... then you lose that structure.  

---

### Answer by username_2 on 2024-04-11. Score: 3

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](https://gist.github.com/Lysxia/a2d73f3bbf2480b0d47c40d1304078a3).

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 by username_1 on 2024-02-03. Score: 0

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

> **Comments:**
> **username_0**: I found a way to rewrite the type $T$ using Yoneda and Church encoding as a least fixpoint of a positive type. See my answer here https://stackoverflow.com/questions/61444425/is-there-a-non-identity-monad-morphism-m-m-that-is-monadically-natural-in-m/77926520 The equivalent type is ∀(b: Type). µ r. b + (b → r)  or another equivalent form is ∀(b: Type). µ r. b → (b + r). But I'm still not able to simplify this rigorously to anything like Nat. My current hypothesis is that this type is equivalent to Nat.  
> **username_0**: Here's what I'm trying to do. Denote R b =  µ r. b → (b + r). Then R b = b → (b + R b). Now we need to use parametricity somehow to show that the type ∀b. b → (b + R b) must be equivalent to ∀b. (b → b) + (b → R b). I expect this to be true because a function of type ∀b. b → (b + R b) cannot decide to return the left or the right part of b + R b depending on an argument of type b. That kind of function must hard-code the decision to return  the left or the right part of b + R b. Then we have ∀b. (b → b) + ∀b. (b → R b). This is just 1 + R 1. But R 1 = Nat. So, we get 1 + Nat and that's Nat.  
> **username_1**: @winitzki It's a bit much to follow. What's the isomorphism between the type in this question and the starting point of your comment? If I follow correctly, this isomorphism is just counting how many times you use the `p : (a -> a) -> a`?  
> **username_1**: No it cannot be the case, because `p x = x(x 1) + 1` separates $\phi_2$ and $\phi_3$. What is it then?  
> **username_0**: I don't yet understand if really $T = \mathrm{Nat}$ and if so, what is the meaning of $\phi_1$, $\phi_2$, $\phi_3$. There are terms of type $T$ that use $p$ in different ways, it cannot be just the counting of how many times $p$ is applied. Let me try to write my answer with more details, although I'm not actually sure it's correct.  
> **username_0**: My reasoning about R 1 and T = Nat was incorrect. Now I believe that T = 1 + 2 + 3 + ... rather than T = Nat = 1 + 1 + 1 + ..., so have written my attempt at an answer but I'm still not sure how to write lambda-terms that correspond to various possibilities.  
> **username_0**: I revised my answer and added a full proof. By the way, do you know how to simplify $\mu X. \,X\to X$? Is it equivalent to $T$? It seems we can write terms of the form $\lambda x_1.\,\lambda x_2.\,...\,\lambda x_m.\, x_n$ as we do for $T$. Can we write any other, inequivalent terms of type $\mu X. \,X\to X$?  
> **username_1**: @winitzki No, this type breaks normalization since you can encode general recursion in it. Consider $(\lambda x. \textsf{unroll}\,x\,x)(\textsf{roll}(\lambda x. \textsf{unroll}\,x\,x))$, where $\textsf{roll} : (C \to C) \to C$ is the constructor, and $\textsf{unroll}$ the destructor.  

---

